regularUnitCofactorCheck
plain-language theorem explainer
For every edge of the regular unit tetrahedron, the Cayley–Menger cofactors of the two opposite vertices equal 1 off-diagonal and −3 on the diagonals. Anyone deriving the internal dihedral cosine from cofactors cites this. The proof is a six-way case split on the edge index, discharging each case by the precomputed regular-unit cofactor identities.
Claim. For every edge $e$ of the regular unit tetrahedron, if $p$ and $q$ are the two vertices opposite $e$ in the Cayley–Menger indexing, then the cofactors satisfy $C_{p,q}=1$, $C_{p,p}=-3$, and $C_{q,q}=-3$.
background
This module defines tetrahedral dihedral cosines from Cayley–Menger cofactors, replacing a prose reference in the older dihedral-angle API. For an edge $e=(i,j)$, the two opposite vertices $(p,q)$ are read in the $5\times 5$ Cayley–Menger matrix (vertex $v:\mathrm{Fin},4$ sits at CM index $v+1$). The classical formula is $\cos\theta_e=C_{p,q}/\sqrt{C_{p,p}C_{q,q}}$, with the sign convention that yields $\cos\theta=1/3$ on the regular tetrahedron.
The predicate being proved packages exactly the three cofactor values needed to reduce that formula on the regular unit edge-squared matrix: off-diagonal $1$ and both diagonals $-3$, for every edge. Those numerical identities are already established upstream as individual cofactor theorems (regularUnit_cofactor_12, _13, _14, _23, _24, _34, and the vertex-diagonal cofactor), each obtained by expanding a $3\times 3$ minor and evaluating its determinant.
proof idea
Introduce the edge index $e:\mathrm{Fin},6$ and split into six cases. In each case, unfold the opposite-vertex pair and simplify against the six precomputed regular-unit cofactor lemmas plus the vertex-diagonal cofactor identity. No new determinant work happens here: the proof only assembles the existing numerical equalities into the universal quantifier over edges.
why it matters
This closes the gap between the cofactor formula and the classical regular-tetrahedron value. Downstream, dihedralCos3_regularUnit applies the cofactor-check reduction to obtain $\cos\theta=1/3$ with no external hypothesis, and dihedralAngle3_regularUnit matches the cofactor angle to the existing regular-tetrahedron dihedral API. The module doc states the goal explicitly: the cofactor definition should give $\cos\theta=1/3$ on the regular tetrahedron. By promoting the cofactor check from an assumption to a proved theorem, those two corollaries become unconditional. In the broader Recognition geometry stack this anchors the discrete curvature / Regge side of the tetrahedral scaffolding to a fully certified classical identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.