cmCofactor3_23_eq_poly
plain-language theorem explainer
The (2,3) Cayley-Menger cofactor of a tetrahedron equals its explicit polynomial in the six squared edge lengths. Geometry and dihedral-angle calculus cite it when replacing opaque determinants by named polynomials. The proof unfolds the cofactor and minor, rewrites the deleted submatrix to an explicit matrix whose determinant is already computed, and fixes the odd-parity sign.
Claim. For any assignment $a$ of the six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{2,3}(a)$ equals the explicit polynomial normal form of that same cofactor evaluated at $a$.
background
The module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates. Downstream dihedral-angle calculus can then quote named polynomial partials instead of opaque Fréchet derivatives.
The Cayley-Menger matrix of a tetrahedron is the standard $5\times 5$ bordered matrix of squared distances. The minor at $(r,c)$ is the determinant after deleting row $r$ and column $c$; the cofactor is that minor times the sign $(-1)^{r+c}$. Here the indices are $r=2$, $c=3$ (0-based), so the sign is $-1$ because $2+3=5$ is odd.
The squared-edge package is the six-tuple of edge squares. The companion polynomial cmCofactor3Poly is the closed-form expansion of each cofactor in those six coordinates; this lemma is the $(2,3)$ instance of the agreement between the determinant definition and that expansion.
proof idea
Term-mode proof in three steps. Unfold the cofactor as sign times minor, and the minor as the determinant of the submatrix that deletes row 2 and column 3. Rewrite that submatrix via the dedicated equality that identifies it with the explicit minor matrix for indices $(2,3)$, then replace the determinant by the already-proved closed form of that matrix determinant. Finish by simplifying the cofactor sign: $2+3$ is odd, so the sign is $-1$, discharged by a decide on ¬ Even 5.
why it matters
This is one cell in the exhaustive case split that proves full cofactor-polynomial agreement: every $C_{r,c}$ equals its named polynomial. That master theorem is the cofactor analogue of the Cayley-Menger derivative expansions, and is what lets dihedral cosine numerators be treated as concrete polynomials rather than abstract determinants.
It is also invoked directly by the opposite-vertex agreement used for tetrahedral dihedral cosines: each edge's opposite CM-vertex pair is one of a short list of index pairs, and $(2,3)$ appears in that list. In the broader Recognition geometry stack, explicit cofactor polynomials feed curvature and angle calculus on the phi-ladder side without leaving residual fderiv terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.