cmCofactor3_32_eq_poly
plain-language theorem explainer
The (3,2) cofactor of the tetrahedral Cayley-Menger matrix equals its explicit polynomial in the six squared edge lengths. Cited by anyone reducing dihedral or volume derivatives to named edge polynomials. Proof unfolds the cofactor, swaps in the concrete deleted-row matrix, evaluates its determinant, and inserts the odd-parity sign -1.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{3,2}(a)$ (signed minor deleting row 3 and column 2 of the $5\times 5$ bordered distance matrix) equals the corresponding explicit polynomial normal form in those six coordinates.
background
This 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 edges 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 standard $5\times 5$ Cayley-Menger matrix. The table cmCofactor3Poly stores the fully expanded polynomial for each pair $(r,c)$.
The immediate upstream facts are the identification of the $(3,2)$-deleted submatrix with a named $4\times 4$ matrix, and the evaluation of that matrix's determinant as a polynomial in the edge squares.
proof idea
Unfold the cofactor and minor definitions to expose $\mathrm{sign}(3,2)\cdot\det(\mathrm{submatrix})$. Rewrite the submatrix via the equality that matches it to the concrete matrix cmMinor32Matrix, then replace the determinant by its already-computed polynomial expansion. Finish by simplifying the sign: $3+2=5$ is odd, so the cofactor sign is $-1$ (discharged by decide on \neg\mathrm{Even}\,5).
why it matters
One cell in the exhaustive case split that proves every tetrahedral Cayley-Menger cofactor agrees with the explicit polynomial table. The parent theorem cmCofactor3_eq_poly runs fin_cases on both indices and invokes this lemma for the $(3,2)$ slot; its doc-comment states that the normal form "agrees with every determinant cofactor of the tetrahedral Cayley-Menger matrix."
That master agreement is what lets dihedral-angle and volume calculus in the geometry layer work with named polynomial partials rather than opaque derivative terms. It is infrastructure for RS geometric identities (edge-ladder volumes, angle constraints), not itself a step of the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.