tetVerts
plain-language theorem explainer
Lookup table listing the four cube vertices of each of the six Freudenthal tetrahedra that fill the unit cube along the body diagonal from 0 to 7. Anyone building incidence data, edge-in-tet maps, or the finite triangulation package cites it. The body is a pure pattern-match table, not a derived proof.
Claim. A map $\mathrm{tetVerts}:\{0,\ldots,5\}\times\{0,\ldots,3\}\to\{0,\ldots,7\}$ sending tetrahedron index $\tau$ and local vertex slot $k$ to a global cube vertex. Explicitly the six ordered 4-tuples are $(0,1,3,7)$, $(0,1,5,7)$, $(0,2,3,7)$, $(0,2,6,7)$, $(0,4,5,7)$, $(0,4,6,7)$, i.e. the monotone paths from $(0,0,0)$ to $(1,1,1)$.
background
The module fixes the standard Freudenthal decomposition of one unit cube into six tetrahedra sharing the body diagonal from vertex 0 to vertex 7. Cube vertices are labeled by binary coordinates: $0=(0,0,0)$, $1=(1,0,0)$, $2=(0,1,0)$, $3=(1,1,0)$, $4=(0,0,1)$, $5=(1,0,1)$, $6=(0,1,1)$, $7=(1,1,1)$.
Each tetrahedron is a monotone path of three coordinate flips from the origin corner to the opposite corner. The six paths correspond to the six permutations of the three axes; the table records their ordered vertex lists. Downstream incidence data (global edges, local edge slots, edge-in-tet membership) all read this table.
A sibling two-cube-strip table reuses the same six patterns on each half of a $1\times1\times2$ strip, and the periodic torus construction lifts the same vertex lists cellwise.
proof idea
No proof: the declaration is a definition by exhaustive pattern match on $\mathrm{Fin},6\times\mathrm{Fin},4$. Each clause hard-codes one global cube vertex index in $\mathrm{Fin},8$. There are no lemmas applied and no tactics.
why it matters
This table is the vertex half of the finite Freudenthal cube triangulation package. It is plugged directly into freudenthalCube as the tetVerts field of the 3D triangulation record (8 vertices, 19 edges, 6 tets). Edge-membership theorems such as edgeInTet_vertices compare global edge endpoints against tetVerts τ to certify that a claimed local edge really sits inside tetrahedron $\tau$.
The same pattern is copied into the two-cube strip (twelve tets) and into the periodic Freudenthal torus, where equality lemmas identify encoded periodic tet vertices with the canonical lift of this table. In the broader Recognition geometry stack this supplies the discrete 3-complex on which Regge-type first-variation and gluing bookkeeping run, consistent with the forced spatial dimension $D=3$ (T8) and the eight-vertex cube that matches the eight-tick register.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.