canonicalPeriodicMixedHingeDeficitExpandedLengthChainTypedEndpointTarget_of_typedSlot
plain-language theorem explainer
On a periodic Freudenthal torus with periods larger than 2, the expanded mixed hinge-deficit length-chain identity in typed endpoint form follows from the same identity written with six-slot guards. Gravity workers packaging the physical six-tet cubic Dirichlet model cite this bridge when they already hold the slot form. The proof equates the two right-hand sides by case analysis on edge-in-tetrahedron incidence, then reapplies the slot hypothesis.
Claim. Let $N_x,N_y,N_z\in\mathbb{N}$ with each period strictly larger than $2$. If the expanded mixed hinge-deficit directional identity holds on the canonical encoded periodic Freudenthal torus of those periods when the tetrahedron sum is written with six-slot guards of the form $\mathrm{edge}=\mathrm{localEdgeOf}(\mathrm{cell},\mathrm{tet},f)$, then the same identity holds when that sum is written via the incidence match on $\mathrm{edgeInTet}$.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it only assembles the theorem-shaped targets that close that instance.
The two props compared here are alternate writings of one expanded mixed target. The endpoint form sums over tetrahedra by matching the global edge against the incidence map edgeInTet (returning a local slot or none). The slot form replaces that match by an explicit sum over the six local edge slots, guarded by the typed equation that the periodic edge equals localEdgeOf of the cell-tet pair at that slot. Both multiply the hinge-measure directional derivative by a signed double sum of Schläfli dihedral derivatives times local edge-length directional derivatives.
Upstream geometry supplies the incidence data: edgeInTet and localEdgeOf from the Freudenthal cube triangulation (and the two-cube strip variant), together with the canonical encoded periodic Freudenthal torus that carries the edge and tet equivalences used to move between periodic edges and internal edge indices.
proof idea
Fix the canonical encoded periodic Freudenthal torus $P$ for the given periods. For an arbitrary vertex potential $\xi$ and periodic edge, transport the edge across $P$'s edge equivalence to an internal index $e$, recording the round-trip identity.
The only real work is a pointwise identity hslot_sum: for each tetrahedron $\tau$, the edgeInTet match that appears in the endpoint RHS equals the six-slot guarded sum from the slot RHS. Case on the incidence option. If none, every slot guard fails (else incidence would return some), so the guarded sum is zero. If some f0, the Finset sum collapses to the single slot $f0$ by uniqueness of the local edge, and that slot's guard holds by the incidence iff lemma; other slots are killed the same way.
With the two RHS writings identified, simpa unfolds both target defs and reapplies the slot hypothesis at $(\xi,\mathrm{edge})$.
why it matters
This is a pure presentation bridge inside the gravity instance stack: it lets later theorems assume the more geometric endpoint writing while discharging obligations that arrive in the typed slot-guarded writing preferred by finite-check and stencil code.
Two parent theorems consume it. canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitTypedSlotTargets builds the canonical local-correspondence endpoint with the mixed target in typed slot-guarded form; canonicalPeriodicEdgeStencilLocalCorrespondence_of_stationary_and_cellTetTargets does the same under the weaker weighted-stationary Schläfli input. Both sit on the path from the encoded periodic Freudenthal scaffold to the physical six-tet cubic Dirichlet model.
In the broader Recognition picture this is infrastructure for the discrete gravity side (Regge-type hinge deficits on the cubic six-tet lattice), not a forcing-chain landmark. It closes no open physical claim by itself; it only removes a bookkeeping mismatch so the Dirichlet-instance obligations can be stated once and reused.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.