cmCofactor3_30_eq_poly
plain-language theorem explainer
The (3,0) cofactor of the tetrahedral Cayley-Menger matrix equals the named explicit polynomial in the six squared edge lengths. Anyone differentiating dihedral angles or volumes via cofactors cites this identity. The proof unfolds the cofactor, rewrites the deleted submatrix to a concrete 4x4 matrix, evaluates its determinant, and fixes the sign (-1)^{3+0}=-1.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{3,0}(a)$ equals the explicit polynomial normal form $\mathrm{Poly}_{3,0}(a)$ in those six coordinates.
background
The module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates, so downstream dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The Cayley-Menger matrix is the standard $5\times5$ bordered matrix of squared distances. The minor $M_{r,c}$ is the determinant after deleting row $r$ and column $c$; the cofactor is $C_{r,c}=(-1)^{r+c}M_{r,c}$. The target normal form cmCofactor3Poly is a match on $(r,c)$ giving a concrete multilinear polynomial in the six edges.
Upstream, cmMinor30_submatrix_eq identifies the abstract submatrix (delete row 3, column 0) with a named $4\times4$ matrix of edge entries, and det_cmMinor30Matrix evaluates that determinant as a polynomial.
proof idea
Unfold the cofactor and minor definitions so the goal is a signed determinant of a submatrix of the Cayley-Menger matrix. Rewrite that submatrix via cmMinor30_submatrix_eq to the concrete matrix cmMinor30Matrix, then replace its determinant by the already-computed polynomial det_cmMinor30Matrix. Finally simp with the cofactor-sign definition and the fact that $3$ is odd, so $(-1)^{3+0}=-1$, matching the sign baked into the normal form.
why it matters
This is one cell in the exhaustive case split that proves cmCofactor3_eq_poly: every determinant cofactor of the tetrahedral Cayley-Menger matrix agrees with its explicit polynomial normal form. That master identity is the cofactor analogue of the Cayley-Menger derivative expansions; dihedral-angle and volume calculus in the geometry stack can then differentiate named polynomials rather than opaque matrix determinants.
In the broader Recognition geometry layer, explicit cofactor polynomials feed rigid-body and simplex identities used when matching continuum geometry to the discrete eight-tick / $D=3$ forcing chain. The declaration itself is pure classical multilinear algebra; its value is mechanical completeness of the $(r,c)$ table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.