cmCofactor3_43_eq_poly
plain-language theorem explainer
For any six squared edge lengths of a tetrahedron, the (4,3)-cofactor of the 5×5 Cayley-Menger matrix equals the named explicit polynomial in those edges. Geometers computing dihedral-angle derivatives cite this when they need a closed form instead of a submatrix determinant. The proof unfolds the cofactor, substitutes the explicit 4×4 minor matrix, evaluates its determinant, and inserts the sign (−1)^{4+3}=−1.
Claim. For every assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{4,3}(a)$ equals the explicit polynomial normal form for row-column indices $(4,3)$ 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 quote named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges (maps Fin 6 → ℝ). The 5×5 Cayley-Menger matrix is built from those edges; its minor deleting row $r$ and column $c$ is the determinant of the corresponding submatrix, and the cofactor is that minor times the sign $(-1)^{r+c}$. The target polynomial form cmCofactor3Poly is a large case-split giving a closed multilinear expression for each pair $(r,c)$.
Upstream, the submatrix obtained by deleting row 4 and column 3 is identified with an explicit matrix cmMinor43Matrix, whose determinant is already expanded as a polynomial identity.
proof idea
Unfold the cofactor into sign times minor, and the minor into a submatrix determinant. Rewrite the submatrix via the equality that replaces the deleted-row/column slice by the named 4×4 matrix, then replace that determinant by its precomputed polynomial expansion. Finish by simplifying the cofactor sign: $4+3=7$ is odd, so the sign is $-1$, discharged by a decide proof that 7 is not even.
why it matters
This is one cell in the exhaustive case grid that proves every Cayley-Menger cofactor equals its polynomial normal form. The parent theorem cases on all pairs $(r,c)\in\mathrm{Fin},5\times\mathrm{Fin},5$ and invokes the corresponding cell lemma; the $(4,3)$ branch is exactly this result.
Once all cofactors are polynomial, partial derivatives with respect to squared edges become ordinary polynomial calculus, which is the stated purpose of the module (cofactor analogue of the Cayley-Menger derivative layer). That infrastructure supports hinge-aware Regge and dihedral geometry downstream, without leaving determinant black boxes in the derivative terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.