CanonicalPeriodicLocalEdgeNoDup
plain-language theorem explainer
Injectivity of local tetrahedral edge slots on the periodic Freudenthal torus: within any cubic cell and any of the six Freudenthal tets, distinct local edge indices map to distinct translated periodic edges. Encoding lemmas cite this to invert the local-to-global edge assignment when building a finite triangulation. Pure Prop definition; the companion theorem discharges it by Fin-case analysis on the cube table.
Claim. For positive integers $N_x,N_y,N_z$, the following holds as a proposition: for every periodic cubic vertex $\mathrm{cell}\in(\mathbb{Z}/N_x)\times(\mathbb{Z}/N_y)\times(\mathbb{Z}/N_z)$, every Freudenthal tetrahedron index $t\in\{0,\ldots,5\}$, and every pair of local edge slots $f,g\in\{0,\ldots,5\}$, if the translated global periodic edges of $(t,f)$ and $(t,g)$ coincide then $f=g$.
background
The module isolates a typed periodic Freudenthal torus (arbitrary positive side lengths $N_x,N_y,N_z$) as the scalable target for a finite 3D triangulation encoding. Vertices are the product lattice $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. Each unit cube is split into the standard six Freudenthal tetrahedra; each tet has six local edge slots.
The map localEdgeOf (periodic version) takes a cell, a tet index, and a local slot and returns a PeriodicEdge: it looks up the fixed cube-table edge from the non-periodic Freudenthal cube triangulation, then translates the base by the cell via bit-displacements. Upstream cube and two-cube-strip tables supply the same combinatorial edge representatives; the torus version only adds the lattice translate.
The module goal is any finite Triangulation3D encoding this typed model must carry the global incidence/edge-slot partition needed by the nonlinear Regge first-variation theorem. Side lengths $>2$ later rule out degenerate wraparound.
proof idea
Definitional Prop, not a proved theorem. The body is the universal statement that localEdgeOf cell tet is injective as a map Fin 6 → PeriodicEdge. No tactics; the companion theorem canonicalPeriodicLocalEdgeNoDup later proves the Prop by intro then exhaustive fin_cases on tet, f, g with simp against the cube localEdgeOf table and the translate constructors.
why it matters
Named remaining wraparound/no-duplication target for promoting the canonical periodic skeleton to a full EncodedPeriodicFreudenthalTorus. Downstream, canonicalEncodedPeriodicFreudenthalTorus_of_incidence takes this Prop as a hypothesis alongside incidence consistency and side lengths $>2, then fills the finite encoder structure (tet/edge equivalences and edgeInTet_iff`).
Also feeds canonicalEdgeInTet_iff_of_noDup (invertibility of the optional edge-in-tet witness), canonicalLocalEdge_complete (every local slot is hit by some global edge index), and related slot lemmas. In the geometry stack this is the last combinatorial injectivity gate before the typed torus becomes a concrete Triangulation3D usable by Regge variation. Not itself a forcing-chain (T0–T8) step; it is mesh infrastructure those continuum limits sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.