CanonicalPeriodicMixedHingeDeficitExpandedLengthChainTypedSlotTarget
plain-language theorem explainer
Packages the typed slot-guarded expanded mixed hinge-deficit target on the canonical periodic Freudenthal torus: for every vertex potential and periodic edge, the hinge measure times a six-slot guarded Schläfli length-chain equals the squared potential jump scaled by the edge displacement length. Gravity workers cite it when discharging the physical six-tet cubic Dirichlet model on a torus. It is a pure Prop abbreviation, not a proved equality.
Claim. Fix periods $N_x,N_y,N_z\ge 3$. Let $P$ be the canonical encoded periodic Freudenthal torus of those periods. The typed slot target asserts: for every vertex potential $\xi$ on $P$ and every periodic edge $e$, the hinge-measure directional derivative of $\xi$ at $e$, times the negative sum over tetrahedra and six local slots of the Schläfli dihedral derivatives times local edge-length derivatives (retaining only the slot whose typed local edge equals $e$), equals $\sqrt{\mathrm{disp}^2(e)}\,(\xi(v_1)-\xi(v_2))^2$.
background
This module does not claim the physical Dirichlet equality outright. It packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus scaffold.
The underlying complex is the canonical encoded periodic Freudenthal torus $P$ for periods $N_x,N_y,N_z>2$. Edges of $P$ are identified with periodic lattice edges via an edge equivalence; each tetrahedron carries six local edge slots through localEdgeOf, which maps a cell/tet pair and a slot index in $\mathrm{Fin},6$ to a global edge index in the Freudenthal cube triangulation.
The left-hand side is a mixed hinge-deficit expansion: hinge measure directional derivative times a double sum over tets and slots, gated by the typed equality that the periodic edge equals the local edge of that slot, then summing Schläfli dihedral derivatives against local edge-length directional derivatives of the potential. The right-hand side is the standard squared jump of $\xi$ across the edge endpoints, scaled by the Euclidean length of the edge displacement.
proof idea
Definitional packaging only: no proof obligations are discharged. The body binds $P$ to the canonical encoded periodic Freudenthal torus, then states a universal quantification over vertex potentials and periodic edges. For each edge it pulls back via the torus edge equivalence, multiplies the hinge-measure directional derivative by a negated double sum over tets and six slots, and guards each summand by the typed slot equation (edge equals local edge of that tet slot). Surviving terms expand via triangulation Schläfli data and local edge-length directional derivatives. The right-hand side is the displacement-length times squared potential jump at the edge endpoints under the vertex finite equivalence.
why it matters
In the gravity stack this Prop is the typed slot-guarded form of the expanded mixed target, replacing an untyped edge-in-tet test by an explicit six-slot guard. Downstream, the displacement-filtered target implies this slot target; this slot target implies the typed endpoint form of the mixed hinge-deficit expanded length-chain target; and the slot targets feed the canonical local-correspondence endpoint for the periodic edge-stencil Dirichlet action.
Those links are exactly the obligation chain the module advertises for wiring the periodic Freudenthal torus into the physical six-tet cubic Dirichlet model. Within Recognition Science this sits in the discrete gravity / Regge side of the ledger geometry (Freudenthal triangulation, eight-tick compatible cubic lattice), not in the T5–T8 forcing chain itself. Closing the chain would turn the packaged obligations into the physical Dirichlet equality on the torus; this definition only names one intermediate target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.