canonicalPeriodicMixedHingeDeficitLocalAngleTarget_of_lengthChainTarget
plain-language theorem explainer
On a periodic Freudenthal torus with periods larger than 2, the length-chain form of the mixed hinge-deficit identity implies the local-angle form. Gravity and Regge-calculus workers cite it when switching between the two presentations of the same first-variation target. The proof is a definitional transport: unfold both targets and the local dihedral package, then apply the hypothesis.
Claim. Let $N_x,N_y,N_z\ge 3$. If for every vertex potential $\xi$ the mixed hinge-deficit first variation, written as an explicit length-chain sum of local dihedral derivatives over incident tetrahedra, equals the canonical edge-stencil Dirichlet energy, then the same identity holds when the deficit directional derivative is packaged via local angles rather than the expanded length chain.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it only organizes the theorem-shaped targets that close the instance.
Two sibling propositions express the same mixed hinge-deficit target. The local-angle form asks that, for every vertex potential $\xi$, the sum over edges of hinge-measure directional derivatives times deficitDirectionalDerivFromLocalAngles (built from the canonical local dihedral derivative package) equals the canonical edge-stencil Dirichlet energy. The length-chain form unfolds that package into an explicit finite sum of localAngleLengthChainDeriv contributions over incident tetrahedron slots.
The ambient complex is canonicalEncodedPeriodicFreudenthalTorus, the standard encoded periodic Freudenthal triangulation with periods $N_x,N_y,N_z>2$. The local dihedral package is the canonical one attached to that complex.
proof idea
One-line definitional transport. Bind $P$ to the canonical encoded periodic Freudenthal torus, introduce an arbitrary vertex potential $\xi$, and simpa away the difference between the two target propositions using the definitions of both targets, of deficitDirectionalDerivFromLocalAngles, and of the canonical local dihedral derivative package. The length-chain hypothesis is then exactly the local-angle goal.
why it matters
This is one direction of the equivalence between the length-chain and local-angle presentations of the mixed hinge-deficit target; the sibling iff theorem packages both directions. Downstream, several Track 1.B local-correspondence endpoints consume these targets: the length-chain correspondence endpoint, the stationary-plus-cell-tet endpoint, and the shortest honest stationary-plus-length-chain endpoint. Those endpoints connect the periodic Freudenthal scaffold to the physical six-tet cubic Dirichlet model, which is the gravity-side finite-difference realization of the Dirichlet energy on the cubic lattice. In the broader Recognition chain this sits in the gravity/Regge layer that realizes continuum Dirichlet structure from discrete hinge deficits, not in the T0–T8 forcing core, but it is required infrastructure for the physical cubic instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.