cmVertexIndex
plain-language theorem explainer
Maps each tetrahedron vertex label in {0,1,2,3} to the matching Cayley-Menger row/column index in {1,2,3,4} by the fixed shift v ↦ v+1. Anyone extracting dihedral cosines from 5×5 CM cofactors cites this index convention. The body is a four-clause pattern match; no proof obligations.
Claim. Define the index map $\mathrm{cmVertexIndex}:\{0,1,2,3\}\to\{1,2,3,4\}$ by $\mathrm{cmVertexIndex}(v)=v+1$. Equivalently, tetrahedron vertex $v$ is sent to Cayley-Menger matrix index $v+1$ (the border row/column of the $5\times 5$ CM matrix occupies index $0$).
background
The module builds tetrahedral dihedral cosines from cofactors of the bordered $5\times 5$ Cayley-Menger matrix. Classically, for an edge $e=(i,j)$ with opposite vertices $(p,q)$,
$$\cos\theta_e = C_{p,q}/\sqrt{C_{p,p}C_{q,q}},$$
where $C$ is the cofactor matrix. Vertex rows and columns of that matrix are offset by one relative to the geometric labels $0..3$: the border occupies index $0$, so geometric vertex $v$ sits at CM index $v+1\in{1,2,3,4}$.
This definition is exactly that offset. Sibling maps (opposite CM vertices, the three-edge dihedral cosine and angle) consume it so that cofactor lookups stay aligned with the classical formula, which yields $\cos\theta=1/3$ on the regular unit tetrahedron.
proof idea
Not a theorem: a total function on Fin 4 defined by four pattern-match clauses sending $0\mapsto 1$, $1\mapsto 2$, $2\mapsto 3$, $3\mapsto 4$. Equivalent to fun v => ⟨v.val + 1, by omega⟩. No lemmas are invoked.
why it matters
Locks the vertex-to-CM index convention used throughout the dihedral-from-cofactors stack in this module (oppositeCMVertices, dihedralCos3, dihedralAngle3, and the regular-unit checks). Downstream, the complex Wick-action path mirrors it when building bordered $6\times 6$ cofactors (cmCofactorC in WickActionComplexFirst), so real and complex CM pipelines share the same shift. In the broader RS geometry layer this is bookkeeping for Regge-style hinge angles on tetrahedra, not a forcing-chain step; it simply makes the classical cofactor formula type-check against Fin 5 indices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.