CanonicalPeriodicMixedHingeDeficitExpandedLengthChainDispFilteredTarget
plain-language theorem explainer
Defines the displacement-filtered mixed hinge-deficit target on the canonical periodic Freudenthal torus: after discarding tetrahedral edge slots whose cube displacement differs from the typed edge, the hinge directional derivative times the expanded Schläfli length-chain equals the Dirichlet stencil (edge length times squared potential jump). Gravity workers cite it when reducing typed-slot guards to pure displacement filters. The body is a pure Prop packaging of that filtered equality.
Claim. For lattice sizes $N_x,N_y,N_z\ge 3$, let $P$ be the canonical encoded periodic Freudenthal torus. The displacement-filtered mixed target asserts: for every vertex potential $\xi$ and every periodic edge $e$, the hinge-measure directional derivative of $\xi$ along $e$, multiplied by the negative sum over tets and over those local slots $f$ whose cube-edge displacement equals $e$'s displacement of the Schläfli dihedral derivatives times local edge-length derivatives (zero when the local edge is not $e$), equals $\sqrt{|\mathrm{disp}(e)|^2}\,(\xi(v_1)-\xi(v_2))^2$.
background
This module packages the exact 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. The scaffold is the canonical encoded periodic Freudenthal torus $P$, built from a cubic lattice with six-tetrahedron Freudenthal triangulation per cell and periodic identification.
A mixed hinge-deficit expanded length-chain target equates two sides: (i) the hinge-measure directional derivative of a vertex potential along an edge, times a double sum over tets and local edge slots of Schläfli dihedral derivatives contracted with local edge-length directional derivatives; (ii) a Dirichlet stencil $\sqrt{|\mathrm{disp}|^2}$ times the squared potential jump across the edge endpoints. The typed-slot form still guards by exact local-edge equality. The displacement-filtered form, defined here, first restricts the inner sum to slots whose positive cube-edge displacement matches the typed edge, so mismatched slots cannot contribute.
Upstream geometry supplies localEdgeOf (chosen global edge for each local tet edge slot) and cubeEdgeDisp (displacement of a cube edge), together with the periodic edge type and the vertex-potential space on $P.K$.
proof idea
Definitional packaging only: no proof obligations. The body binds $P$ to the canonical encoded periodic Freudenthal torus, then states a universal quantification over vertex potentials $\xi$ and periodic edges. For each edge it pulls back via $P$'s edge equivalence, multiplies the hinge-measure directional derivative by a filtered double sum (tets $\times$ Fin-6 slots whose cubeEdgeDisp matches the edge displacement, with an inner edge-equality guard that zeros non-matching local edges), and equates the product to the Dirichlet right-hand side built from periodicDispSqEdge and the squared potential difference at the edge endpoints.
why it matters
This Prop is the middle rung in a three-step reduction of the mixed hinge-deficit target toward the physical Dirichlet model. Downstream, canonicalPeriodicMixedHingeDeficitExpandedLengthChainTypedSlotTarget_of_dispFiltered lifts a proof of this displacement-filtered form to the typed-slot-guarded form; canonicalPeriodicMixedHingeDeficitExpandedLengthChainDispFilteredTarget_of_baseDisp discharges it from a still coarser base-and-displacement filter; and canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitDispFilteredTargets uses the filtered family as the mixed-target hypothesis in the canonical local-correspondence endpoint.
In the Recognition gravity stack the goal is to identify the Regge-style hinge deficit action on the six-tet cubic lattice with a discrete Dirichlet energy, so that continuum limits recover Newtonian gravity from the RS length-chain and $K=\varphi^{1/2}$ bridge. Packaging the displacement filter as a named target keeps the obligation chain explicit and auditable rather than burying slot bookkeeping inside a single monolithic theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.