cmCofactor3_20_eq_poly
plain-language theorem explainer
The (2,0)-cofactor of the tetrahedral Cayley-Menger matrix equals the named explicit polynomial in the six squared edge lengths. Cite this when expanding CM minors into coordinate polynomials for dihedral or volume calculus. The proof unfolds the cofactor, identifies the deleted 4×4 submatrix, and matches its determinant (with even-parity sign +1) to the stored normal form.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{2,0}(a)$ equals the explicit polynomial normal form prescribed for row-column indices $(2,0)$.
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 cofactor $C_{r,c}$ is defined as the sign $(-1)^{r+c}$ times the determinant of the matrix obtained by deleting row $r$ and column $c$ from the $5\times 5$ Cayley-Menger matrix. The companion definition cmCofactor3Poly stores, by case on $(r,c)$, a fixed multilinear polynomial intended as that cofactor's normal form.
Upstream, cmMinor20_submatrix_eq identifies the concrete deleted submatrix at $(2,0)$ with a named $4\times 4$ matrix whose determinant has already been expanded (det_cmMinor20Matrix).
proof idea
Unfold the cofactor and minor definitions so the goal is a signed determinant of a deleted submatrix. Rewrite that submatrix via cmMinor20_submatrix_eq and replace its determinant by the precomputed expansion det_cmMinor20Matrix. Finish with simp on the cofactor sign: $2+0$ is even, so the sign is $+1$, and both sides match.
why it matters
This is one cell of the case grid that discharges the master agreement theorem cmCofactor3_eq_poly: every determinant cofactor of the tetrahedral Cayley-Menger matrix equals its explicit polynomial normal form. That master result is the cofactor analogue of the Cayley-Menger derivative expansions; it lets dihedral-angle and volume identities work with named polynomials rather than opaque minors.
In the broader Recognition geometry stack, explicit CM cofactors feed rigid-simplex calculus (edge-length gradients, dihedral constraints) used when spatial dimension $D=3$ and eight-tick discrete structure are already forced. No open scaffold remains here: the cell is fully proved and only needs to be assembled with its siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.