regularUnit_cofactor_23
plain-language theorem explainer
For the unit regular tetrahedron (all squared edges equal to 1), the Cayley–Menger cofactor at matrix indices (2,3) equals 1. Dihedral-angle work cites this as one of the six opposite-edge cofactor normalizations. The proof unfolds the cofactor into sign times minor, rewrites the (2,3)-minor as a fixed off-diagonal matrix, and evaluates its determinant to −1.
Claim. Let $C_{r,c}$ be the cofactor of the $5\times 5$ Cayley–Menger matrix built from squared edge lengths. For the unit regular tetrahedron (every squared edge length equal to $1$), one has $C_{2,3}=1$.
background
This module sits between the explicit tetrahedral Cayley–Menger polynomial cm3 and the genuine $5\times 5$ determinant. Rows and columns are indexed $0..4$, with the border of ones in row/column 0 and squared lengths $a_0..a_5$ filling the $4\times 4$ distance block 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}$. The unit regular edge data sets every squared length to $1$. Upstream, the $(2,3)$-submatrix of that regular matrix is identified with a concrete off-diagonal $4\times 4$ matrix whose determinant equals $-1$.
proof idea
Unfold the cofactor into sign times minor. The index sum $2+3=5$ is odd, so the sign is $-1$ (discharged by a decidability simp). Rewrite the deleted-$(2,3)$ submatrix via the equality that matches it to the named regular off-diagonal minor matrix, then apply the lemma that its determinant is $-1$. The product $(-1)\cdot(-1)$ simplifies by norm_num to $1$.
why it matters
Dihedral cosines for a tetrahedron are ratios of Cayley–Menger cofactors of opposite edges. Downstream, regularUnitCofactorCheck packages all six opposite-edge cofactors of the unit regular tetrahedron as a proved predicate rather than an assumption; this declaration supplies the $(2,3)$ case (edge $(01)$ opposite $(23)$ in the module indexing). Together with the sibling cofactor evaluations it closes the regular-unit normalization used when checking the dihedral formula against the classical arccos$(1/3)$ value. In the broader Recognition geometry stack this is pure Euclidean bookkeeping supporting later discrete-geometry constraints, not a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.