CanonicalPeriodicMixedHingeDeficitExpandedLengthChainBaseDispFilteredTarget
plain-language theorem explainer
Defines the base-and-displacement-filtered expanded mixed hinge-deficit target on the canonical periodic Freudenthal torus of size Nx×Ny×Nz. For every vertex potential and every periodic edge, the hinge directional derivative times a filtered Schläfli length-chain sum equals the squared potential jump scaled by the edge displacement length. Gravity workers cite it when discharging the physical six-tet cubic Dirichlet model. The body is a pure Prop packaging of that equality.
Claim. Fix lattice sizes $N_x,N_y,N_z\ge 3$. Let $P$ be the canonical encoded periodic Freudenthal torus of those sizes. The target asserts: for every vertex potential $\xi$ on $P$ and every periodic edge $e$, the product of the hinge-measure directional derivative of $\xi$ along $e$ with the negative sum (over tetrahedra and local faces whose cube-edge displacement matches $e$'s displacement, and whose base matches the periodic base offset) of Schläfli dihedral derivatives times local edge-length directional derivatives equals $\sqrt{|\mathrm{disp}(e)|^2}\,(\xi(v_1)-\xi(v_2))^2$.
background
The module packages exact obligations that turn the encoded periodic Freudenthal torus into an instance of the physical six-tet cubic Dirichlet model. It does not claim the Dirichlet equality outright; it names the intermediate targets that must be proved.
The scaffold $P$ is canonicalEncodedPeriodicFreudenthalTorus: a periodic triangulation built from the Freudenthal cube decomposition (six tets per cube) with edge and tet equivalences into a global complex. Vertex potentials are real functions on the torus vertices. Hinge-measure and local edge-length directional derivatives, together with the triangulation Schläfli data (dihedral derivatives), form the expanded mixed length-chain side of the identity.
localEdgeOf chooses, for each tet and each of its six edge slots, a global cube-edge representative. The displacement filter keeps only faces whose cube-edge displacement equals the periodic edge's displacement; the remaining guard is a periodic base-offset equation via addVertexBits. The right-hand side is the standard squared jump of $\xi$ across the edge endpoints, scaled by the Euclidean length of the displacement.
proof idea
No proof: this is a definition of a Prop. The body introduces the canonical torus $P$, then states a universal quantification over vertex potentials and periodic edges. For each edge it pulls back via $P$'s edge equivalence, builds the filtered double sum over tets and local faces (displacement match, then base-offset match), multiplies by the hinge directional derivative, and equates the result to the scaled squared potential jump. Downstream theorems discharge or transport this Prop; the definition itself only names the obligation.
why it matters
This is the base-and-displacement-filtered form of the expanded mixed target on the physical six-tet cubic lattice. Downstream, canonicalPeriodicMixedHingeDeficitExpandedLengthChainDispFilteredTarget_of_baseDisp lifts it to the displacement-only filtered target, and canonicalPeriodicMixedHingeDeficitExpandedLengthChainBaseDispFilteredTarget_of_typedTet relates it to the typed-tet form that removes anonymous tet indices. The local-correspondence endpoint canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitBaseDispTargets consumes the mixed target in this filtered shape.
In the Recognition gravity stack these targets are the exact bridge from discrete Regge/Schläfli calculus on the periodic Freudenthal torus to the continuum Dirichlet (finite-difference) action. Closing them is required before the physical six-tet cubic Dirichlet model can be instantiated; the module explicitly refuses to assert that equality for free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.