det_cmMinor01Matrix
plain-language theorem explainer
For any six squared edge lengths of a tetrahedron, the determinant of the explicit 4×4 Cayley–Menger minor matrix at positions (0,1) equals the negative of the named cofactor polynomial at those indices. Dihedral-angle and volume calculus cite this to replace opaque minors by polynomials. The proof unfolds both sides, expands the determinant along the first row, and finishes by ring normalization.
Claim. Let $a:\{0,\ldots,5\}\to\mathbb{R}$ be the six squared edge lengths of a tetrahedron. Form the $4\times 4$ real matrix $M_{01}(a)$ whose first row is $(1,a_0,a_1,a_2)$ and whose remaining rows encode the complementary squared edges with zeros on the diagonal block. Then $\det M_{01}(a)=-P_{01}(a)$, where $P_{01}$ is the explicit cubic polynomial normal form of the Cayley–Menger cofactor at row $0$, column $1$.
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 data are packaged as SqEdges, an abbreviation for maps $\mathrm{Fin},6\to\mathbb{R}$. The target polynomial $P_{rc}$ (cmCofactor3Poly) is defined by a finite case split on the cofactor indices $(r,c)\in\mathrm{Fin},5\times\mathrm{Fin},5$; the $(0,1)$ branch is a concrete cubic combination of the six edge squares. The matrix $M_{01}(a)$ is the concrete $4\times 4$ array obtained by deleting the complementary rows and columns of the bordered Cayley–Menger matrix and writing the remaining entries in terms of $a$.
This lemma is the pure determinant identity that equates $\det M_{01}(a)$ with $-P_{01}(a)$. It sits between the matrix definition and the later identification of the geometric cofactor with that polynomial.
proof idea
Term-style tactic proof. Unfold the matrix definition and the $(0,1)$ branch of the cofactor polynomial. Expand the $4\times 4$ determinant along the first row via Matrix.det_succ_row_zero, pushing the finite sums through Fin.sum_univ_succ and the column-skipping map Fin.succAbove. The resulting multivariate polynomial identity is discharged by ring_nf.
why it matters
Feeds directly into cmCofactor3_01_eq_poly, which proves that the geometric Cayley–Menger cofactor at $(0,1)$ equals the named polynomial: after rewriting the minor as this matrix and applying the present determinant identity, a sign check finishes the argument. That equality is the cofactor analogue of the Cayley–Menger derivative expansions, letting dihedral-angle formulas differentiate polynomials rather than abstract determinants. In the broader Recognition geometry stack, explicit cofactor polynomials support volume and angle calculus on the tetrahedron without leaving the polynomial ring, which is the setting needed for later rigidity and forcing arguments that track edge-length dependence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.