CanonicalPeriodicMixedHingeDeficitExplicitFiberClosedFormAllBilinearTarget
plain-language theorem explainer
Packages the claim that every one of the seven displacement classes on a periodic cubic lattice obeys the explicit-fiber bilinear hinge-deficit identity. Gravity and discrete-Regge workers cite it when lifting per-class bilinear targets to a single global obligation. The body is a universal quantifier over Fin 7 applied to the per-displacement bilinear target.
Claim. For lattice sizes $N_x,N_y,N_z\ge 1$ with each dimension strictly larger than $2$, the proposition asserts that for every displacement class $d\in\{0,\ldots,6\}$, the explicit-fiber closed-form mixed-hinge deficit on the canonical periodic torus satisfies the bilinear identity in that class.
background
The module links an encoded periodic Freudenthal torus to the physical six-tet cubic Dirichlet model. It does not freely assert the physical Dirichlet equality; it packages the exact theorem obligations needed to instantiate that model on a periodic Freudenthal scaffold.
Displacement classes index the seven nontrivial axis and diagonal shifts that appear in the mixed-hinge stencil on the cubic lattice. The per-displacement bilinear target is an alias for the explicit-fiber closed-form identity in a single class $d$: the hinge deficit, written in fiber coordinates, matches a bilinear form in the displacement data.
The present definition simply conjoins those seven class-wise identities under a universal quantifier. Lattice sizes must exceed $2$ in each direction so that the periodic stencil has room for the mixed hinges without self-loops or boundary collapse.
proof idea
Definitional abbreviation, not a proved theorem. The right-hand side is $\forall d:\mathrm{Fin},7$, the per-displacement bilinear target at $d$. No tactics or lemmas fire; unfolding yields the seven-fold conjunction of the upstream per-class Prop.
why it matters
Serves as the single hypothesis that the lifting theorem canonicalPeriodicMixedHingeDeficitExplicitFiberClosedFormTarget_of_allBilinear consumes: if all seven bilinear class identities hold, the global explicit-fiber closed-form target follows. A companion negative result shows the same all-bilinear package fails on a concrete axis-displacement witness, so the definition is sharp enough to be refuted on small lattices.
In the broader gravity stack this sits inside the Regge cubic-lattice and Freudenthal-torus pipeline that feeds the physical six-tet Dirichlet model. It is bookkeeping for discrete curvature identities, not a continuum Einstein equation, and does not itself touch the T0–T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.