cmCofactor3_34_eq_poly
plain-language theorem explainer
The (3,4) Cayley–Menger cofactor of a tetrahedron equals a named explicit polynomial in the six squared edge lengths. Anyone computing dihedral cosines or edge-0 numerators cites this identity. The proof unfolds the cofactor, rewrites the deleted submatrix to a fixed 4×4 form, evaluates its determinant, and fixes the sign (−1)^{3+4}=−1.
Claim. For any assignment $a$ of the six squared edge lengths of a tetrahedron, the Cayley–Menger cofactor $C_{3,4}(a)$ equals the explicit polynomial $\mathrm{Poly}_{3,4}(a)$ in those six coordinates. (Indices $3,4$ label the opposite-vertex pair for edge $0$ in the $5\times 5$ bordered Cayley–Menger matrix.)
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$ bordered Cayley–Menger matrix built from squared edge lengths $a\in\mathbb{R}^6$. The minor $\mathrm{cmMinor3},a,r,c$ is the determinant after deleting row $r$ and column $c$; the cofactor is $C_{r,c}=(-1)^{r+c}$ times that minor. The sibling definition $\mathrm{cmCofactor3Poly},r,c$ is the closed-form polynomial that is claimed to match $C_{r,c}$.
For the pair $(3,4)$, the module supplies a concrete $4\times 4$ matrix normal form (cmMinor34Matrix), a proof that the submatrix equals that form, and an evaluated determinant identity. The sign factor is $(-1)^{3+4}=-1$ because $7$ is odd.
proof idea
Unfold the cofactor and minor definitions so the goal is a signed determinant of a submatrix of the Cayley–Menger matrix. Rewrite that submatrix via cmMinor34_submatrix_eq to the fixed matrix cmMinor34Matrix. Replace the determinant by the closed form det_cmMinor34Matrix. Finish with simp on the cofactor sign, using decide to record that $3+4=7$ is not even, so the sign is $-1$. The result is definitional equality with cmCofactor3Poly 3 4.
why it matters
This is one cell of the full cofactor–polynomial dictionary. It is the first case in cmCofactor3_opposite_eq_poly, which states polynomial agreement for every numerator cofactor used by tetrahedral dihedral cosines (edge $0$ maps to opposite vertices $(3,4)$). It is also a branch of the exhaustive fin_cases proof of cmCofactor3_eq_poly, the global statement that every $C_{r,c}$ equals its polynomial normal form.
Downstream differentiation uses it directly: hasDerivAt_cmCofactor3_34_along_coord rewrites the determinant cofactor along a coordinate line to the polynomial, then quotes the polynomial’s closed-form partial. That path is the cofactor analogue of CayleyMengerDerivatives and feeds geometric calculus on the tetrahedron (dihedral angles, volume sensitivities) inside the Recognition geometry stack. No forcing-chain landmark (T5–T8) is touched; the result is pure classical CM algebra supporting later continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.