freudenthalExplicitFiberPairExpandedSummand_eq_angleChain
plain-language theorem explainer
On a periodic Freudenthal torus (grid sizes > 2), the expanded explicit-fiber summand for a local (tetrahedron, edge-slot) pair equals the local angle–length chain derivative at the corresponding encoded tetrahedron and slot. Gravity and Regge-calculus workers cite it when wiring hinge-deficit expansions to first-variation length chains. The proof is pure definitional equality (rfl).
Claim. Let $N_x,N_y,N_z>2$ and let $T$ be the canonical encoded periodic Freudenthal torus on that grid. For any vertex potential $\xi$ on $T$, any positive-displacement periodic edge $e$, and any local Freudenthal pair $p=(\tau,s)\in\{0,\ldots,5\}\times\{0,\ldots,5\}$, the expanded explicit-fiber summand of $(\xi,e,p)$ equals the local angle–length chain derivative of $\xi$ at the encoded tetrahedron selected by $(e,p)$ and at edge-slot $s$.
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 freely assert the physical Dirichlet equality.
A local Freudenthal pair is a finite table entry $(\tau,s)\in\mathrm{Fin},6\times\mathrm{Fin},6$ left after the periodic-cell base-offset equation is isolated: six tetrahedra per cube cell and six edge slots per tet. Periodic edges are positive-displacement edges on the torus (base vertex plus one of seven cube displacements). The squared-edge data of each Freudenthal tet are the fixed tuple of three unit steps, two face diagonals, and one body diagonal.
The local angle–length chain derivative is the first-variation building block that differentiates dihedral angle contributions with respect to edge lengths along a length chain. The expanded explicit-fiber summand is the same quantity written after the fiber over the periodic edge has been expanded and the squared-edge factor unfolded.
proof idea
One-line definitional equality: both sides reduce to the same term once the expanded summand is unfolded at the selected encoded tetrahedron (via the torus tet-equivalence inverse applied to the fiber-selected cell and tet index) and the given edge slot. No algebraic rewriting or case split is required; Lean closes by rfl.
why it matters
The identity is the bridge that lets hinge-deficit expansions on the six-tet cubic lattice be rewritten as angle–length chain derivatives, which is the language of the Regge first-variation and Hessian machinery used for the physical Dirichlet target.
It is consumed by the two conversion theorems that pass between the explicit-fiber target and the angle-chain target for the canonical periodic mixed hinge-deficit expanded length chain. Those conversions are part of the obligation package that instantiates PhysicalSixTetCubicDirichletModel on the encoded periodic Freudenthal torus scaffold. In the broader RS gravity stack this sits under the discrete curvature / Regge route toward continuum Dirichlet energy on the cubic lattice, not under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.