freudenthalExplicitFiberClosedFormFiberSum
plain-language theorem explainer
Closed-form fiber sum of explicit expanded pair summands for one positive cube-displacement class on the canonical periodic Freudenthal torus. Gravity and Regge workers cite it when packaging mixed hinge-deficit targets or auditing endpoint-only templates against the explicit fiber. The body is a plain finite sum over the local pair fiber of that displacement class.
Claim. For lattice sizes $N_x,N_y,N_z>2$, a vertex conformal potential $\xi$ on the canonical encoded periodic Freudenthal torus, a positive-displacement periodic edge, and a displacement class $d\in\{0,\ldots,6\}$, define the real number equal to the sum, over all local pairs in the fiber of $d$, of the closed-form explicit-fiber expanded summand of $(\xi,\mathrm{edge},\mathrm{pair})$.
background
The module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not assert the physical Dirichlet equality for free; it packages the exact obligations needed to instantiate that model on the torus.
A vertex conformal potential is a real assignment to the vertices of a finite 3D triangulation. A positive-displacement periodic edge is a base vertex together with one of the seven positive cube displacements. The sum runs over the local pair fiber of a fixed displacement class $d$, and each summand is the closed-form explicit-fiber expanded contribution of that local pair for the given potential and edge.
Upstream, the canonical encoded periodic Freudenthal torus is built from the canonical periodic endpoint incidence; the triangulation field supplies the vertex set on which $\xi$ lives.
proof idea
Definition, not a proof. The value is the finite sum of freudenthalExplicitFiberPairClosedFormExpandedSummand over the local pairs in the displacement fiber of $d$. No lemmas are applied; the body is a single summation expression.
why it matters
This sum is the explicit closed-form object that downstream packaging targets compare against endpoint-only templates and mixed hinge-deficit claims. It appears in the per-displacement closed-form mixed target, in the axis-witness global endpoint-unit fiber-sum target (certified value $-4$ on displacement class $0$), in the bridge equating global and local audit sums, and in the bilinear endpoint-template target whose inconsistency with a $-4$ unit sum is already proved for class $0$.
In the broader gravity stack it sits between the periodic Freudenthal geometry and the physical six-tet cubic Dirichlet model: the fiber sum is what must match (or fail to match) endpoint-factorized templates before any Dirichlet equality can be discharged. The finite audit that interior coefficients do not vanish, and that $F(1,1)=0$ is forced by the template while the fiber sum is nonzero on classes $0$ and $3$, is phrased directly in terms of this quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.