canonicalPeriodicMixedHingeDeficitExpandedLengthChainBaseDispCellTetTarget_of_localPair
plain-language theorem explainer
If the mixed hinge-deficit length-chain identity holds in local-pair collapsed form on the canonical periodic Freudenthal torus, it holds in the expanded cell-by-tetrahedron product-split form. Discrete-Regge and gravity workers cite this when lifting a collapsed stencil identity back to the full cell sum. The proof equates the two sum shapes by base-offset uniqueness, then applies the local-pair hypothesis.
Claim. Let $N_x,N_y,N_z>2$ be positive integers. On the canonical encoded periodic Freudenthal torus of those periods, if the mixed hinge-deficit expanded length-chain identity holds after each periodic cell sum is collapsed to the unique cell solving the base-offset equation for every local tetrahedron-face pair, then the same identity holds when written as an explicit double sum over lattice cells and the six local tetrahedra of the Freudenthal cube triangulation.
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: a cubic lattice torus of periods $N_x,N_y,N_z>2$, triangulated by six tetrahedra per cube, with edges and tets identified via the standard Freudenthal local-edge table and bit-offset vertex arithmetic. The dimensionless bridge ratio $K=\varphi^{1/2}$ enters the Schläfli and length-derivative data on each tet.
Two sibling targets record the same mixed hinge-deficit identity at different sum granularities. The base/displacement cell-tet target expands the sum over periodic tets as an explicit cell sum times a local six-tet sum, filtered by cube-edge base and displacement. The local-pair target is the same statement after the cell sum has already been collapsed to the unique cell solving the base-offset equation for each local pair.
proof idea
Classical proof. Fix the canonical encoded periodic torus $P$, a vertex potential $\xi$, and a periodic edge. The only work is a finite-sum collapse: the triple sum over cells, local tets, and displacement-matching faces, with an if that keeps the Schläfli-dihedral times length-directional-derivative term only when the edge base equals the bit-offset cube-edge base, equals the double sum over tets and matching faces evaluated at the unique matching cell from periodicMatchingBaseCell.
That equality is obtained by commuting the cell and tet sums, then applying the add-vertex-bits ite summation lemma facewise. After rewriting by the collapse, the goal is exactly the local-pair target, which is the hypothesis.
why it matters
This is a bookkeeping bridge inside the physical six-tet cubic Dirichlet instance: it lets later theorems assume the more convenient local-pair form of the mixed hinge-deficit identity and still discharge the expanded cell-tet form required by the typed product-split target.
Its sole recorded consumer is the canonical periodic edge-stencil local-correspondence theorem built from canonical deficit local-pair targets, which packages the local-correspondence endpoint once the mixed target is reduced to the local-pair displacement-filtered form. That sits on the path from the encoded periodic Freudenthal scaffold and Regge cubic-lattice limit infrastructure toward the physical Dirichlet model, without yet claiming the free physical equality.
In the broader Recognition gravity stack this is geometry-side scaffolding for discrete curvature on the eight-tick cubic lattice, not a forcing-chain (T0-T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.