CanonicalPeriodicMixedHingeDeficitExplicitFiberClosedFormPerDispBilinearTarget
plain-language theorem explainer
Definitional alias that names the per-displacement explicit-fiber mixed hinge-deficit identity as a bilinear target on the canonical periodic Freudenthal torus. Gravity and discrete-Regge workers cite it when packaging axis, face-diagonal, and body-diagonal fiber identities. The body is a pure rename of the existing per-displacement closed-form target; no new proof content.
Claim. For lattice sizes $N_x,N_y,N_z>2$ and displacement class $d\in\{0,\ldots,6\}$, the proposition that every edge of class $d$ on the canonical periodic Freudenthal torus has mixed hinge deficit admitting an explicit-fiber closed form bilinear in the two endpoint vertex potentials.
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 give the physical Dirichlet equality for free; it only names the theorem-shaped targets that would complete the instance.
The underlying per-displacement target asserts: on the canonical encoded periodic Freudenthal torus $P$, for every vertex potential $\xi$ and every periodic edge of fixed positive-displacement class $d$, the mixed hinge deficit along that edge admits an explicit-fiber closed form. Upstream notes that a pure endpoint-only packaging $\exists F:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ with fiber sum $=F(\xi_0,\xi_1)$ is blocked for $d\in{0,3}$ by the proved vertex expansion and a finite audit (interior coefficients do not vanish; at $(1,1)$ the fiber sum is $-4$ while the template forces $F(1,1)=0$).
Calling the target bilinear records the intended algebraic shape of that closed form: a bilinear expression in the two endpoint potentials along the edge.
proof idea
Pure definitional alias. The body applies the existing per-displacement explicit-fiber closed-form mixed target to the same lattice sizes, nondegeneracy hypotheses $N_x,N_y,N_z>2$, and displacement index $d$. No tactics, no lemmas, no reduction.
why it matters
Gives a stable name for the bilinear packaging of one displacement class so that coarser targets can quantify over classes cleanly. Downstream, the three-class target is the conjunction of this proposition at the axis, face-diagonal, and body-diagonal representatives; the all-class target is the universal quantification over all seven displacement classes in $\mathrm{Fin},7$.
Those aggregators sit inside the obligation stack that would connect the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model and, further out, to the Regge cubic-lattice limit and nonlinear Regge-action correspondence imported by the module. In the Recognition gravity line this is bookkeeping toward a discrete Dirichlet energy on the eight-tick / $D=3$ lattice geometry, not a new continuum claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.