FreudenthalAxisDisp0LocalFiberSumEqAuditTarget
plain-language theorem explainer
Equates the local combinatorial fiber sum for class-0 axis witnesses with a six-term finite audit table of endpoint-unit contributions. Gravity and Regge-lattice workers cite this Prop when wiring Freudenthal-torus fiber audits into the physical six-tet Dirichlet model. It is a bare equality of two reals; discharge is separate (six Finset.sum_eq_single plus norm_num certificates).
Claim. The sum of axis-witness pair summands over the local displacement-class-$0$ fiber equals the six-term audit total $(-1/2)+(-1/2)+(-1)+(-1/2)+(-1)+(-1/2)$ at endpoint-unit data (base $(1,0,0)$, $N=5$).
background
This module packages exact theorem obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it records the combinatorial and audit targets that must hold.
The left-hand side is the real sum of axis-witness pair summands over the local pair-displacement fiber at class $0$. The right-hand side is the audit-mirrored total for axis class $0$ at endpoint-unit data, matching the explicit Python fiber-endpoint analysis: six rational contributions summing the same pairs.
Sibling scaffolding in the module builds periodic edge stencils, canonical Hessian/Dirichlet actions, and axis-displacement stencils on the Freudenthal lattice. The audit sum is the finite checkpoint those combinatorial sums must hit before global fiber identities are assembled.
proof idea
Definition only: the Prop is the literal equality of the local fiber sum with the six-term audit constant. No proof body. Discharge lives in the companion theorem that unfolds the fiber sum, splits it by six Finset.sum_eq_single steps (one per audited pair), and closes each summand by norm_num, following the generated certificate script.
why it matters
Closes the local-audit link in the Freudenthal axis class-$0$ chain toward the physical six-tet cubic Dirichlet instance. Downstream, the global endpoint-unit fiber-sum target is obtained from the global-equals-local target together with this audit equality; the companion holds theorem supplies the concrete certificate. Without matching the finite audit table, the periodic Freudenthal scaffold cannot be trusted as an instance of the physical Dirichlet model. This is bookkeeping on the gravity side of the RS lattice program (Regge/cubic limit, length-chain endpoints), not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.