cmCofactor3_13_eq_poly
plain-language theorem explainer
The (1,3) cofactor of the tetrahedral Cayley-Menger matrix equals its explicit polynomial in the six squared edge lengths. Anyone deriving dihedral-angle formulas from CM determinants cites this case identity. The proof unfolds the cofactor, rewrites the deleted-row minor via a named submatrix equality and its closed determinant, then simplifies the parity sign.
Claim. For any assignment $a$ of the six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{1,3}(a)$ equals the named explicit polynomial $\mathrm{Poly}_{1,3}(a)$ in those six coordinates.
background
The module expands every cofactor of the $5\times 5$ tetrahedral Cayley-Menger matrix into a concrete polynomial in the six squared edge coordinates (SqEdges). Downstream dihedral-angle calculus can then differentiate named polynomials instead of opaque Fréchet derivatives of determinants.
A Cayley-Menger cofactor is $C_{r,c}=(-1)^{r+c},M_{r,c}$, where $M_{r,c}$ is the determinant of the submatrix obtained by deleting row $r$ and column $c$. The sign is realized as a real $\pm 1$ by parity of $r+c$. The companion object cmCofactor3Poly is the hand-expanded polynomial normal form for each pair $(r,c)$.
This lemma treats the single index pair $(1,3)$. For that pair the exponent $1+3=4$ is even, so the sign is $+1$.
proof idea
Unfold the cofactor and minor definitions. Rewrite the deleted submatrix by the sibling equality that identifies the $(1,3)$-minor with a concrete $4\times 4$ matrix of edge squares, then replace its determinant by the already-proved closed form det_cmMinor13Matrix. Finish with simp on the sign definition together with the decidable fact that $4$ is even, which forces the sign factor to $1$ and matches the polynomial side.
why it matters
The lemma is one of the twenty-five case identities assembled by cmCofactor3_eq_poly, which asserts polynomial agreement for every cofactor of the tetrahedral Cayley-Menger matrix. It is also invoked by cmCofactor3_opposite_eq_poly, the specialization to the six opposite-vertex pairs that appear as numerators of tetrahedral dihedral cosines.
Those dihedral identities sit in the geometry layer that feeds Recognition Science volume and angle calculus; explicit polynomial cofactors let later modules differentiate and specialize without re-expanding determinants. The result is pure Euclidean geometry scaffolding, not a forcing-chain step, but it removes opaque matrix minors from every downstream CM-based formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.