edgeVertices3
plain-language theorem explainer
Maps each of the six tetrahedral edge indices to the ordered pair of endpoint vertices in Fin 4. Anyone working with realized tetrahedra, face normals, or Cayley–Menger cofactors cites this as the shared edge-labeling convention. The definition is a one-line alias of the Regge foundation edge table.
Claim. The map $e \mapsto (i,j)$ sends each edge index $e \in \{0,\ldots,5\}$ to the ordered pair of vertex indices $(i,j) \in \{0,1,2,3\}^2$ with the standard tetrahedral labeling: $0\mapsto(0,1)$, $1\mapsto(0,2)$, $2\mapsto(0,3)$, $3\mapsto(1,2)$, $4\mapsto(1,3)$, $5\mapsto(2,3)$.
background
The module builds Euclidean realizations of tetrahedra: it turns the abstract six squared-edge lengths used by the Cayley–Menger layer into concrete points in $\mathbb{R}^3$. Edges of a 4-vertex simplex are indexed by $\mathrm{Fin},6$; vertices by $\mathrm{Fin},4$.
The upstream table in the Regge foundation fixes the combinatorial convention once and for all: edge $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$. That table is the sole content of this definition; the local name simply re-exports it into the realization namespace so downstream geometry can refer to endpoints without importing the Regge module directly.
Sibling constructions (edge vectors, squared distances of realized points, Gram matrices, volume-from-Gram) all read endpoints through this map.
proof idea
One-line definitional alias: the body is exactly the upstream edgeVertices table from the Regge rigorous foundation. No computation, no proof obligations.
why it matters
This is the shared edge-to-vertex dictionary for the entire realized-tetrahedron stack. Downstream, adjacent-face-normal constructions unpack each edge index through it, then form the two face normals meeting that edge and prove their cross product is a scalar multiple of the shared edge vector. Linear-independence statements for the edge-plus-two-opposite-vertex triple likewise begin by reading endpoints here.
On the cofactor side, the four edge-indexed identities equating products of Cayley–Menger diagonal cofactors to sixteen times the geometric dihedral denominator square all depend on the same labeling, so that edge $0$ through edge $5$ line up with the correct pairs of faces. Without a single fixed convention, those dihedral and affine-independence lemmas would not compose.
In the broader Recognition geometry layer this sits under the $D=3$ forcing (T8): tetrahedra are the elementary 3-simplices whose edge data feed Regge-style curvature and volume formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.