freudenthalAxisDisp0EndpointUnitAuditSum
plain-language theorem explainer
Named real constant equal to the six audit-mirrored per-pair contributions for Freudenthal axis class 0 at endpoint-unit data (base (1,0,0), N=5). Gravity and discrete-geometry workers cite it when matching combinatorial local fiber sums to the finite Python audit table. The body is a literal six-term rational sum that evaluates to -4.
Claim. Define the audit sum for axis class $0$ at endpoint-unit data (base $(1,0,0)$, lattice size $N=5$) by the six per-pair contributions $$\tfrac{-1}{2}+\tfrac{-1}{2}+(-1)+\tfrac{-1}{2}+(-1)+\tfrac{-1}{2}\in\mathbb{R}.$$
background
The module packages exact 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 wires scaffold data to the model target.
Axis class 0 is the displacement class along a coordinate axis of the Freudenthal cube triangulation. Endpoint-unit data means the base edge is the unit vector $(1,0,0)$ on a periodic lattice of size $N=5$. The six summands are the audit-mirrored per-pair contributions produced by the external script freudenthal_explicit_fiber_endpoint_analysis.py, one for each local pair in the class-0 fiber.
Sibling infrastructure includes periodic edge stencils, axis-displacement actions, and Dirichlet targets on the canonical Hessian. This constant is the finite numerical table those combinatorial sums are checked against.
proof idea
Pure definition: the body is the six-term rational expression written out in place. No lemmas, no tactics. Downstream, norm_num after unfold shows the sum equals $-4$.
why it matters
Closes the numerical side of the class-0 axis audit bridge inside the physical six-tet cubic Dirichlet instance. Downstream, the equality theorem records that the constant is exactly $-4$, and the proposition FreudenthalAxisDisp0LocalFiberSumEqAuditTarget asserts that the combinatorial local fiber sum equals this audit value; its holding theorem discharges that match by expanding the six pair summands.
In the broader gravity stack this is one concrete check that the encoded periodic Freudenthal torus scaffold reproduces the finite-difference Dirichlet action expected by the physical model. It is bookkeeping, not a forcing-chain step, but without the matched audit table the Dirichlet instantiation obligations stay open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.