freudenthalExplicitFiberDispTableExpandedSum_eq_localPairExpandedInnerSum
plain-language theorem explainer
On a large enough periodic Freudenthal torus, the expanded fiber sum over local pairs sharing a fixed edge displacement equals the nested sum that walks the six tetrahedra, filters local edge slots with that displacement, and contracts Schläfli dihedral derivatives against directional edge-length derivatives of the vertex potential. Gravity and discrete-Regge workers cite it when collapsing pair-indexed tables to tet-incident form. The proof is a Finset reindexing: fiber-as-filter, product-universe, and sum_congr on the expanded summand.
Claim. Let $N_x,N_y,N_z\ge 3$ and let $P$ be the canonical encoded periodic Freudenthal torus of those sizes. For any vertex potential $\xi$ on $P$ and any periodic edge $e$, the sum of the expanded fiber pair summands over all local pairs whose displacement equals $e$'s displacement equals $\sum_{t=0}^{5}\sum_{f:\,\mathrm{disp}(t,f)=\mathrm{disp}(e)}\sum_{k=0}^{5}(\partial\theta/\partial\ell)_{f k}\,D_k\ell(\xi)$ evaluated on the periodically matched base cell of that local edge.
background
The module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not freely assert the physical Dirichlet equality; it supplies the algebraic bridges between pair-fiber bookkeeping and tet-incident expansions.
A Freudenthal cube is split into six tetrahedra. Each tet has six local edge slots mapped by localEdgeOf into the nineteen one-cube edge representatives; cubeEdgeBase and cubeEdgeDisp record the base vertex and lattice displacement of each representative. Periodic edges on the torus are pairs (base cell, displacement). The fiber of a displacement is the set of local pairs (tet index, local face/edge slot) whose cube edge carries that same displacement.
The expanded summand multiplies a Schläfli dihedral derivative from the incidence-built triangulation data by the directional derivative of local edge length under the vertex potential $\xi$. The constant $K=\varphi^{1/2}$ appears only as the dimensionless bridge scale on the encoded complex, not as a free parameter in the identity.
proof idea
First prove an auxiliary equality hsum: the nested sum over tet $\in\mathrm{Fin},6$ and filtered local slots $f$ with matching displacement equals the sum over the filtered universe of FreudenthalLocalPair of the same contracted dihedral/length term. That step unfolds the pair type and displacement projection, rewrites via univ_product_univ, sum_filter, and sum_product, then simplifies with eq_comm.
The main calc has two legs. (1) Replace the named fiber by the filter characterization freudenthalLocalPairDispFiber_eq_filter, then sum_congr with dsimp of the expanded summand and selected cell so the left-hand fiber sum becomes the filtered pair sum. (2) Apply hsum.symm to turn that filtered pair sum into the tet-then-filter nested form on the right-hand side. No analytic estimates; pure finite-sum reindexing.
why it matters
This identity is the bookkeeping hinge between displacement-fiber tables and tet-incident expansions of the discrete Dirichlet/Regge variation on the six-tet cubic complex. The sole recorded consumer is freudenthalExplicitFiberDispTableExpandedSum_eq_typedEdgeInTetExpandedIncidentSum, which lifts the same equality one step further toward typed edge-in-tet incident sums used by the physical model instance.
In the broader Recognition gravity stack, the periodic Freudenthal torus is the concrete lattice carrier for the cubic Dirichlet target and the nonlinear Regge correspondence imports. Closing fiber-to-incident equalities is required before the canonical Hessian can be certified as a Dirichlet form on the encoded complex. The result sits downstream of the geometry scaffold (periodic torus, cube triangulation, Schläfli incidence data) and upstream of the physical six-tet Dirichlet packaging; it does not itself touch the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.