tetVerts
plain-language theorem explainer
Explicit vertex table for the twelve Freudenthal tetrahedra in the two-cube strip: six in the left unit cube and six in the right, on a shared 12-vertex set. Anyone building the strip triangulation or checking edge-in-tet incidence cites this map. The body is a pure case table, not a derived construction.
Claim. Let $T=\mathrm{Fin}\,12$ index the twelve tetrahedra of the two-cube Freudenthal strip and $V=\mathrm{Fin}\,12$ its global vertices. The map $\mathrm{tetVerts}:T\to(\mathrm{Fin}\,4\to V)$ sends each tetrahedron $\tau$ and local corner $i\in\{0,1,2,3\}$ to the corresponding global vertex index, with six tets on the left cube and six on the right.
background
The module builds the smallest nontrivial multi-cube Freudenthal example: two unit cubes glued along one square face, each cut into the standard six Freudenthal tetrahedra with matching face triangulation. After deduplicating the five shared-face edges one obtains 12 vertices, 33 global edges, and 12 tets.
Here $V:=\mathrm{Fin},12$ is that global vertex set and $T:=\mathrm{Fin},12$ indexes the tetrahedra. The one-cube precursor in FreudenthalCubeTriangulation uses an analogous table $\mathrm{Fin},6\to\mathrm{Fin},4\to\mathrm{Fin},8$; the strip table extends that pattern across the glue face so left and right cubes share the interface vertices consistently.
This table is the combinatorial skeleton later packaged into the Triangulation3D record for the strip and reused when checking that every local tet edge lands on a declared global edge.
proof idea
Definition by exhaustive pattern match: twelve blocks (one per $\tau:T$), each listing four global vertex indices in $V$ for local slots $0..3$. No lemmas or tactics; the values are the explicit Freudenthal corner lists for the left cube ($\tau=0..5$) and right cube ($\tau=6..11$), written so shared-face vertices receive the same global labels on both sides.
why it matters
This is the vertex incidence data that makes the two-cube strip a concrete Triangulation3D: twoCubeStrip plugs tetVerts in as its tet-vertex field (12 verts, 33 edges, 12 tets). Downstream, edgeInTet_vertices uses the table to prove that whenever a global edge sits in a tet, the two endpoints match the corresponding local edge slots (up to order).
The same pattern feeds the periodic Freudenthal torus development (canonicalPeriodicTriangulation, encoded $K$-tet vertex equalities), where multi-cube gluing must stay consistent under lattice periods. In the Recognition geometry stack this is the first multi-cube incidence instance beyond the single-cube sanity check, so face-compatible Freudenthal decomposition is pinned before larger torus or continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.