edgeInTet
plain-language theorem explainer
Incidence table sending a global edge (among 19) and a tetrahedron (among 6) of the Freudenthal cube to the local edge slot 0–5 when that edge lies on the tet, else none. Cited by anyone wiring Regge or discrete-geometry incidence on the standard six-tet cube. Pure exhaustive case table on Fin 19 × Fin 6; no proof body.
Claim. For each global edge index $e\in\{0,\ldots,18\}$ and each tetrahedron index $\tau\in\{0,\ldots,5\}$ in the Freudenthal six-tetrahedron cube, the incidence map returns the local edge slot $f\in\{0,\ldots,5\}$ if $e$ is the $f$-th edge of $\tau$, and is undefined otherwise.
background
The module builds incidence bookkeeping for the standard Freudenthal split of the unit cube into six tetrahedra along the body diagonal from vertex $0=(0,0,0)$ to $7=(1,1,1)$. Vertices carry binary coordinates; the six tets are the monotone paths from $0$ to $7$.
Each tet has six edges, indexed locally by $\mathrm{Fin},6$. Globally the triangulation uses 19 edges (cube edges, face diagonals, and the body diagonal that appear in the tets). A companion map sends a tet and local slot to the corresponding global edge; the present definition is the partial inverse incidence.
The two-cube-strip module defines an analogous map by sequential equality tests against that companion. Here the single-cube module hard-codes the same relation as a finite lookup table.
proof idea
Definition by exhaustive pattern match: thirty-six clauses list the (global edge, tet) pairs that hit, each returning $\mathrm{some}$ local slot, with a catch-all $\mathrm{none}$. No tactics and no proof obligations; the table is the content. Later lemmas (via $\mathrm{fin_cases}$) certify that the table is exactly the inverse of the local-to-global edge map and that vertex endpoints match.
why it matters
Supplies the incidence field used by the finite Freudenthal cube triangulation instance ($8$ vertices, $19$ edges, $6$ tets). Downstream lemmas prove the table is inverse to the local-to-global edge map, that every local slot is realized, that endpoints agree with tet vertex data, and that squared edge lengths match between local tet data and global edges. Those facts are the combinatorial substrate for first-variation Regge action on this cell (the module imports the Regge first-variation infrastructure). In the Recognition geometry stack this is the concrete $D=3$ cubic cell on which discrete curvature and defect sums are evaluated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.