FreudenthalAxisDisp0GlobalFiberSumEqLocalTarget
plain-language theorem explainer
Bridge proposition asserting that the global closed-form fiber sum on the axis witness edge (displacement class 0, endpoint unit potential) equals the local combinatorial audit fiber sum. Gravity workers cite it when wiring the periodic Freudenthal torus into the physical six-tet cubic Dirichlet model. It is a bare equality Prop; discharge is left to sibling theorems.
Claim. The closed-form fiber sum of the endpoint-unit vertex potential along the axis witness edge at displacement class $0$ equals the local combinatorial fiber sum $\sum_{\mathrm{pair}\in F_0} s(\mathrm{pair})$ over the Freudenthal local pair-displacement fiber at $0$.
background
This module packages the exact obligations needed to instantiate PhysicalSixTetCubicDirichletModel on an encoded periodic Freudenthal torus. It does not grant the physical Dirichlet equality for free; each bridge is an explicit Prop.
The global side is the closed-form fiber sum for one positive displacement class: given lattice bounds $N_x,N_y,N_z>2$, a vertex potential $\xi$, a periodic edge, and a displacement index $d\in\mathrm{Fin},7$, it evaluates the explicit fiber contribution. Here the potential is the endpoint-unit potential on the axis witness, the edge is the axis witness edge with base $(1,0,0)$ and displacement $0$, and $d=0$.
The local side is the combinatorial audit sum: sum of axis-witness pair summands over the local pair-displacement fiber at displacement $0$. The doc-comment states the intent directly: "Local combinatorial fiber sum matches the finite audit table."
proof idea
Definition only: the body is the bare equality of two real numbers, the closed-form fiber sum applied to the witness lattice bounds, endpoint-unit potential, axis witness edge, and displacement $0$, versus the local audit fiber sum. No tactics or lemmas are invoked at this declaration; sibling theorems later discharge the Prop by reducing through pair-explicit summand equalities.
why it matters
This Prop is the local-to-global bridge on the axis witness for displacement class $0$. Downstream, FreudenthalAxisDisp0GlobalFiberSumEqLocalTarget_of_all_pair_explicit turns an all-pair explicit match into this equality, and FreudenthalAxisDisp0GlobalFiberSumEqLocalTarget_holds asserts it holds. From there, FreudenthalAxisDisp0GlobalEndpointUnitFiberSumTarget_of_local (and the audit-augmented variant) lift the local match to the global endpoint-unit fiber-sum target required by the physical six-tet cubic Dirichlet instance.
In the broader RS gravity stack this sits under the Regge/Freudenthal lattice limit path that feeds the physical Dirichlet action on the cubic six-tet scaffold. It is bookkeeping, not a new physical law, but without it the encoded periodic torus cannot be certified against the finite audit table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.