CanonicalPeriodicMixedHingeDeficitExpandedLengthChainLocalPairTarget
plain-language theorem explainer
Packages the local-pair form of the mixed hinge-deficit / expanded length-chain target on the canonical periodic Freudenthal torus: for every vertex potential and periodic edge, the hinge directional factor times a base-offset-filtered sum of dihedral–length chain terms equals the edge length scale times the squared potential jump. Gravity workers cite it when collapsing the mixed Regge target to unique matching cells. Pure Prop definition; no equality is proved here.
Claim. For lattice sizes $N_x,N_y,N_z>2$, let $P$ be the canonical encoded periodic Freudenthal torus. The local-pair mixed target asserts: for every vertex potential $\xi$ and every periodic edge $e$ with displacement $d$ and endpoints $(v_1,v_2)$, $$\partial_{\mathrm{hinge}}(\xi,e)\cdot\Bigl(-\sum_{\mathrm{tet},f:\,d=\mathrm{disp}(\mathrm{localEdge}(\mathrm{tet},f))}\sum_k \partial_{\mathrm{dih}}\,\partial_{\ell}\Bigr)=\sqrt{|d|^2}\,(\xi(v_1)-\xi(v_2))^2,$$ where each summand uses the unique periodic matching base cell solving the base-offset equation for that local pair.
background
This module ties the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not give the physical Dirichlet equality for free; it packages the exact obligations needed to instantiate that model on a periodic torus.
The geometry is the six-tetrahedron Freudenthal triangulation of the unit cube. localEdgeOf assigns, for each tet and each of its six edge slots, a global edge representative in the cube graph. Periodic edges carry a base cell and a displacement; the matching-base-cell construction collapses a full periodic cell sum to the unique cell solving the base-offset equation for a given local pair.
Upstream, the continuum bridge identifies a weighted graph Laplacian on vertex potentials with a hinge-deficit action: $\tfrac12\sum_{i\sim j}w_{ij}(\varepsilon_i-\varepsilon_j)^2=\tfrac1\kappa\sum_h\delta_h A_h$. The mixed target here is the differentiated, length-chain expanded form of that correspondence, restricted to one edge at a time.
proof idea
Definitional packaging only: the body is a let binding of the canonical encoded periodic Freudenthal torus, followed by a universal Prop over vertex potentials and periodic edges. The left-hand side multiplies the hinge-measure directional derivative by a double sum over the six tets and those local faces whose cube-edge displacement matches the edge, then over the six length slots, of dihedral derivative times local edge-length directional derivative (Schläfli data of the matched cell-tet). The right-hand side is $\sqrt{\mathrm{disp}^2}$ times the squared potential jump at the edge endpoints. No tactics or lemmas are invoked.
why it matters
This is the collapsed local-pair obligation inside the physical six-tet cubic Dirichlet instance. Downstream, canonicalPeriodicMixedHingeDeficitExpandedLengthChainBaseDispCellTetTarget_of_localPair lifts it to the full base/displacement/cell/tet expanded target; canonicalPeriodicMixedHingeDeficitExpandedLengthChainLocalPairTarget_of_fiber derives it from the explicit Freudenthal-local-pair fiber form; and canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitLocalPairTargets uses it as the mixed-target hypothesis in the canonical local-correspondence endpoint (edge-stencil Dirichlet correspondence under weighted-deficit stationarity).
In the Recognition gravity stack this sits on the discrete-to-continuum bridge from Regge hinge deficits on the periodic Freudenthal lattice toward the physical finite-difference Dirichlet action. It does not itself close the Dirichlet equality; it is one of the named theorem-shaped obligations the module isolates so the physical model can be instantiated without hidden gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.