cmCofactor3_42_eq_poly
plain-language theorem explainer
For any six squared edge lengths, the Cayley-Menger cofactor C_{4,2} equals its named explicit polynomial normal form. The master agreement theorem that covers every index pair cites this case. The proof unfolds the cofactor, rewrites the (4,2)-minor as a concrete 4×4 matrix, substitutes its determinant polynomial, and simplifies the even-parity sign to +1.
Claim. Let $a$ be any assignment of six squared edge lengths of a tetrahedron. Then the Cayley-Menger cofactor $C_{4,2}(a)$ equals the explicit polynomial normal form for the index pair $(4,2)$ evaluated at $a$.
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 cite named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The cofactor $C_{r,c}$ is defined as the sign $(-1)^{r+c}$ times the determinant of the submatrix obtained by deleting row $r$ and column $c$ from the $5\times5$ Cayley-Menger matrix. The companion definition cmCofactor3Poly is a match on $(r,c)$ that returns a fixed multilinear polynomial in the six edge squares.
Upstream, cmMinor42_submatrix_eq identifies the abstract $(4,2)$-submatrix with a concrete named $4\times4$ matrix, and det_cmMinor42Matrix evaluates that matrix's determinant as an explicit polynomial.
proof idea
Unfold the cofactor and minor definitions. Rewrite the abstract submatrix via cmMinor42_submatrix_eq, then replace its determinant by the closed form from det_cmMinor42Matrix. Finish with simp on the cofactor sign: $r+c=4+2=6$ is even, so the sign is $+1$ and the two sides match.
why it matters
This is one cell of the exhaustive case split that proves cmCofactor3_eq_poly: every determinant cofactor of the tetrahedral Cayley-Menger matrix agrees with the explicit polynomial normal form. That master identity is the cofactor analogue of the Cayley-Menger derivative expansions; it lets dihedral-angle formulas differentiate named polynomials rather than opaque matrix minors. In the Recognition geometry stack these cofactors feed volume and angle identities on the tetrahedron, which sit under the $D=3$ spatial forcing (T8) and the eight-tick discrete calculus. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.