canonicalPeriodicMixedHingeDeficitExpandedLengthChainTarget_of_perEdge
plain-language theorem explainer
If the expanded mixed hinge-deficit identity holds edgewise on the canonical periodic Freudenthal torus, it holds after summing over all global edges. Gravity and Regge-calculus workers cite this when lifting local Schläfli/length-chain checks to the global Dirichlet target. The proof is a one-line Finset sum congruence from the per-edge hypothesis.
Claim. Let $N_x,N_y,N_z\ge 3$. Write $P$ for the canonical encoded periodic Freudenthal torus of those sizes. If for every vertex potential $\xi$ and every global edge $e$ the expanded mixed hinge-deficit length-chain identity holds at $e$, then for every $\xi$ the same identity holds after summing over all global edges of $P$.
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.
The ambient complex is the canonical encoded periodic Freudenthal torus $P$ (sizes $N_x,N_y,N_z$ with each dimension at least 3). Vertex potentials $\xi$ live on its 0-skeleton. The mixed hinge-deficit expanded length-chain target equates, after expansion, a sum of hinge-measure directional derivatives times local Schläfli and conformal edge-length derivative coefficients to the canonical edge-stencil Dirichlet energy $$\sum_e \sqrt{\ell_e^2},(\xi_{u(e)}-\xi_{v(e)})^2.$$
The per-edge variant is the same finite local identity before the global edge sum. The global target is literally that sum over $e\in\mathrm{Fin},n_E$.
proof idea
Fix the canonical encoded periodic Freudenthal torus $P$. The goal is the universal quantification over vertex potentials $\xi$ of an equality of two finite sums over global edges. Introduce $\xi$, then apply Finset.sum_congr with reflexive index equality and the per-edge hypothesis at $(\xi,e)$ on each summand. A simpa closes the identification with the canonical edge-stencil Dirichlet energy expression. No geometric content beyond summation is used.
why it matters
In the gravity stack this is the bookkeeping step that turns a local (per-edge) expanded mixed hinge-deficit check into the fully summed target required by the physical six-tet cubic Dirichlet instance.
It is consumed by two local-correspondence endpoints: one that reduces the mixed target to a per-edge expanded finite identity under an eventual-zero weighted-deficit hypothesis, and one that uses the weaker weighted-stationary Schläfli input together with cell-tet targets. Both sit on the path from the periodic Freudenthal scaffold to the physical Dirichlet model on the cubic lattice.
Within Recognition Science this supports the discrete geometric side of the gravity sector (Regge-type action on the eight-tick / $D=3$ lattice), not the T5–T8 forcing chain itself. It closes no open physical claim; it only packages summation so downstream correspondence theorems can quote a single global Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.