CanonicalPeriodicMixedHingeDeficitExplicitFiberFlatUnfoldedTarget
plain-language theorem explainer
Packages the flat-unfolded explicit-fiber mixed hinge-deficit target on the canonical periodic Freudenthal torus: for every vertex potential and every positive-displacement edge, the hinge directional derivative times a signed fiber sum of flat-expanded pair summands equals edge length times squared potential jump. Gravity workers cite it when discharging Dirichlet-model obligations on the six-tet cubic lattice. The body is a pure Prop abbreviation, not a proved equality.
Claim. For lattice sizes $N_x,N_y,N_z>2$, let $P$ be the canonical encoded periodic Freudenthal torus. The flat-unfolded explicit-fiber mixed target asserts: for every vertex potential $\xi$ on $P$ and every positive-displacement periodic edge $e$, $$(\partial_{\mathrm{hinge}}\xi)(e)\cdot\Bigl(-\sum_{\mathrm{pairs\ in\ fiber}} S^{\mathrm{flat}}_{\mathrm{pair}}(\xi,e)\Bigr)=\sqrt{\ell(e)^2}\,(\xi(v_1)-\xi(v_2))^2,$$ where the fiber summands are the flat-expanded explicit-fiber pair terms and $\ell(e)^2$ depends only on the displacement class.
background
The 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 theorem obligations needed to instantiate that model on a periodic torus.
A periodic edge is a base vertex plus one of seven positive cube displacements. Squared edge length is read from the displacement class alone (axis edges length 1, face diagonals $\sqrt{2}$, etc.). The hinge-measure directional derivative is the first variation of the Regge hinge measure along a vertex potential. The fiber over a displacement enumerates local pair contributions; here each contribution is the flat-unfolded expanded summand rather than a closed-form or length-chain form.
Upstream, the canonical encoded torus is built from the endpoint-incidence certificate, and the edge equivalence identifies abstract edges with periodic edges. The dimensionless bridge ratio $K=\varphi^{1/2}$ appears only as the curvature scale carried by the encoded complex.
proof idea
Definitional packaging only: bind $P$ to the canonical encoded periodic Freudenthal torus, then quantify over vertex potentials and periodic edges. For each edge, pull back via the edge equivalence, form the product of the hinge directional derivative with the negated sum of flat-expanded explicit-fiber pair summands over the local displacement fiber, and equate that product to $\sqrt{\mathrm{periodicDispSqEdge}(\mathrm{disp})}$ times the squared potential difference of the two endpoints. No tactics or lemmas are applied; the Prop is the obligation itself.
why it matters
This target is one of the exact obligations the module exposes so that the physical six-tet cubic Dirichlet model can be instantiated on a periodic Freudenthal torus. Downstream, it is equivalent to the expanded length-chain explicit-fiber target, and it inter-reduces with the closed-form explicit-fiber target (each implies the other under the stated size hypotheses). It feeds the local edge-stencil correspondence theorems that assemble weighted deficit stationarity into a Dirichlet-type finite-difference action, and it appears in negative witnesses (e.g. the $N=5$ axis-displacement counterexample) that rule out naive correspondence without the right fiber expansion.
In the broader RS gravity stack this sits under the Regge cubic-lattice limit and the Freudenthal length-chain endpoint certificates: the Dirichlet action is the continuum bridge from discrete hinge deficits to continuum curvature, consistent with the $D=3$ forcing (T8) and the eight-tick geometric scaffolding. It does not itself prove the physical equality; it names the flat-unfolded fiber form that later theorems discharge or refute.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.