freudenthalExplicitFiberDispTableExpandedSum_eq_typedEdgeInTetExpandedIncidentSum
plain-language theorem explainer
On a periodic Freudenthal torus with periods larger than 2, the expanded fiber-pair sum over displacement-matched local pairs equals the typed edge-in-tet incident sum of dihedral derivatives times edge-length directional derivatives. Gravity and discrete-Regge workers cite it when reindexing mixed hinge-deficit stencils from explicit-fiber tables to canonical incidence form. The proof is a three-step calc: fiber table to local-pair inner sum, then slot-guarded reindex, then per-tet edgeInTet match.
Claim. Let $N_x,N_y,N_z>2$ and let $P$ be the canonical encoded periodic Freudenthal torus on those periods. For any vertex potential $\xi$ on $P$ and any periodic edge $e$, the sum of expanded fiber-pair summands over the local displacement fiber of $e$ equals $\sum_\tau$ of either $0$ (if $e$ is not incident to tetrahedron $\tau$) or $\sum_{k=0}^{5}(\partial\theta/\partial\ell)_{\tau,f,k}\,(\partial\ell/\partial\xi)_{\tau,k}$ when the incidence map returns local slot $f$.
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 assert the physical Dirichlet equality for free.
The ambient complex is the canonical encoded periodic Freudenthal torus $P$: a cubic lattice with six-tetrahedron Freudenthal triangulation per cell, periodized in three axes with $N_x,N_y,N_z>2$. Edges carry a typed incidence map edgeInTet (global edge and tet to optional local slot) and the inverse localEdgeOf (tet and local slot to global edge). Schläfli data on each tet supply dihedral-angle derivatives with respect to the six edge lengths; vertex potentials $\xi$ induce directional derivatives of those lengths.
The left-hand side packages the same contribution as an explicit fiber over displacement-matched local pairs (a table-driven form convenient for axis stencils). The right-hand side is the canonical typed incidence sum used by hinge-deficit and Dirichlet targets downstream.
proof idea
Three-step calc.
-
Apply
freudenthalExplicitFiberDispTableExpandedSum_eq_localPairExpandedInnerSumto rewrite the fiber-pair sum as a double sum over the six local tets and the Finset of local slots $f$ whose cube-edge displacement matchesedge.disp, with summands built from Schläfli dihedral derivatives at the periodically matched base cell times length directional derivatives. -
Apply
canonicalPeriodicTypedEdge_localPairExpandedInnerSum_eq_slotGuardedInnerSumto reindex that expression to a sum over all global tets $\tau$, with an inner sum over slots $f$ guarded by the equalityedge = localEdgeOf(cell,tet,f)(else zero). -
Pointwise in $\tau$, invoke the symmetric form of
canonicalPeriodicTypedEdge_perTet_edgeInTetExpanded_eq_slotGuardedto replace the slot-guarded sum by thematch edgeInTet e τexpression that is the theorem's right-hand side. Finish withFinset.sum_congr.
why it matters
This identity is the finite reindexing bridge between explicit-fiber bookkeeping and typed edgeInTet incidence on the periodic six-tet complex. Downstream, canonicalPeriodicTrack1BFiniteReindexingTarget_holds is literally a one-line application of it for every potential and edge.
It also feeds the mixed hinge-deficit chain: canonicalPeriodicMixedHingeDeficitExpandedLengthChainTypedEndpointTarget_of_explicitFiber and the converse typed-to-explicit direction, and the safer axis-stencil route canonicalPeriodicMixedHingeDeficitAxisStencilTarget_of_explicitFiberAxis, whose doc-comment calls this the proved finite reindexing that keeps the typed-edge sum global then returns to canonical incidence form.
In the broader RS gravity stack this is scaffolding closure for the physical six-tet cubic Dirichlet instance on the Freudenthal torus (Regge-action / discrete curvature side), not a continuum Einstein equation. It sits under the $D=3$ lattice geometry forced upstream (T8) and under the eight-tick / cubic cell combinatorics, but does not itself touch $J$-cost, $\varphi$-ladder masses, or $\alpha$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.