canonicalPeriodicMixedHingeDeficitExpandedLengthChainLocalPairTarget_of_fiber
plain-language theorem explainer
If the mixed hinge-deficit expanded length-chain target holds in single-filtered local-pair fiber form on the canonical periodic Freudenthal torus, then it holds in ordinary local-pair form. Gravity workers packaging the six-tet cubic Dirichlet instance cite this when collapsing displacement-fiber sums to local pairs. The proof is a Finset reindexing that equates the (tet, face) double sum with the Freudenthal local-pair sum, then applies the fiber hypothesis.
Claim. Let $N_x,N_y,N_z\in\mathbb{N}$ with each at least $3$. If the mixed hinge-deficit expanded length-chain target holds in its single-filtered local-pair fiber form (sum over $\mathrm{FreudenthalLocalPair}$ with fixed displacement) on the canonical encoded periodic Freudenthal torus of size $(N_x,N_y,N_z)$, then it holds in ordinary local-pair form, where for each local pair the periodic cell sum collapses to the unique base cell matching the edge offset.
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; it connects the encoded periodic scaffold to the model target.
The ambient geometry is the canonical encoded periodic Freudenthal torus of size $(N_x,N_y,N_z)$ with $N_i>2$. Edges carry a base cell and a displacement; the six-tet Freudenthal triangulation of the unit cube supplies local edge slots via localEdgeOf, with cube-edge base and displacement maps. The dimensionless bridge ratio $K=\varphi^{1/2}$ enters the Schläfli and length-derivative data.
Two sibling propositions state the same mixed target. The ordinary local-pair form filters by tet and face with matching cube-edge displacement, collapsing the periodic cell sum to the unique matching base cell. The fiber form rewrites that content as a single sum over Freudenthal local pairs with fixed displacement. This theorem bridges the two.
proof idea
Fix the canonical encoded periodic Freudenthal torus $P$. For arbitrary vertex potential $\xi$ and periodic edge, the goal is the ordinary local-pair target equality. The only work is a sum reindexing identity: the double sum over tet $\in\mathrm{Fin},6$ and faces $f$ with matching cube-edge displacement equals the sum over Freudenthal local pairs with the same displacement, both carrying the same Schläfli dihedral derivative times local edge-length directional derivative at the matched cell.
That identity is proved by unfolding the local-pair type and its displacement projection, rewriting via the product of universes, sum_filter, and sum_product, then simplifying with commutativity of equality. After rewriting the goal along the identity, the fiber hypothesis applies directly to $\xi$ and the edge.
why it matters
The sole downstream consumer is the canonical edge-stencil local-correspondence theorem that takes mixed targets in explicit local-pair displacement-fiber form. That parent packages the local-correspondence endpoint for the physical six-tet cubic Dirichlet instance on the periodic Freudenthal torus.
In the broader gravity stack this sits between the encoded periodic scaffold (Freudenthal triangulation, Regge action correspondence, length-chain endpoint certificates) and the finite-difference Dirichlet action targets. It is bookkeeping rather than new physics: it lets later theorems work in whichever sum shape is convenient without re-proving the mixed hinge-deficit identity. No forcing-chain landmark (T5–T8) is touched directly; the link is through discrete Regge curvature on the cubic lattice limit that feeds the RS gravity sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.