cmCofactor3_02_eq_poly
plain-language theorem explainer
The (0,2) cofactor of the tetrahedral Cayley-Menger matrix equals a fixed explicit polynomial in the six squared edge lengths. Downstream dihedral-angle calculus cites this when replacing opaque minors by named polynomials. The proof matches the deleted-row submatrix to a hand-built 4×4 matrix, evaluates its determinant, and multiplies by the cofactor sign (+1).
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{0,2}(a)$ equals the explicit polynomial $a_2 a_3 a_5 - a_2^2 a_3 + a_1 a_4 a_5 - 2 a_1 a_2 a_5 + a_1 a_2 a_4 + a_1 a_2 a_3 - a_1^2 a_4 - a_0 a_5^2 + a_0 a_2 a_5 + a_0 a_1 a_5$.
background
The module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates, so dihedral-angle calculus can quote named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The $5\times 5$ Cayley-Menger matrix is built from those six lengths; the minor at $(r,c)$ is the determinant after deleting row $r$ and column $c$, and the cofactor is that minor times the sign $(-1)^{r+c}$. The target polynomial form is the $(0,2)$ branch of the match that lists a closed-form expression for every index pair.
Upstream, the submatrix obtained by deleting row 0 and column 2 is identified entrywise with a concrete $4\times 4$ matrix whose determinant has already been expanded by hand.
proof idea
Unfold the cofactor and minor definitions. Rewrite the deleted-row submatrix via the entrywise identity that equates it to the hand-built $(0,2)$ minor matrix, then replace that matrix's determinant by its precomputed polynomial expansion. Finish by simplifying the cofactor sign: $0+2$ is even, so the sign is $+1$, and the two sides match.
why it matters
This is one cell in the case split that proves every tetrahedral Cayley-Menger cofactor agrees with its explicit polynomial normal form. The parent theorem discharges all $(r,c)\in\mathrm{Fin},5\times\mathrm{Fin},5$ by fin_cases and invokes this lemma for the $(0,2)$ branch. That agreement is the cofactor analogue of the Cayley-Menger derivative expansions: once cofactors are polynomials, partials needed for dihedral angles become ordinary algebraic derivatives rather than abstract fderiv terms. In the broader geometry stack it keeps volume and angle identities fully algebraic in the six edge squares.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.