Skip to content

README.md

Latest commit

 

History

History
150 lines (125 loc) · 7.66 KB

README.md

File metadata and controls

150 lines (125 loc) · 7.66 KB
Raw

BongTheory

BongTheory is a Lean 4 formalization of the theory of bases of norm generators (BONGs) for quadratic lattices over dyadic local fields. Its principal source results are five papers by Constantin N. Beli published or circulated in 2003, 2006, 2009/2010, 2019, and 2020. The two arXiv papers use their frozen 2022 v2 revisions. Active public extensions cover the published versions of the He--Hu n-universality paper and He's n-ADC paper. The separate He classic formalization is deliberately withheld from this GitHub deployment.

Current status

  • Proof-assistant status: the public theorem endpoints compile and use only propext, Classical.choice, and Quot.sound; conditional arithmetic endpoints keep each undischarged mathematical premise visible in their type.
  • Semantic-fidelity status: PROVISIONAL_MATCH.
  • Beli 2020 coverage status: FORMALIZATION_COMPLETE_WITH_SOURCE_DISCREPANCY; its printed Theorem 3.1 exponent is kept separate from the exponent derived from Theorem 2.1.
  • He-paper coverage status: PARTIAL. He--Hu has complete formal coverage of its 47 numbered results subject to semantic sign-off; He ADC Section 6 is fully triaged and Section 7 has 20/21 fully formalized numbered items, one documented quantifier mismatch, and a complete Corollary 7.21 catalogue whose final numerical formulas now use an internal proof of the cited O'Meara 63:9 unit-square-class count.
  • Project grade: D because the He ADC audit identifies a substantive theorem-level mismatch; this does not downgrade the separately graded kits.
  • Local reproducibility status: REPRODUCIBLE_WITH_DOCUMENTED_EXTERNAL_DEPENDENCIES at commit 9350ca37181f3275129d16e091e9dd09a7ee5846 for the He ADC closure through Report 68; its independently extracted historical package passes a fresh 5,581-job build and the 60,948-declaration enforcing gate. Report 69 discloses why its shared root documents do not satisfy the new single-paper packaging rule and are not the final release asset. He--Hu has its separate exact, independently extracted Review Kit at 8bff7e2. See He ADC Report 69 and He--Hu Report 14.
  • Public hosted reproducibility status: exact-tag Ubuntu and Windows checks passed under the scopes and cache boundaries recorded in the public v0.2.0-rc.1 receipt. The initial Ubuntu build succeeded but its following audit step exposed a cross-platform workflow-path defect; the failure and corrected exact-tag run are both retained in that receipt.

Compilation is evidence that Lean accepts the encoded statements. It is not, by itself, evidence that every paper statement has been translated faithfully. The independent mathematical-review package is under docs/audit.

Formalized public results

Source Paper result Lean endpoint
Beli 2003 Theorem 1 Bong.BONG.beliTheoremOne_proved
Beli 2003 Theorem 2 Bong.Lattice.beliTheoremTwo_proved
Beli 2003 Theorem 3 Bong.BONG.beliTheoremThree_proved
Beli 2006 Theorem 3.2 Bong.beli2006Theorem32_proved
Beli 2006 Theorem 4.5 Bong.beli2006Theorem45_proved
Beli 2009/2010 Theorem 3.1 Bong.BONG.GoodBONG.beli2009Theorem31_concrete
Beli 2019 v2 Theorem 2.1 Bong.beli2019Theorem21
Beli 2019 v2 Theorem 2.1 with (iii') Bong.beli2019Theorem21_prime
Beli 2020 Theorem 2.1 Bong.BONG.GoodBONG.isUniversal_iff_universalTheorem21Conditions
Beli 2020 Theorem 3.1, direct derivation Bong.Lattice.JordanDecomposition.isUniversal_iff_universalTheorem31DirectConditions
Beli 2020 Corollary 4.10 Bong.BONG.GoodBONG.beliUniversalCorollary410

See THEOREM_INDEX.md for a fuller source-to-code map and SOURCES.md for the exact paper versions used.

He papers under active formalization

Published source Current public endpoint Honest status
He--Hu, Sci. China Math. 67 (2024), Theorems 1.1-1.2 heHu2022Theorem11, heHu2022Theorem12PublishedEvenLiteral, heHu2022Theorem12PublishedOddLiteral proved; semantic review remains provisional
He, Doc. Math. 30 (2025), local Sections 4, 6, and 7 published-family profiles, complete Section 6 triage, Theorems 7.1, 7.2 and 7.4, the chain through Remark 7.3, the Corollary 7.21 catalogue, and O'Meara 63:9 partial paper; Lemma 7.13 has a quantifier mismatch, while all dyadic numerical counts are unconditional in the repository interface

The ADC paper's Lemma 6.8(iv) is refuted at n=2 by an actual nonmaximal 2-ADC lattice, with a concrete Q_2 check. See each paper's fidelity report for exact coverage, assumptions, source discrepancies, and missing human approval.

For these two publicly deployed papers the publisher version of record is the sole semantic authority. Preprints are retained only as separately hashed comparison sources. The implementation order and promotion gates are recorded in docs/HePapersRoadmap.md.

Download one paper

Reviewers do not need the complete development tree. The paper-specific Review Kit index links released source-only ZIPs and records pending kits. Each kit contains its canonical Lean entry, axiom audit, fidelity package, exact source commit, and checksums. Every kit is generated from the local transitive import closure and is built again after extraction; unreleased manifests are also built as per-paper CI artifacts.

The metadata-driven procedure in papers/SCHEMA.md is the default distribution requirement for every later BONG-related paper added to this repository.

Reproduce locally

The repository pins Lean in lean-toolchain and all Lake dependencies in lake-manifest.json.

lake exe cache get
lake build
lake env lean BongTest/FinalPublicTheoremAudit.lean
lake env lean BongTest/Beli2003Audit.lean
lake env lean BongTest/Beli2006Audit.lean
lake env lean BongTest/Beli2009Audit.lean
lake env lean BongTest/Beli2019Audit.lean
lake env lean BongTest/Beli2020Audit.lean
lake env lean BongTest/HeHu2022Audit.lean
lake env lean BongTest/He2023ADCAudit.lean

For the complete clean-clone protocol and expected output, see REPRODUCING.md. The audited Windows source-rebuild receipt is docs/reproducibility/clean-clone-5befe079.md. The current public hosted receipt is docs/reproducibility/github-actions-v0.2.0-rc.1.md.

Repository layout

Bong/                  formal definitions and proofs
Bong/Papers/           canonical paper-specific import entry points
BongTest/              compilation, signature, and axiom audits
papers/                paper manifests, download index, and packaging standard
scripts/paper-kits/     Review Kit generation and clean-extract verification
docs/audit/            semantic-fidelity review packages
docs/DevelopmentHistory.md
                       chronological M0--M... development record

Development scratch files and generated .olean files are intentionally not tracked. Publisher PDFs are not redistributed; the repository records source links and cryptographic hashes instead.

Trust and review

The formal trust boundary and the distinction between kernel checking, reproducibility, and mathematical semantic review are documented in TRUST.md. Instructions for independent reviewers are in REVIEWING.md.

License and citation

The Lean source is released under Apache-2.0; see LICENSE. Citation metadata is provided in CITATION.cff. The papers remain under their respective publishers' or arXiv licences.