CanonicalPeriodicMixedHingeDeficitExpandedLengthChainTypedEdgeTarget
plain-language theorem explainer
Defines the typed periodic-edge form of the expanded mixed hinge-deficit identity on the canonical encoded periodic Freudenthal torus. For every vertex potential and every lattice edge, the hinge-measure directional derivative times the Schläfli-weighted length derivatives equals the squared potential jump scaled by the edge length. Gravity workers cite it when discharging the local per-edge obligation of the physical six-tet cubic Dirichlet model. It is a pure Prop packaging, not a proved equality.
Claim. For lattice sizes $N_x,N_y,N_z\ge 3$, let $P$ be the canonical encoded periodic Freudenthal torus. The typed expanded mixed target asserts: for every vertex potential $\xi$ and every periodic edge $e$, $$\mu_{\mathrm{hinge}}'(P,\xi;e)\cdot\Bigl(-\sum_{\tau}\sum_k \partial_{\mathrm{dih}}\theta_{\tau,f}(k)\,\partial_{\ell}\ell_{\tau,k}(\xi)\Bigr)=\sqrt{\ell^2(e)}\,(\xi(v_1)-\xi(v_2))^2,$$ where the inner sum runs only over tets incident to $e$, and $(v_1,v_2)$ are the endpoints of $e$.
background
The module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not claim the Dirichlet equality outright; it packages the exact obligations needed to instantiate that model on a periodic torus with six-tetrahedron cubic triangulation.
A vertex potential $\xi$ assigns a real value to each lattice vertex. Edges are typed as periodic lattice edges rather than anonymous Fin nE indices, so the identity is stated directly in geometric coordinates. The left-hand side is the first variation of the mixed hinge deficit: the hinge measure directional derivative multiplies a Schläfli chain that contracts dihedral-angle derivatives against local edge-length derivatives of $\xi$. The right-hand side is the squared potential jump across the edge, scaled by the Euclidean edge length $\sqrt{\ell^2(e)}$.
Upstream geometry supplies the triangulation incidence data, the global squared edge lengths, and the encoded torus construction under the size hypotheses $N_i>2$.
proof idea
Definitional Prop abbreviation. The body builds the canonical encoded periodic Freudenthal torus $P$, then states a universal quantifier over vertex potentials and typed periodic edges. For each edge it pulls back via the edge equivalence, expands the mixed hinge deficit through the triangulation Schläfli data and local length derivatives, and equates that product to the squared endpoint jump of $\xi$ times $\sqrt{\ell^2(e)}$. No tactics or lemmas are applied; the declaration only names the obligation.
why it matters
This Prop is the typed-edge form of the expanded mixed target that the physical six-tet cubic Dirichlet instance must discharge. Downstream, canonicalPeriodicMixedHingeDeficitExpandedLengthChainPerEdgeTarget_of_typed lifts it to the per-edge (still expanded) target, and canonicalPeriodicMixedHingeDeficitExpandedLengthChainTypedEdgeTarget_of_typedEndpoint derives it from the typed-endpoint variant. The local-correspondence theorem canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitTypedEdgeTargets then uses the typed deficit targets to obtain the canonical edge-stencil correspondence.
In the broader RS gravity stack this sits inside the Regge-to-Dirichlet bridge on the periodic Freudenthal lattice: matching the mixed hinge variation to a pure squared finite-difference jump is the discrete precursor of the continuum Dirichlet energy. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; those enter only through the ambient constants and dimension choices of the lattice model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.