det_cmMinor33Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor for cofactor (3,3) equals the named polynomial in the six squared edge lengths. Anyone expanding tetrahedral CM cofactors for dihedral-angle calculus would cite this identity. The proof unfolds both sides, expands the determinant along the first row, and finishes by ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the determinant of the normal-form $4\times 4$ matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & a_0 & a_2 \\ 1 & a_0 & 0 & a_4 \\ 1 & a_2 & a_4 & 0 \end{pmatrix}$$ equals the explicit polynomial normal form for the Cayley–Menger cofactor at row–column indices $(3,3)$.
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 refer to named polynomial partials instead of opaque Fréchet derivatives.
Squared edge lengths of a tetrahedron are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The target polynomial cmCofactor3Poly is the explicit normal form for every CM cofactor, matched on the row and column indices in $\mathrm{Fin},5$. The matrix cmMinor33Matrix is the concrete $4\times 4$ normal form for the diagonal minor used by cofactor $(3,3)$: first row/column of ones with a leading zero, and the remaining $3\times 3$ block filled by the squared edges $a_0,a_2,a_4$ in the usual CM pattern.
proof idea
Term-style tactic proof. Unfold the matrix definition and the target polynomial. Apply the first-row Laplace expansion (Matrix.det_succ_row_zero) together with the standard Fin sum and succAbove simplifications, which reduce the $4\times 4$ determinant to an explicit cubic polynomial in the six edge squares. Finish with ring_nf, which matches that expansion against the hard-coded normal form for indices $(3,3)$.
why it matters
This is one brick in the cofactor-polynomial layer that mirrors CayleyMengerDerivatives. The immediate consumer is cmCofactor3_33_eq_poly, which identifies the abstract CM cofactor at $(3,3)$ with this polynomial by rewriting through the submatrix equality, this determinant identity, and the even-parity cofactor sign. Once every cofactor has such a poly form, partial derivatives needed for dihedral-angle formulae become ordinary polynomial calculus rather than symbolic fderiv terms. No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is touched directly; the result is pure classical geometry scaffolding for later RS geometry modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.