cmCofactor3_12_eq_poly
plain-language theorem explainer
The (1,2) cofactor of the tetrahedral Cayley–Menger matrix equals its named explicit polynomial in the six squared edge lengths. Anyone computing dihedral cosines or CM partials from closed-form polynomials rather than opaque determinants will cite this. The proof unfolds the cofactor, substitutes the (1,2)-minor submatrix identity and its determinant polynomial, then evaluates the odd sign (−1)^{1+2}.
Claim. For any assignment $a$ of the six squared edge lengths of a tetrahedron, the Cayley–Menger cofactor $C_{1,2}(a)$ equals the explicit polynomial $\mathrm{Poly}_{1,2}(a)$ in those six coordinates.
background
The module expands every cofactor of the $5\times 5$ tetrahedral Cayley–Menger matrix into a named polynomial in the six squared edge coordinates (SqEdges). Downstream dihedral-angle calculus can then differentiate those polynomials instead of working with opaque fderiv terms on determinants.
The cofactor is defined as $C_{r,c}=(-1)^{r+c},M_{r,c}$, where $M_{r,c}$ is the determinant of the matrix obtained by deleting row $r$ and column $c$. The sign factor is $+1$ when $r+c$ is even and $-1$ when odd. The companion object cmCofactor3Poly r c is the closed-form polynomial that is claimed to match $C_{r,c}$ identically.
This lemma treats the single off-diagonal pair $(r,c)=(1,2)$. Sibling lemmas handle the other index pairs; together they feed the universal agreement statement.
proof idea
Unfold the cofactor and minor definitions so the goal is a signed determinant of a $4\times 4$ submatrix. Rewrite that submatrix via cmMinor12_submatrix_eq and replace its determinant by the precomputed polynomial det_cmMinor12Matrix. Finish by simplifying the sign: $1+2=3$ is odd, so cmCofactorSign3 1 2 = -1, which matches the leading sign baked into the polynomial normal form.
why it matters
This is one cell in the case-split that proves full cofactor–polynomial agreement (cmCofactor3_eq_poly): every $C_{r,c}$ equals its named polynomial. It is also invoked by cmCofactor3_opposite_eq_poly, which covers the six opposite-vertex cofactors that appear as numerators of tetrahedral dihedral cosines.
Those cosines and their edge derivatives sit in the geometry layer that feeds Recognition Science’s continuum limit (spatial dimension $D=3$ forced at T8, eight-tick discrete register). Explicit polynomial cofactors let dihedral calculus stay algebraic rather than relying on automatic differentiation of determinants, which is the module’s stated purpose as the cofactor analogue of CayleyMengerDerivatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.