cmCofactor3_44_eq_poly
plain-language theorem explainer
The (4,4) Cayley–Menger cofactor of a tetrahedron equals the named explicit polynomial in the six squared edge lengths. Anyone computing tetrahedral dihedral cosines or their derivatives from CM data cites this identity. The proof unfolds the cofactor, replaces the deleted submatrix by its coordinate form, evaluates that 4×4 determinant, and fixes the sign (+1) because 4+4 is even.
Claim. For any assignment $a$ of the six squared edge lengths of a tetrahedron, the Cayley–Menger cofactor $C_{4,4}(a)$ equals the explicit polynomial $\mathrm{Poly}_{4,4}(a)$ in those six coordinates.
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so dihedral-angle calculus can use named polynomial partials instead of opaque Fréchet derivatives.
The ambient object is the $5\times 5$ Cayley–Menger matrix built from squared edge lengths $a\in\mathrm{SqEdges}$. The minor obtained by deleting row $r$ and column $c$ is $\mathrm{cmMinor3},a,r,c$; the cofactor is $C_{r,c}=(-1)^{r+c}$ times that minor. The companion definition $\mathrm{cmCofactor3Poly},r,c$ is the fully expanded polynomial normal form of the same quantity.
Index pair $(4,4)$ is one of the diagonal cofactors that appear in denominators of tetrahedral dihedral cosines (via opposite CM vertices). Agreement at this single entry is a building block for the global statement that every cofactor matches its polynomial.
proof idea
Term-mode proof by direct expansion. Unfold $C_{4,4}$ and the minor definition, then rewrite the deleted submatrix via $\mathrm{cmMinor44_submatrix_eq}$ and replace its determinant by the precomputed identity $\mathrm{det_cmMinor44Matrix}$. Finish with $\mathrm{simp}$ on the cofactor sign: $4+4=8$ is even, so the sign factor is $+1$ and the two sides match.
why it matters
Feeds the master agreement theorem $\mathrm{cmCofactor3_eq_poly}$, which cases on all $(r,c)\in\mathrm{Fin},5\times\mathrm{Fin},5$ and dispatches each cell to a sibling lemma of this form. Also feeds $\mathrm{cmCofactor3_opposite_diag_eq_poly}$, the diagonal-only package used by tetrahedral dihedral cosine denominators.
In the Recognition geometry stack this is pure algebraic scaffolding: once every cofactor is a named polynomial, partial derivatives of dihedral cosines become ordinary polynomial calculus rather than abstract $fderiv$ terms (the cofactor analogue of CayleyMengerDerivatives). No forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; the result is local Euclidean tetrahedron algebra that later angle and volume identities rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.