regularUnit_cofactor_34
plain-language theorem explainer
For the unit regular tetrahedron (all squared edges 1), the Cayley–Menger cofactor at matrix indices (3,4) equals 1. Cite this when verifying the regular-unit cofactor suite that feeds the dihedral cosine formula. The proof unfolds the cofactor, reduces the (3,4) minor to an explicit off-diagonal 4×4 of determinant −1, and multiplies by the odd-parity sign −1.
Claim. Let all six squared edge lengths of a tetrahedron equal $1$. Then the Cayley–Menger cofactor $C_{3,4}$ of the associated $5\times 5$ matrix equals $1$.
background
This module sits between the explicit tetrahedral Cayley–Menger polynomial and the $5\times 5$ determinant/cofactor layer used by the dihedral cosine formula. Rows and columns are indexed $0..4$, with the usual border of ones and zeros on the diagonal of the edge block; the six squared lengths occupy the off-diagonal edge slots.
A cofactor is the signed minor: delete row $r$ and column $c$, take the determinant, and multiply by $(-1)^{r+c}$. The unit regular tetrahedron is the edge assignment with every squared length equal to $1$. Upstream, the $(3,4)$ minor of that matrix is identified with a fixed off-diagonal normal-form matrix whose determinant is $-1$.
proof idea
Unfold the cofactor into sign times minor. The index sum $3+4=7$ is odd, so the sign simplifies to $-1$. Rewrite the minor via the equality that identifies the $(3,4)$ submatrix of the regular-unit Cayley–Menger matrix with the explicit off-diagonal normal form; that form has determinant $-1$. The product $(-1)\cdot(-1)=1$ is finished by norm_num.
why it matters
The dihedral cosine formula needs concrete cofactor values on the regular unit tetrahedron as a sanity and normalization check. Downstream, regularUnitCofactorCheck packages all six opposite-edge cofactors and cites this result for the $(3,4)$ slot, turning what had been an assumption into a proved lemma. That check is part of the geometry layer that connects Cayley–Menger determinants to dihedral angles; it does not itself invoke the Recognition forcing chain (T0–T8), but it hardens the classical tetrahedral geometry that later RS geometry modules may quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.