axisWitnessDisp0LocalFiberSum
plain-language theorem explainer
Defines the local combinatorial fiber sum for displacement class 0 on the axis witness: sum the closed-form Schläfli pair summands over the six Freudenthal (tet, edge-slot) pairs in the class-0 fiber. Gravity auditors cite it when matching the explicit local fiber against the finite audit table and when bridging global closed-form fiber sums to that local target. The body is a one-line Finset sum, not a proof.
Claim. Let $F_0$ be the explicit local Freudenthal fiber for positive displacement class $0$ (six pairs of tetrahedron index and edge slot). For each pair $p\in F_0$, let $S(p)$ be the sum over the six edge directions of the closed-form Schläfli coefficient of $p$ times the axis-witness flat edge-length contribution in that direction. Define the local class-$0$ fiber sum as $\sum_{p\in F_0} S(p)\in\mathbb{R}$.
background
This module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not grant the physical Dirichlet equality for free; it builds the finite combinatorial objects that later equalities must match.
Displacement classes on the torus are indexed by Fin 7. The local fiber for class $0$ is the explicit six-element set of Freudenthal local pairs (tetrahedron type, edge slot) that carry that class in every cell. Each pair summand folds six Schläfli closed-form coefficients against the axis-witness flat edge-length directions, so the fiber sum is a pure real scalar built from those local data.
The axis witness is the distinguished geometric configuration used to audit the zero-mode / Dirichlet side of the Regge cubic lattice limit. Downstream props compare this scalar both to a global explicit-fiber closed-form sum and to a finite Python-generated audit table.
proof idea
Definition only: expand as the Finset sum of axisWitnessPairSummand over freudenthalLocalPairDispFiber 0. No tactics, no lemmas applied at the definition site. Each summand is itself a six-term sum of Schläfli coefficient times axis-witness flat edge length; the fiber is the hard-coded six-pair set for displacement class 0.
why it matters
This scalar is the local side of the class-0 axis-witness audit bridge in the physical six-tet cubic Dirichlet instance. Downstream, FreudenthalAxisDisp0LocalFiberSumEqAuditTarget asserts equality with the finite audit table sum, discharged by FreudenthalAxisDisp0LocalFiberSumEqAuditTarget_holds via explicit six-pair expansion. Separately, FreudenthalAxisDisp0GlobalFiberSumEqLocalTarget asserts that the global explicit-fiber closed-form sum equals this local sum, with a theorem reducing that claim to per-pair explicit summand matches.
In the broader gravity stack it sits between the periodic Freudenthal torus scaffold and the physical Dirichlet model target: a concrete real that must agree with both combinatorial audit data and the global fiber formula before the encoded torus can be accepted as an instance of the physical six-tet cubic Dirichlet action. It is scaffolding arithmetic for the Regge/Dirichlet side, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.