freudenthalExplicitFiberPairExplicitInnerSum_eq_expandedSummand
plain-language theorem explainer
On the canonical encoded periodic Freudenthal torus, the six-term inner sum of dihedral derivatives times edge-length directional derivatives at a local (tet, edge-slot) pair equals the expanded fiber summand at the selected matching cell. Gravity and Regge-calculus workers cite it when collapsing the explicit fiber table to a single summand. The proof is pure definitional equality (rfl).
Claim. Fix lattice sizes $N_x,N_y,N_z>2$ and a vertex conformal potential $\xi$ on the canonical encoded periodic Freudenthal torus $P$. For any positive-displacement periodic edge and any local Freudenthal pair $(\tau,e)\in\mathrm{Fin}\,6\times\mathrm{Fin}\,6$, writing $\mathrm{cell}$ for the selected matching cell of that edge-pair, $$\sum_{k=0}^{5}\partial_{\theta_k}\!\mathrm{dihedral}(\mathrm{tetData}(\tau_{\mathrm{cell}}),e)\,\cdot\,\partial_{\xi}\ell_k(\tau_{\mathrm{cell}})=\mathrm{ExpandedSummand}(\xi,\mathrm{edge},(\tau,e)).$$
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not freely assert the physical Dirichlet equality.
The ambient complex is the canonical encoded periodic Freudenthal torus $P$ built from endpoint incidence on an $N_x\times N_y\times N_z$ lattice ($N_i>2$). Vertex conformal potentials are real functions on the vertices of $P$'s triangulation. A periodic edge is a base vertex plus one of seven positive cube displacements. Local Freudenthal pairs are the finite table $\mathrm{Fin},6\times\mathrm{Fin},6$ of (tetrahedron, edge-slot) indices left after the periodic-cell base-offset equation is isolated.
The left-hand side assembles, at the selected matching cell, the product of the Schläfli dihedral derivative (from incidence triangulation data) with the directional derivative of local edge length $\sqrt{a_f}$ under $\xi$. The right-hand side is the already-expanded fiber summand for that same edge and pair.
proof idea
One-line definitional proof: rfl. The expanded summand is defined to be exactly the six-term sum of dihedralDeriv times localEdgeLengthDirectionalDeriv evaluated on the tet obtained by transporting the selected cell through $P$'s tet equivalence. Unfolding both sides yields identical terms, so no algebraic rewriting is required.
why it matters
Feeds the parent theorem that equates the full explicit-fiber displacement-table sum to the sum of expanded summands over local pairs. That step is part of wiring the encoded periodic Freudenthal scaffold into the PhysicalSixTetCubicDirichletModel target: matching inner sums cell-by-cell lets the Hessian/Dirichlet action on the six-tet cubic lattice be read off from the fiber table without residual combinatorial mismatch.
In the broader gravity stack this sits under Regge first-variation and 3D Hessian infrastructure on the Freudenthal triangulation, supporting the finite-difference Dirichlet action used for the cubic lattice continuum limit. It is bookkeeping equality, not a new physical law, but it closes a necessary identification in the instance chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.