regularUnit_cofactor_12
plain-language theorem explainer
For the regular unit tetrahedron (all squared edge lengths equal to 1), the Cayley–Menger cofactor C_{1,2} equals 1. Dihedral-angle and volume identities that expand the 5×5 CM determinant cite this entrywise evaluation. The proof unfolds the cofactor definition, reduces the (1,2)-minor to a fixed off-diagonal normal form, and evaluates that 4×4 determinant to −1.
Claim. Let $A$ be the $5\times 5$ Cayley–Menger matrix of the regular unit tetrahedron (every squared edge length equal to $1$). Then the cofactor $C_{1,2}(A)$ equals $1$.
background
This module sits between the explicit tetrahedral Cayley–Menger polynomial cm3 and the genuine $5\times 5$ determinant. Rows/columns are indexed $0..4$, with the border row/column of ones and the $4\times 4$ block of squared edge lengths $a_0..a_5$ for pairs $(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}$. The regular-unit edge data set every squared length to $1$, so the matrix is completely rigid and every minor is a pure number.
Upstream, the $(1,2)$-submatrix of the regular-unit CM matrix is identified with a fixed off-diagonal normal form whose determinant equals $-1$. Those two facts are the only nontrivial inputs.
proof idea
Unfold the cofactor into sign times minor. The index sum $1+2=3$ is odd, so the sign is $-1$ (discharged by a decide on parity). Rewrite the minor via the equality that identifies the deleted-$(1,2)$ submatrix with the regular-unit off-diagonal normal form, then replace its determinant by the already-proved value $-1$. A final norm_num multiplies $(-1)\cdot(-1)$ to obtain $1$.
why it matters
The dihedral cosine formula for a tetrahedron is built from ratios of CM cofactors. Downstream, regularUnitCofactorCheck packages the six opposite-edge cofactor evaluations (including this one) into a single discharged hypothesis: the regular-unit cofactor check is now a theorem, not an assumption. That closes the regular-tetrahedron base case for the dihedral layer that feeds Recognition geometry (volume, solid angle, and the eight-tick spatial scaffolding tied to $D=3$). Without the entrywise values, the cosine identities remain conditional on numeric cofactor tables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.