canonicalPeriodicMixedHingeDeficitExplicitFiberClosedFormPerDispTarget_of_closedForm
plain-language theorem explainer
If the closed-form explicit-fiber mixed hinge-deficit identity holds for every edge on the canonical periodic Freudenthal torus, then its restriction to each fixed positive displacement class d holds as well. Gravity and Regge-lattice workers cite this when specializing the six-tet cubic Dirichlet packaging by displacement. The proof is a short specialization: apply the full target and rewrite via the hinge directional-derivative and fiber-sum identities.
Claim. Fix lattice sizes $N_x,N_y,N_z>2$ and a displacement class $d\in\{0,\ldots,6\}$. Suppose that for every vertex potential $\xi$ and every periodic edge $e$, the mixed hinge-deficit identity holds: the hinge-length directional derivative of $\xi$ along $e$, times the negated closed-form explicit fiber sum over local pairs, equals $\sqrt{\mathrm{disp}^2(e)}$ times the corresponding averaged endpoint contribution. Then the same identity holds whenever one restricts to edges with displacement exactly $d$, with the fiber sum specialized to that class.
background
This module packages the exact theorem 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; it connects the encoded periodic Freudenthal scaffold to the model target.
The ambient geometry is the canonical encoded periodic Freudenthal torus on an $N_x\times N_y\times N_z$ lattice (each side strictly larger than 2). Edges carry a displacement class in seven positive classes. The closed-form mixed target asserts, for every potential $\xi$ and edge, an equality between the hinge-length directional derivative times a negated fiber sum built from freudenthalExplicitFiberPairClosedFormExpandedSummand, and a factor $\sqrt{\mathrm{periodicDispSqEdge}}$ times the matching endpoint average.
The per-displacement target is the same identity restricted to edges with a fixed class $d$. Upstream, the hinge directional derivative is already identified in typed periodic coordinates, and the closed-form fiber sum is known to equal the displacement-indexed fiber.
proof idea
Term-mode specialization. Bind the canonical encoded periodic Freudenthal torus $P$. Introduce a potential $\xi$, an edge, and the hypothesis that the edge has displacement $d$. Instantiate the full closed-form target at $(\xi,\mathrm{edge})$ to obtain the unrestricted identity. Then simpa rewrites both sides into the per-displacement packaging, using: the hinge-measure directional derivative in typed periodic coordinates; equality of the closed-form fiber sum with the displacement-indexed fiber; and the displacement hypothesis. No new algebraic content is proved.
why it matters
In the gravity stack this is a packaging bridge: the full closed-form mixed hinge-deficit obligation implies each of the seven per-class obligations used when the endpoint-only template is unavailable. The per-class target doc records that endpoint-only packaging ($\exists F$ with fiber sum $=F(\xi_0,\xi_1)$) is blocked for $d\in{0,3}$ by the 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$).
No downstream consumers are wired yet (used_by is empty). The lemma sits in the chain that must eventually discharge the physical six-tet cubic Dirichlet instance on the periodic Freudenthal torus, feeding Regge-action and cubic-lattice limit work. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is lattice-geometry scaffolding for the gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.