canonicalPeriodicMixedHingeDeficitExpandedLengthChainDispFilteredTarget_of_baseDisp
plain-language theorem explainer
On a periodic Freudenthal torus with periods larger than 2, the displacement-filtered mixed hinge-deficit target follows from its base-and-displacement-filtered sibling. Anyone wiring expanded length-chain data into the physical six-tet cubic Dirichlet model would cite this bridge. The proof equates the typed edge-equality guard with a periodic base-offset equation once displacements already match, then rewrites the hypothesis.
Claim. Let $N_x,N_y,N_z>2$ be positive integers. If the expanded mixed hinge-deficit length-chain identity holds on the canonical encoded periodic Freudenthal torus after filtering local slots by edge displacement and replacing the remaining edge-equality guard by a periodic base-offset equation, then the same identity holds with the original typed edge-equality guard under displacement filtering alone.
background
The 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: a six-tetrahedra-per-cube triangulation of a discrete 3-torus with periods $N_x,N_y,N_z>2$.
Mixed hinge-deficit targets relate the directional derivative of hinge measure along a vertex potential $\xi$ to a double sum, over tetrahedra and local edge slots, of Schläfli dihedral derivatives times local edge-length directional derivatives. Displacement filtering drops any local slot whose cube-edge displacement differs from the typed periodic edge under study.
The base-and-displacement form goes one step further. After the displacement filter, the remaining guard that the typed edge equals the local edge of a tet is rewritten as equality of the edge base with a periodic vertex-bit offset of the cube-edge base (addVertexBits of cubeEdgeBase). The two target Props differ only in that guard.
proof idea
Fix the canonical encoded periodic Freudenthal torus $P$ and an arbitrary vertex potential $\xi$ with typed periodic edge. For each tetrahedron index $\tau$ and each displacement-matching local slot $f$, prove the biconditional
edge $=$ localEdgeOf(...) $\iff$ edge.base $=$ addVertexBits(..., cubeEdgeBase(...))
using canonicalPeriodicTypedEdge_base_eq_of_localEdgeOf one way and canonicalPeriodicTypedEdge_eq_localEdgeOf_iff_base_and_disp the other (displacement is already in the filter). Case-split on the base equation, simplify both sides of the filtered sum via Finset.sum_congr, then simpa the hypothesis through the two target unfoldings.
why it matters
This is a pure guard-rewriting step inside the gravity instance chain. Downstream, canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitBaseDispTargets ("Canonical local-correspondence endpoint with the mixed target in base-and-displacement-filtered form") and canonicalPeriodicEdgeStencilLocalCorrespondence_of_stationary_and_cellTetTargets (weaker weighted-stationary Schläfli input) consume the base-disp form when building local edge-stencil correspondence for the physical Dirichlet model. Closing the gap between the two filtered presentations lets those endpoints accept whichever form is easier to discharge from Schläfli or length-chain data.
In the Recognition Science gravity stack this sits under the Regge-action / cubic-lattice limit path: discrete curvature on the Freudenthal six-tet complex must match a finite-difference Dirichlet action before continuum identification. It does not itself force $D=3$ or the eight-tick octave; those enter earlier via the forcing chain and the torus construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.