canonicalLocalEdge_complete
plain-language theorem explainer
Under the wraparound no-duplication hypothesis, every local edge slot of every periodic Freudenthal tetrahedron is hit by some global periodic edge in the canonical edge-in-tet lookup. Anyone assembling the finite periodic triangulation skeleton or proving incidence consistency cites this surjectivity. The proof builds the witnessing edge from the local Freudenthal table and rewrites via the no-dup characterization.
Claim. Let $N_x,N_y,N_z\ge 1$. Assume that within each periodic cubic cell and each of its six Freudenthal tetrahedra, the six local edge slots map injectively to global edges (no two slots share an edge). Then for every periodic tetrahedron $\tau$ and every local slot $f\in\{0,\ldots,5\}$ there exists a global periodic edge $e$ such that the canonical edge-in-tetrahedron map sends $(e,\tau)$ to $\mathrm{some}\,f$.
background
The module builds a typed periodic Freudenthal torus: vertices on an $N_x\times N_y\times N_z$ lattice with wraparound, positive-displacement edges (base vertex plus one of seven cube displacements), and tetrahedra as a cell times one of six Freudenthal tets per cube. The goal is a finite Triangulation3D whose global incidence partition feeds the nonlinear Regge first-variation theorem.
localEdgeOf (from the cube triangulation) assigns to each tet index and local slot $f\in\mathrm{Fin},6$ a concrete global edge representative. The periodic skeleton lifts this via finite equivalences tetFinEquiv and edgeFinEquiv. The lookup canonicalEdgeInTet asks whether a global edge occupies a given local slot of a tet, returning an optional slot index.
The hypothesis CanonicalPeriodicLocalEdgeNoDup is the remaining wraparound target: in every cell and tet, distinct local slots give distinct edges. Upstream, canonicalEdgeInTet_iff_of_noDup converts that injectivity into an iff characterizing when the lookup returns some f.
proof idea
Construct the witness explicitly. Decode $\tau$ to a cell and tet index via tetFinEquiv, then set edge := localEdgeOf cell tet f. Reindex that edge to a Fin label by edgeFinEquiv.symm.
A short simp recovers that applying edgeFinEquiv to the reindexed label yields the same localEdgeOf value. Feed that equality into the reverse direction of canonicalEdgeInTet_iff_of_noDup (which needs the no-dup hypothesis) to conclude canonicalEdgeInTet e \tau = some f.
why it matters
Incidence consistency for the canonical periodic triangulation needs every local tet slot to be occupied by a unique global edge. This completeness lemma supplies the existence half of that occupancy under the wraparound no-dup assumption.
It is consumed by canonicalPeriodicIncidenceConsistent_of_endpoint, which packages global squared-edge data and edge-in-tet vertex incidence into an IncidenceConsistent instance on canonicalPeriodicTriangulation. That instance is the geometric prerequisite for the nonlinear Regge first-variation theorem on the periodic mesh.
In the broader Recognition geometry stack, the Freudenthal six-tet cube decomposition and the eight-tick/octave structure sit behind the discrete 3D skeleton (forcing chain T7–T8). The module doc still flags that a full encoded torus certificate also needs wraparound no-duplication and local/global squared-edge proofs; this theorem closes the slot-surjectivity fragment once no-dup is granted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.