freudenthalExplicitFiberDispTableSum_eq_expandedSummandSum
plain-language theorem explainer
On the encoded periodic Freudenthal torus, the fiber sum of Schläfli dihedral derivatives times edge-length directional derivatives equals the sum of the packaged explicit fiber-pair expanded summands, edge by edge. Regge/Dirichlet auditors use it to collapse the mixed hinge-deficit table into the explicit-fiber form. The proof is Finset.sum_congr reducing pointwise to the per-pair expanded-summand identity.
Claim. Fix $N_x,N_y,N_z>2$, a vertex potential $\xi$ on the canonical encoded periodic Freudenthal torus $P$, and a typed periodic edge $e$. Let $F(e)$ be the local pair-displacement fiber of $e$. Then $$\sum_{p\in F(e)}\sum_{k\in\mathrm{Fin}\,6}\bigl(\partial_{\mathrm{dih}}\,\mathrm{tet}(c_p,p)\bigr)_{\!k}\,\partial_{\ell}\mathrm{len}(\xi;c_p,p)_k = \sum_{p\in F(e)} S_{\mathrm{exp}}(\xi,e,p),$$ where $c_p$ is the periodic matching base cell of the cube edge of $p$, and $S_{\mathrm{exp}}$ is the explicit fiber-pair expanded summand.
background
This module packages the 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 only supplies the algebraic bridges between the scaffold and the target.
The setting is a 3-torus triangulated by the Freudenthal six-tetrahedra-per-cube scheme, with periodic edge types and a vertex potential $\xi$. Hinge geometry enters through Schläfli data: each tetrahedron carries dihedral-angle derivatives with respect to its six edge lengths. The deficit at a hinge is $2\pi-\sum\theta$ (DihedralAngle.deficit). Local pairs in a displacement fiber index the cube-edge incidences that contribute to a given periodic edge.
The left-hand sum is the table form: match each fiber pair to a base cell, pull tet data via the torus tet-equivalence, and contract dihedral derivatives against directional edge-length derivatives of $\xi$. The right-hand sum packages the same contribution as an expanded summand per fiber pair.
proof idea
One-step Finset congruence. Apply Finset.sum_congr rfl over the local pair-displacement fiber; the index set is identical on both sides. For each fiber pair, dsimp unfolds the selected-cell abbreviation, then invoke the already-proved per-pair identity freudenthalExplicitFiberPairExplicitInnerSum_eq_expandedSummand, which equates the inner Fin-6 Schläfli contraction on the matched cell to the explicit expanded summand. No further arithmetic is needed.
why it matters
Sits in the Gravity domain bridge from the periodic Freudenthal scaffold to PhysicalSixTetCubicDirichletModel. Sibling declarations (periodic edge-stencil Dirichlet action and target, canonical Hessian-is-Dirichlet certificates, mixed-axis stencil actions) consume equalities of this shape when they rewrite the mixed hinge-deficit table into a rational axis stencil comparable to the finite-difference audit.
The nearby corrected explicit-fiber global form keeps the global sum over typed periodic edges and compares it to that stencil; the present lemma is the fiber-level bookkeeping step that makes the global comparison well-typed. No downstream used_by edges are recorded yet, so it is presently a leaf obligation inside the instance package rather than a cited parent theorem.
Framework role is geometric infrastructure for the Regge-side Dirichlet limit on the cubic lattice, not a direct T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.