oppositeCMVertices
plain-language theorem explainer
For each of the six edges of a tetrahedron, returns the pair of Cayley-Menger matrix indices of the two vertices opposite that edge (geometric vertex $v$ maps to CM index $v+1$). Anyone writing cofactor formulas for tetrahedral dihedral cosines cites this lookup. The body is an exhaustive six-case table on $\mathrm{Fin}\,6$, not a derived lemma.
Claim. Assign to each tetrahedral edge index $e\in\{0,\ldots,5\}$ the ordered pair $(p,q)\in\{0,\ldots,4\}^2$ of Cayley-Menger row/column indices of the two vertices opposite $e$, under the convention that geometric vertex $v\in\{0,1,2,3\}$ occupies CM index $v+1$. Explicitly: edge $(0,1)\mapsto(3,4)$, $(0,2)\mapsto(2,4)$, $(0,3)\mapsto(2,3)$, $(1,2)\mapsto(1,4)$, $(1,3)\mapsto(1,3)$, $(2,3)\mapsto(1,2)$.
background
The module builds tetrahedral dihedral cosines from cofactors of the $5\times 5$ Cayley-Menger matrix, replacing an earlier prose reference in the dihedral-angle development. For an edge $e=(i,j)$, write $(p,q)$ for the two remaining vertices. Geometric vertices live in $\mathrm{Fin},4$; CM rows/columns are shifted by one, so vertex $v$ sits at index $v+1$ in $\mathrm{Fin},5$.
The classical formula used throughout is $$\cos\theta_e=C_{p,q}/\sqrt{C_{p,p}C_{q,q}},$$ where $C$ is the cofactor matrix of the Cayley-Menger matrix. The sign convention is fixed so that a regular unit tetrahedron yields $\cos\theta=1/3$, matching the standard internal dihedral angle.
This declaration is the pure combinatorial bookkeeping that turns an edge label in $\mathrm{Fin},6$ into the pair $(p,q)$ of CM indices needed by every subsequent cofactor expression.
proof idea
No proof: the declaration is a total function defined by six pattern-match clauses on $\mathrm{Fin},6$. Each clause hard-codes the CM-index pair for one tetrahedral edge, with inline comments recording the geometric edge and its opposite vertices before the $+1$ shift. There are no lemmas, tactics, or algebraic reductions.
why it matters
Every cofactor-based dihedral cosine in the geometry stack indexes opposite vertices through this map. Downstream, CofactorDerivatives uses it to build the numerator cofactor, the product of diagonal cofactors (the cosine denominator), the polynomial discriminant identity
$$C_{pp}C_{qq}-C_{pq}^2=2,\mathrm{cm}_3(a),a_e,$$
and the closed-form and path derivatives of the squared cosine ratio. Without a single canonical opposite-vertex table, those formulas would re-encode the same six cases ad hoc.
In the broader Recognition geometry layer this is scaffolding for rigorous Regge-style hinge and dihedral data (the module imports the Cayley-Menger matrix and Regge foundation). It does not itself touch the forcing chain (T0-T8), RCL, or $\phi$-ladder mass formulas; it is local combinatorial infrastructure for 3D simplex angles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.