canonicalPeriodicMixedHingeDeficitExpandedLengthChainPerEdgeTarget_of_typed
plain-language theorem explainer
On the canonical encoded periodic Freudenthal torus with periods larger than 2, the expanded mixed hinge-deficit length-chain identity for typed periodic edges implies the same identity for anonymous Fin-indexed edges. Gravity and discrete-Regge workers cite this when packaging the six-tet cubic Dirichlet local correspondence. The proof is a one-line reindexing through the torus edge equivalence.
Claim. Fix periods $N_x,N_y,N_z>2$. Let $P$ be the canonical encoded periodic Freudenthal torus of those periods. If for every vertex potential $\xi$ and every typed periodic edge the expanded mixed hinge-deficit length-chain identity holds (hinge-measure directional derivative times the signed tet sum along the length chain), then the same identity holds for every $\xi$ and every edge index $e\in\mathrm{Fin}\,n_E(P)$.
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; it only connects the encoded periodic scaffold to the model target.
The per-edge target is the finite local identity that remains before summing over global edges: for each potential $\xi$ and each edge $e$, the hinge-measure directional derivative multiplies a signed sum over tets incident to $e$ in the expanded length-chain form of the mixed hinge deficit. The typed-edge target is the same identity, but quantified over PeriodicEdge rather than anonymous Fin nE indices, so the remaining local statement is free of opaque edge numbering.
Both targets are stated on the canonical encoded periodic Freudenthal torus $P$ built from the endpoint-incidence data for periods strictly larger than 2. The torus supplies an edge equivalence between typed periodic edges and Fin nE.
proof idea
Bind $P$ to the canonical encoded periodic Freudenthal torus. Introduce a potential $\xi$ and an anonymous edge index $e$. Apply the typed-edge hypothesis at $\xi$ and at the typed edge $P.\mathrm{edgeEquiv},e$, then simplify with the definition of $P$. The two Prop bodies differ only by that reindexing, so the implication is pure transport along the edge equivalence.
why it matters
The theorem is the last bookkeeping step that turns a typed periodic-edge mixed-deficit identity into the Fin-indexed per-edge form used by the stencil machinery. Downstream, canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitTypedEdgeTargets builds the canonical local-correspondence endpoint with the mixed target reduced to a typed periodic-edge finite identity; the companion ..._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, i.e. the discrete gravity side of the Recognition lattice (Regge-type hinge deficits on the cubic six-tet decomposition). Without this transport, typed and Fin-indexed formulations of the expanded length-chain target would remain formally disconnected.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.