edgeVerts
plain-language theorem explainer
Enumerates the 19 undirected edges of the Freudenthal six-tetrahedron triangulation of the unit cube as ordered pairs of cube vertices in {0,...,7}. Anyone building Regge or discrete-geometry bookkeeping on this cube cites it as the global edge table. The body is a pure case table on Fin 19 with an absurd branch for out-of-range indices.
Claim. Define a map from $\{0,\ldots,18\}$ to ordered pairs of cube vertices in $\{0,\ldots,7\}$ listing the nineteen distinct edges of the Freudenthal triangulation of the unit cube (binary labels $0=(0,0,0)$ through $7=(1,1,1)$), with the residual index branch empty by $\omega$-arithmetic.
background
The module fixes the standard Freudenthal decomposition of one unit cube into six tetrahedra along the body diagonal from vertex 0 to vertex 7. Cube vertices carry 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)$. The six tets are exactly the monotone paths from 0 to 7.
Incidence data for a finite 3D triangulation needs a global edge list before local face and tet tables. This definition supplies that list: nineteen unique edges as ordered pairs in $\mathrm{Fin},8\times\mathrm{Fin},8$. A parallel table appears in the two-cube strip module (thirty-three edges); the cosmology rung-descent utilities use a different, set-theoretic edgeVerts that extracts vertices from an arbitrary edge Finset.
Squared edge lengths and the assembled triangulation record sit immediately downstream of this table.
proof idea
No proof: pure definition by pattern match. Each of the nineteen constructors of Fin 19 is mapped to a fixed ordered pair of Fin 8 vertices. The catch-all branch for indices $\ge 19$ is discharged by absurdity via omega, so the function is total on Fin 19.
why it matters
This table is the edge field of freudenthalCube, the finite Triangulation3D instance with nV=8, nE=19, nT=6. Downstream edgeInTet_vertices uses it to match global edges against local tet edge vertices (orientation either way). Sibling lemmas (local_sqEdge_eq_global, edgeInTet_iff_localEdgeOf) and the two-cube strip reuse the same naming pattern.
In the broader Recognition geometry stack the Freudenthal cube is the discrete 3-cell on which Regge first-variation and rung-ladder bookkeeping sit; D=3 is already forced at T8, and the eight-tick octave lives on the dual discrete time. The cosmology unit-step descent theorems consume edge-vertex incidence of this shape when they read off realised maximum rungs. Without a fixed global edge enumeration the incidence class cannot be instantiated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.