CanonicalPeriodicMixedHingeDeficitLengthChainTarget
plain-language theorem explainer
Packages the mixed hinge-deficit identity on the canonical periodic Freudenthal torus as an explicit length-chain finite-sum Prop: for every vertex potential, the edge-sum of hinge-measure directional derivatives times the negative tet-slot sum of local-angle length-chain derivatives equals the canonical edge-stencil Dirichlet energy. Gravity/Regge workers cite it when discharging Track 1.B local-correspondence and mixed-target packaging. It is a pure Prop definition, not a proved equality.
Claim. For integers $N_x,N_y,N_z>2$, let $P$ be the canonical encoded periodic Freudenthal torus of those sizes. The length-chain mixed hinge-deficit target asserts: for every vertex potential $\xi$ on $P$, $$\sum_e \partial_{\mathrm{hinge}}(\xi,e)\cdot\Bigl(-\sum_{\tau\ni e}\partial_{\mathrm{loc\text{-}ang,\,\ell\text{-}chain}}(\xi,\tau,f_{e\tau})\Bigr)=E_{\mathrm{edge\text{-}stencil}}(\xi),$$ where the inner sum runs over tetrahedra incident to edge $e$ via the incidence map, and the right-hand side is the canonical edge-stencil Dirichlet energy.
background
This module ties the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not give the physical Dirichlet equality for free; it packages the exact theorem obligations needed to instantiate that model on a periodic Freudenthal complex.
A hinge deficit is $2\pi-\sum\theta$ over dihedral angles at the hinge. The incidence map edgeInTet sends a global edge and tetrahedron index to a local edge slot when the edge belongs to that tet (six tets per Freudenthal cube). The length-chain form unfolds the local dihedral derivative package into an explicit sum of local-angle length-chain derivatives over those incident slots.
The left-hand side is therefore a mixed quadratic: hinge-measure directional derivatives paired against length-chain angle derivatives. Session 202 finite audits show this mixed length-chain quadratic matches the rational axis stencil, not the older full seven-class square-root edge stencil.
proof idea
No proof: the declaration is a def of a Prop. It binds $P$ to the canonical encoded periodic Freudenthal torus at the given sizes (with $N_i>2$), then states a universal quantification over vertex potentials equating the mixed hinge/length-chain double sum to the canonical edge-stencil Dirichlet energy. Downstream lemmas convert this form to/from the local-angle target and the expanded length-chain target by rewriting the summands.
why it matters
This is the corrected Session 202 mixed hinge-deficit target in length-chain finite-sum form. It is the obligation fed into the shortest honest Track 1.B local-correspondence endpoint (second-order Schläfli stationarity plus this global length-chain mixed identity) and into the canonical local-correspondence endpoint that keeps the mixed target as an explicit length-chain sum.
Equivalence and introduction lemmas relate it to the local-angle and expanded length-chain variants; the $N=5$ abbreviation specializes it for certificate-scale packaging. It also appears in the Track 1.B closure target bundle. In the broader RS gravity stack this is discrete Regge/Dirichlet scaffolding on the eight-tick / $D=3$ cubic lattice side, not a continuum Einstein equation. The $N=5$ surface is flagged as wrong-weighted by the Session 202 audit; packaging theorems still route through this name while the corrected mixed/Hessian target is named separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.