A registered result in its source context
Original ledger classification: Formal [F] (Lean kernel; no extra axioms)
Recorded statement: Lean 4 formalisation of the v89/v92 arithmetic cores - AUDIT: PASS (machine-formalised [F]): new module TfptCarrier/GlueUniqueness.lean proves by kernel decide (NO native_decide, no new axioms; #print axioms = propext, Classical.choice,…
Statement, assumptions and sources
Paper context: tfpt research contracts
The exact identifier, original classification and full claim are available below.
The source wording and classification below are preserved as recorded. A paper link, shared script or authored topic relation does not upgrade the claim or report a new proof run. Read later reviewed findings separately.
Read the exact registered claim and its dependencies
FORM.GLUE.01
Original ledger classification: Formal [F] (Lean kernel; no extra axioms)
Original claim text
Lean 4 formalisation of the v89/v92 arithmetic cores - AUDIT: PASS (machine-formalised [F]): new module TfptCarrier/GlueUniqueness.lean proves by kernel decide (NO native_decide, no new axioms; #print axioms = propext, Classical.choice, Quot.sound only): (1) the isotropic elements of the carrier discriminant form (Z4xZ4, qZ=(5x^2+3y^2) mod 8) are exactly {(0,0),(1,1),(1,3),(2,2),(3,1),(3,3)}; (2) the order-4 isotropic elements are exactly {(1,1),(1,3),(3,1),(3,3)} and generate exactly TWO cyclic subgroups H1=<(1,1)>, H2=<(1,3)> (orbit equalities formalised); (3) the Klein four-subgroup is NOT isotropic (qZ(2,0)=4) => every order-4 isotropic subgroup is cyclic => GLUE UNIQUENESS up to the spinor swap, which provably exchanges H1<->H2; (4) the unique isotropic order-2 element is (2,2) (the SO(16)_1 halfway stage); (5) carrier index arithmetic 4*4=16, [B:A]^2=16 => index 4=|mu4|=|Z2|^2, mu-additivity 16/16=1; (6) glue sectors are currents (h-eighths sums = 8/8) and 248=45+15+64+64+60. Wired into AxiomCheck.lean + AuditCheck.lean; full lake build 3351 jobs OK; scripts/audit.sh => AUDIT: PASS (transcript refreshed). Toolchain leanprover/lean4:v4.29.1 + mathlib (cache)
Original classification detail
Formal [F]: glue uniqueness + carrier index arithmetic kernel-verified
Dependencies as recorded
GATE.METRIC.06; GATE.METRIC.07; FORM.P2.02
Open the original ledger source, row 169Sections that explicitly cite this claim
A literal claim identifier is present in these paper sections. The section and its premises determine what the citation supports.
- Research Contract 1 — [formula in source]tfpt research contracts
- Front matter / supportTFPT — Introduction and reading guide; Verification reference catalog
- Research Contract 1 — [formula in source]tfpt research contracts
- Front matter / supportResearch contracts
Registered verification modules
No separate module is linked in this claim record. This is a coverage statement, not a verdict about its truth.
A registered module is a source reference. Its presence does not assert that the module was executed in this snapshot.