regularUnit_cofactor_24
plain-language theorem explainer
For the unit regular tetrahedron (all squared edges 1), the Cayley–Menger cofactor C_{2,4} equals 1. Anyone checking the dihedral-cosine formula on the regular unit case cites this. The proof unfolds the cofactor, notes the sign is +1 because 2+4 is even, then rewrites the minor to a precomputed off-diagonal matrix whose determinant is 1.
Claim. Let $a$ be the squared-edge data of the unit regular tetrahedron (every squared length equal to $1$). Then the Cayley–Menger cofactor $C_{2,4}(a)$ equals $1$.
background
This module sits between the explicit tetrahedral Cayley–Menger polynomial cm3 and the genuine $5\times 5$ Cayley–Menger determinant. The matrix convention indexes rows/columns $0..4$, with the border of ones and the six squared edge lengths $a_0..a_5$ filling the interior off-diagonals in the order $(01),(02),(03),(12),(13),(23)$.
A minor deletes one row and one column and takes the determinant; the cofactor multiplies that minor by the sign $(-1)^{r+c}$. Here $r=2$, $c=4$, so the sign is $+1$ because $2+4$ is even. The edge data regularUnitSqEdges is the constant function $1$: every squared length of the unit regular tetrahedron.
Two upstream facts are used: the $(2,4)$-minor of the regular-unit matrix equals a fixed $4\times 4$ off-diagonal matrix regularUnitOffDiagMinorMatrix24, and the determinant of that matrix is already known to be $1$.
proof idea
Term-mode proof by unfolding and rewrite. Unfold the cofactor into sign times minor. The sign definition reduces by simp once Even 6 is decided, giving factor $+1$. Rewrite the remaining minor via regularUnit_minor_24_eq_offDiag to the named off-diagonal matrix, then apply det_regularUnitOffDiagMinorMatrix24 to conclude the determinant is $1$.
why it matters
Feeds regularUnitCofactorCheck in DihedralCayleyMenger, whose doc-comment states that the regular-unit cofactor check is now a theorem, not an assumption. That check packages the six opposite-vertex cofactors needed by the dihedral cosine formula on the unit regular tetrahedron. Together with the sibling cofactor identities (regularUnit_cofactor_34, _23, _14, _13, _12), it closes the regular-unit side of the determinant/cofactor layer that the module exists to supply. In the broader Recognition geometry stack this is pure Euclidean scaffolding: volume and dihedral data for the regular tetrahedron, not a forcing-chain step, but required before any RS claim that quotes regular-tetrahedron angles or volumes can sit on a proved cofactor identity rather than a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.