freudenthalExplicitFiberPairClosedFormExpandedSummand_eq_flat
plain-language theorem explainer
On a canonical periodic Freudenthal torus with sides larger than 2, the closed-form per-pair expanded summand (Schläfli dihedral derivative times local edge-length directional derivative) equals the flat-unfolded per-pair summand at the selected matching cell. Lattice gravity and Regge-calculus workers cite this when swapping closed-form tet data for flat torus data inside the explicit-fiber table. Proof is unfold, Finset.sum_congr, and one dihedral-derivative identification.
Claim. Let $N_x,N_y,N_z>2$, let $\xi$ be a vertex potential on the canonical encoded periodic Freudenthal torus of those sizes, let $e$ be a positive-displacement periodic edge, and let $(\tau,s)\in\{0,\ldots,5\}^2$ be a local Freudenthal (tet, edge-slot) pair. Then the closed-form expanded summand for that pair (sum over slots of the freudenthal-tet dihedral length derivative times the flat local edge-length directional derivative of $\xi$) equals the flat-unfolded expanded summand at the selected matching cell.
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.
A local Freudenthal pair is an element of $\mathrm{Fin},6\times\mathrm{Fin},6$: a (tet index, edge-slot) after the periodic-cell base-offset equation has been isolated. The ambient geometry is the canonical encoded periodic Freudenthal torus (sides $N_x,N_y,N_z>2$), with vertex potentials on its $K$-structure and positive-displacement periodic edges (base vertex plus one of seven cube displacements).
The closed-form side uses dihedral length derivatives of the unit-cube Freudenthal tetrahedron; the flat side uses the triangulation Schläfli data of the same torus. Both multiply by the same flat local edge-length directional derivative of $\xi$ at the selected matching cell.
proof idea
Unfold both expanded summands and the local-pair closed-form summand. Fix the selected matching cell for the given edge and pair. Apply Finset.sum_congr so it remains only to match summands slotwise.
Each slot contribution is a product: dihedral length derivative times the flat local edge-length directional derivative of $\xi$. The second factor is identical on both sides. The first factors are identified by rewriting with canonicalPeriodicFlat_tet_dihedralDeriv_eq_freudenthalClosed, which equates the freudenthal-tet closed dihedral derivative to the dihedral derivative from the torus triangulation Schläfli data at the image tet under the cell/pair encoding.
why it matters
This is a per-pair bridge between closed-form Schläfli data and flat-unfolded fiber data inside the explicit-fiber expansion. Downstream it feeds the full fiber-sum equality freudenthalExplicitFiberFlatDispFiberSum_eq_closedFormFiberSum, the linearity lemmas (add and scalar multiplication) for the closed-form expanded summand, and the two target-transfer theorems that move between CanonicalPeriodicMixedHingeDeficitExplicitFiberClosedFormTarget and the flat-unfolded target.
It also supports the axis-stencil coefficient certificate that expands one explicit-fiber local pair into checked endpoint-slot atoms. In the Recognition gravity stack this is scaffolding closure for the physical six-tet cubic Dirichlet instance on the periodic Freudenthal torus, not a new continuum claim: it keeps the discrete Regge first-variation bookkeeping consistent across the two presentations of the same fiber table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.