freudenthalExplicitFiberPairExpandedSummand
plain-language theorem explainer
Expanded Schläfli/length-chain summand for one explicit-fiber local pair on the canonical periodic Freudenthal torus. Given a vertex potential, a periodic edge, and a local (tet, edge-slot) pair, it returns the six-term product sum of dihedral derivatives times edge-length directional derivatives at the selected encoded tetrahedron. Regge/gravity workers cite it when expanding mixed hinge-deficit first variations into explicit fiber contributions. Pure definition: select cell and tet, then form the angle-length chain sum.
Claim. For $N_x,N_y,N_z>2$, vertex potential $\xi$ on the canonical encoded periodic Freudenthal torus, periodic edge $e$, and local pair $(t,s)\in\{0,\ldots,5\}^2$, the expanded explicit-fiber summand is $$\sum_{k=0}^{5}(\partial_{\theta_s}\ell_k)\,D_k\xi,$$ where the sum runs over the six edges of the selected encoded tetrahedron for $(e,(t,s))$, $\partial_{\theta_s}\ell_k$ is the Schläfli dihedral derivative of edge $k$ at slot $s$, and $D_k\xi$ is the directional derivative of that edge length under $\xi$.
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 free-assert the physical Dirichlet equality; it wires the encoded torus scaffold to the model target.
A local Freudenthal pair is an element of $\mathrm{Fin},6\times\mathrm{Fin},6$: a finite table of (tet index, edge-slot) pairs left after the periodic-cell base-offset equation is isolated. The ambient geometry is the canonical encoded periodic Freudenthal torus built from endpoint incidence, with dimensionless bridge ratio $K=\varphi^{1/2}$.
Upstream, triangulation Schläfli data supply per-tet dihedral derivatives, and localEdgeLengthDirectionalDeriv supplies the first variation of edge length under a vertex potential. The summand is the local angle-length chain product at one selected tet and slot.
proof idea
Definition, not a proved identity. Bind the canonical encoded torus $P$, choose the cell for the given edge and local pair, recover the encoded tetrahedron $\tau$ via the tet equivalence, then sum over $k:\mathrm{Fin},6$ the product of the Schläfli dihedral derivative at the pair's edge-slot with the local edge-length directional derivative of $\xi$ on edge $k$ of $\tau$. No lemmas are applied; the body is the expanded chain-rule term itself.
why it matters
This is the atomic expanded summand in the explicit-fiber route to the mixed hinge-deficit axis stencil. Downstream it appears inside the $N=5$ residual and mixed LHS expansions (explicitFiberAxisStencilResidualAtN5, explicitFiberMixedLhsAtN5) and in the pair/edge scaled-expansion theorems that match checked endpoint-slot coefficient atoms.
In-module it feeds the chain of targets that lift an explicit-fiber identity to the canonical periodic mixed hinge-deficit axis-stencil target (the safe replacement for the false typed-endpoint route). That chain is how the module discharges obligations for the physical six-tet cubic Dirichlet instance on the Freudenthal lattice, connecting discrete Regge first variation to the Dirichlet action target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.