localEdgeOf
plain-language theorem explainer
Assigns to each of the six Freudenthal tetrahedra and each of its six local edge slots a global edge index in {0,...,18}. Regge incidence proofs on the unit cube cite this table as the canonical local-to-global edge map. It is a pure case-split definition: thirty-six explicit assignments, no derivation.
Claim. In the Freudenthal decomposition of the unit cube into six tetrahedra, the map $(\tau,f)\mapsto e$ sends each tetrahedron index $\tau\in\{0,\ldots,5\}$ and each local edge slot $f\in\{0,\ldots,5\}$ to a global edge index $e\in\{0,\ldots,18\}$.
background
The module fixes the standard Freudenthal split of the unit cube along the body diagonal from vertex $0=(0,0,0)$ to $7=(1,1,1)$. Cube vertices are labeled by binary coordinates $0..7$. The six tetrahedra are exactly the monotone lattice paths from $0$ to $7$.
Each tetrahedron has $\binom{4}{2}=6$ edges (local slots). Globally one needs the cube's $12$ skeleton edges, one chosen diagonal on each of the $6$ faces, and the body diagonal, totaling $19$ edges indexed by $\mathrm{Fin},19$. This definition is the lookup table that names, for every local slot of every tet, which of those $19$ global edges it is.
A parallel table appears in the two-cube strip module; the present map is the single-cube instance used by the incidence bookkeeping class for Regge first-variation work.
proof idea
Definition by exhaustive pattern match on $\mathrm{Fin},6\times\mathrm{Fin},6$. Each of the thirty-six pairs $(\tau,f)$ is assigned a concrete global index in $\mathrm{Fin},19$. No lemmas are invoked; the body is the table itself.
why it matters
This table is the witness that every local edge slot of every Freudenthal tetrahedron is realized by some global edge. Downstream, edgeInTet_iff_localEdgeOf proves the inverse incidence relation by finite case analysis against this map; localEdge_complete obtains existence of a global edge for each slot as the pair (localEdgeOf τ f, ...); and freudenthalCube_edgeSlotPartition packages the map into the unique/no-duplication edge-slot partition required by the incidence class.
The same pattern is reused on the two-cube strip. In the broader RS geometry stack this is pure 3-space bookkeeping: the cube lives in the $D=3$ forced by the T8 step of the forcing chain, and the six-tet split is the discrete substrate for Regge hinge and zero-mode analysis imported from the first-variation module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.