cmCofactor3_33_eq_poly
plain-language theorem explainer
The (3,3) cofactor of the tetrahedral Cayley–Menger matrix equals a named explicit polynomial in the six squared edge lengths. Anyone computing dihedral cosines or CM partials from closed-form polynomials cites this case. The proof unfolds the cofactor, substitutes the explicit 4×4 minor and its determinant polynomial, then simplifies the even-parity sign to +1.
Claim. For any assignment $a$ of the six squared edge lengths of a tetrahedron, the Cayley–Menger cofactor $C_{3,3}(a)$ equals the explicit polynomial normal form $\mathrm{Poly}_{3,3}(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. Downstream dihedral-angle calculus can then differentiate those polynomials instead of opaque Fréchet derivatives of determinants.
The cofactor is defined as $C_{r,c}=(-1)^{r+c},M_{r,c}$, where $M_{r,c}$ is the determinant of the submatrix obtained by deleting row $r$ and column $c$. The sign is $+1$ when $r+c$ is even and $-1$ otherwise. The input $a$ is a 6-tuple of squared edge lengths (the SqEdges type).
This lemma is the diagonal case $(r,c)=(3,3)$. Sibling lemmas treat the other index pairs; together they feed a single exhaustive agreement theorem over all of $\mathrm{Fin},5\times\mathrm{Fin},5$.
proof idea
Term-mode proof in three steps. Unfold the cofactor and minor definitions so the goal is a signed determinant of a submatrix. Rewrite that submatrix to an explicit $4\times 4$ matrix of edge squares via the dedicated equality cmMinor33_submatrix_eq, then replace its determinant by the precomputed polynomial det_cmMinor33Matrix. Finally simp on the cofactor sign: $3+3=6$ is even, so the sign is $+1$ and the two sides match.
why it matters
This is one cell in the exhaustive case split that proves every tetrahedral CM cofactor equals its polynomial normal form (cmCofactor3_eq_poly). That global agreement is what lets dihedral cosine denominators and their partials be written as named polynomials rather than determinant expressions.
It is also invoked directly by the opposite-diagonal package (cmCofactor3_opposite_diag_eq_poly), which specializes to the diagonal cofactors appearing in tetrahedral dihedral-angle formulas. In the Recognition geometry stack this is infrastructure for explicit calculus on the Cayley–Menger volume and angle layer, not a forcing-chain step (T0–T8), but it is the cofactor analogue of the derivative-polynomial module and closes the gap between matrix determinants and closed-form edge polynomials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.