canonicalPeriodicMixedHingeDeficitLengthChainTarget_of_expanded
plain-language theorem explainer
On a periodic Freudenthal torus with periods larger than 2, the fully expanded mixed hinge-deficit length-chain identity implies the packaged length-chain form that uses the local angle–length chain-rule derivative. Gravity and Regge-calculus workers cite it when moving between expanded Schläfli sums and the compact local-derivative packaging. The proof is a definitional transport: introduce the canonical encoded torus and rewrite both targets via the chain-rule derivative.
Claim. Let $N_x,N_y,N_z\ge 1$ with $N_x,N_y,N_z>2$. If the canonical mixed hinge-deficit identity holds in fully expanded finite-sum form (explicit Schläfli dihedral coefficients times conformal edge-length directional derivatives) on the canonical encoded periodic Freudenthal torus of those periods, then it also holds in length-chain form, where the inner sum is packaged as the local angle–length chain-rule derivative over incident tetrahedron slots.
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 records theorem-shaped targets that close the scaffold.
The ambient complex is the canonical encoded periodic Freudenthal torus for periods $N_x,N_y,N_z>2$. Two sibling targets state the same mixed hinge-deficit first-variation identity at different expansion depths. The length-chain target unfolds the local dihedral package to an explicit sum of the local angle–length chain-rule derivative over incident tet slots. That derivative is the sum, over the six local edges of a tet, of Schläfli dihedral derivatives times conformal local edge-length directional derivatives of a vertex potential.
The expanded target opens that packaging completely, exposing the Schläfli coefficients and edge-length derivatives as a raw finite sum. Both are universal statements over vertex potentials on the torus triangulation.
proof idea
One-line definitional transport. Bind $P$ to the canonical encoded periodic Freudenthal torus for the given periods. For an arbitrary vertex potential $\xi$, rewrite the goal and the hypothesis by unfolding both target Props together with the definition of the local angle–length chain-rule derivative and the bound $P$. The expanded hypothesis at $\xi$ then matches the length-chain goal at $\xi$ by simpa.
why it matters
The bridge lets downstream local-correspondence endpoints accept whichever packaging is convenient. It feeds the canonical edge-stencil local-correspondence theorem that takes the mixed target in fully expanded length-chain form, and the parallel endpoint that uses the weaker weighted-stationary Schläfli input rather than eventual-zero. Those endpoints are the concrete link from the encoded periodic Freudenthal scaffold to the physical six-tet cubic Dirichlet model in this gravity module.
In the broader Recognition gravity stack this sits inside the Regge/cubic-lattice limit path: hinge deficits, Schläfli first variation, and length-chain derivatives must line up before a Dirichlet-type continuum target can be claimed on the lattice. The result is pure packaging hygiene, not a new physical identity, but without it the expanded and compact forms cannot be swapped in the correspondence theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.