CanonicalPeriodicMixedHingeDeficitExplicitFiberClosedFormPerDispTarget
plain-language theorem explainer
For each of the seven positive lattice displacement classes on a periodic Freudenthal torus (grid sizes >2), this packages the pointwise mixed identity equating the closed-form explicit-fiber sum, weighted by the average endpoint potential, to the squared endpoint potential jump (times the geometric edge-length factor). Regge/gravity workers instantiating the six-tet cubic Dirichlet model cite it as the per-class hinge-deficit target. It is a pure Prop definition: no proof content.
Claim. Fix $N_x,N_y,N_z>2$ and a positive displacement class $d\in\{0,\ldots,6\}$. Write $P$ for the canonical encoded periodic Freudenthal torus on that grid. The target asserts: for every vertex potential $\xi$ on $P$ and every periodic edge $e$ of class $d$, $$\sqrt{\ell_d^{2}}\cdot\frac{\xi(v_0)+\xi(v_1)}{2}\cdot\bigl(-\Sigma_{\mathrm{fiber}}(\xi,e,d)\bigr)=\sqrt{\ell_d^{2}}\cdot\bigl(\xi(v_0)-\xi(v_1)\bigr)^{2},$$ where $v_0,v_1$ are the endpoints of $e$, $\ell_d^{2}$ is the squared lattice length of class $d$, and $\Sigma_{\mathrm{fiber}}$ is the closed-form explicit-fiber sum along $e$.
background
The ambient module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not assert the physical Dirichlet equality for free; it packages the exact obligations needed to instantiate that model on a periodic torus.
A vertex potential is a real assignment to torus vertices. Periodic edges are typed by one of seven positive displacement classes (axis, face-diagonal, space-diagonal). Each class carries a fixed squared lattice length $\ell_d^{2}$. The closed-form explicit-fiber sum $\Sigma_{\mathrm{fiber}}$ is the length-chain contribution along the fiber of a typed edge; it is $\mathbb{R}$-linear in the potential.
The pure endpoint packaging (existence of $F:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ with fiber sum $=F(\xi_0,\xi_1)$) is blocked for axis and selected face-diagonal classes: the vertex expansion plus a finite coefficient audit leave nonzero interior coefficients, and at $(\xi_0,\xi_1)=(1,1)$ the fiber sum is $-4$ while any such $F$ is forced to vanish on the diagonal. The global mixed length-chain target (sum over edges) is the intended load-bearing replacement.
proof idea
Definitional packaging only: the body introduces the canonical encoded periodic Freudenthal torus for the given grid bounds, then states a universal Prop over vertex potentials and periodic edges of fixed displacement class $d$. Both sides of the asserted equality are written out explicitly (geometric length factor, average or difference of the two endpoint potentials, and the closed-form explicit-fiber sum). No tactics, no lemmas applied, no sorry.
why it matters
This is the per-displacement-class mixed hinge-deficit obligation used throughout the six-tet cubic Dirichlet instance. Downstream it is aliased as the bilinear per-disp target, recovered from bilinear-endpoint and closed-form hypotheses, and fed into the edge-stencil local-correspondence theorems (including a negative witness that the closed-form per-disp target fails at a concrete axis witness). It sits between the length-chain finite-sum form of the canonical mixed hinge-deficit target and the physical finite-difference Dirichlet action on the periodic torus.
Within Recognition gravity, the Freudenthal triangulation and Regge-style hinge measures are the discrete bridge toward continuum Dirichlet energy; this definition isolates the combinatorial identity that would make the explicit-fiber sum behave like a pure endpoint quadratic. The doc-comment flags that the pointwise endpoint-quadratic ansatz is not the load-bearing path for axis classes: the global mixed length-chain target is. The remaining open work is a Lean certificate of the audited cancellations, or a revised target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.