det_cmMinor32Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor for row/column indices (3,2) equals the negative of the named cofactor polynomial in the six squared edge lengths. Anyone equating abstract CM cofactors to polynomial normal forms cites this. The proof unfolds both sides and reduces the 4×4 determinant by row expansion and ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the determinant of the explicit $4\times 4$ minor matrix associated to Cayley–Menger indices $(3,2)$ equals $-P_{3,2}(a)$, where $P_{r,c}$ is the explicit cofactor polynomial in those six squared lengths.
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so downstream dihedral-angle calculus can use named polynomial partials rather than opaque Fréchet derivatives.
Squared edge data are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The target cofactor polynomial $P_{r,c}$ is the match-defined normal form cmCofactor3Poly. The matrix side is the concrete $4\times 4$ array cmMinor32Matrix a with first row $(0,1,1,1)$ and remaining entries drawn from the six squared lengths $a_0,\ldots,a_5$ in the standard Cayley–Menger layout for the $(3,2)$ minor.
This identity is the determinant half of the bridge from that concrete minor to the polynomial table entry at indices $(3,2)$.
proof idea
Unfold the minor matrix and the cofactor polynomial definitions. Expand the $4\times 4$ determinant along the first row via Matrix.det_succ_row_zero, with the finite sums and succAbove reindexing simplified. The resulting multivariate polynomial identity is discharged by ring_nf. No external geometric lemmas are required; it is pure matrix algebra against the tabulated polynomial.
why it matters
Feeds directly into cmCofactor3_32_eq_poly, which proves the abstract Cayley–Menger cofactor at $(3,2)$ equals the explicit polynomial by rewriting through the minor-submatrix equality, this determinant identity, and the cofactor sign. That agreement is part of the module-wide program equating every CM cofactor to a named polynomial so dihedral-angle derivatives can be computed symbolically. Sibling results do the same for other index pairs (e.g. $(3,4)$, $(2,4)$). In the broader Recognition geometry stack this supplies the algebraic substrate for rigid tetrahedral angle calculus on the edge-length ladder, without invoking the forcing chain (T0–T8) directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.