CanonicalPeriodicMixedHingeDeficitExpandedLengthChainExplicitFiberAngleChainTarget
plain-language theorem explainer
Defines the angle-chain form of the mixed hinge-deficit / expanded length-chain target on the canonical periodic Freudenthal torus. For every vertex potential and every positive-displacement periodic edge, the hinge-measure directional derivative times a signed sum of local angle-length chain derivatives equals edge length times squared potential jump. Gravity workers cite it when discharging the physical six-tet cubic Dirichlet instance. The body is a pure Prop packaging, not a proof.
Claim. Fix grid sizes $N_x,N_y,N_z\ge 3$. Let $P$ be the canonical encoded periodic Freudenthal torus on that grid. The angle-chain mixed target asserts: for every vertex potential $\xi$ and every positive-displacement periodic edge $e$, $$(\partial_{\mathrm{hinge}}\xi)(e)\cdot\Bigl(-\sum_{\mathrm{pairs\ in\ fiber}}\partial_{\mathrm{angle\text{-}length}}\xi\Bigr)=\sqrt{\ell(e)^2}\,(\xi(v_+)-\xi(v_-))^2,$$ where the sum runs over the explicit Freudenthal local pair-displacement fiber of $e$'s displacement class, and $v_\pm$ are the edge endpoints.
background
The module packages 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.
The scaffold is the canonical encoded periodic Freudenthal torus $P$ on an $N_x\times N_y\times N_z$ lattice with each side strictly larger than 2. Periodic edges are positive-displacement edges: a base vertex plus one of seven cube displacements, with squared length $1$ or $2$ read from the displacement class alone. Vertices are indexed by a canonical finite equivalence.
Two first-variation ingredients appear: the hinge-measure directional derivative of the Regge-type action in the potential $\xi$, and the local angle-length chain derivative along selected tetrahedra in the explicit fiber over each displacement. The dimensionless bridge ratio $K=\varphi^{1/2}$ enters only as the curvature scale carried by $P$.
proof idea
No proof: this is a def whose body is a Prop. It binds $P$ to the canonical encoded periodic Freudenthal torus, then states a universal equality over vertex potentials and periodic edges. The left-hand side multiplies the hinge-measure directional derivative by the negated sum of local angle-length chain derivatives over the Freudenthal local pair-displacement fiber; the right-hand side is $\sqrt{\texttt{periodicDispSqEdge}}$ times the squared potential jump at the edge endpoints via the vertex finite equivalence. Downstream lemmas treat inhabiting this Prop as a hypothesis.
why it matters
This is the angle-chain packaging of the explicit-fiber mixed hinge-deficit target on the periodic scaffold. Downstream, ...Target_of_angleChain converts an angle-chain witness into the explicit-fiber mixed target, while ...AngleChainTarget_of_explicit runs the converse direction; both feed canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitExplicitFiberAngleChainTargets, which ties weighted deficit stationarity to the local edge-stencil Dirichlet correspondence.
In the gravity stack this is one of the exact theorem obligations that close the gap between the encoded periodic Freudenthal geometry and the physical six-tet cubic Dirichlet model. It sits in the discrete Regge / finite-difference route toward continuum Dirichlet energy on the cubic lattice, not in the T0-T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.