det_cmMinor20Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor for indices (2,0) equals the named degree-4 cofactor polynomial in the six squared edge lengths. Anyone reducing tetrahedral cofactors or dihedral-angle derivatives to edge polynomials would cite it. 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, $\det M_{20}(a)$ equals the explicit cofactor polynomial at row $2$ and column $0$, where $M_{20}(a)$ is the $4\times 4$ matrix with first row $(1,1,1,1)$, second row $(0,a_0,a_1,a_2)$, third row $(a_1,a_3,0,a_5)$, and fourth row $(a_2,a_4,a_5,0)$.
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 live in SqEdges, the type of maps $\mathrm{Fin},6\to\mathbb{R}$. The target polynomial cmCofactor3Poly is the normal form for every $5\times 5$ Cayley–Menger cofactor, given by a large case split on the row and column indices. The matrix side is the concrete $4\times 4$ minor cmMinor20Matrix, whose entries are $0$, $1$, or selected squared edges $a_i$.
This lemma is the pure determinant identity that later equates the geometric cofactor (signed determinant of a submatrix of the Cayley–Menger matrix) to that polynomial normal form.
proof idea
Term-style tactic proof. Unfold the matrix definition and the target polynomial, then apply the first-row determinant expansion (Matrix.det_succ_row_zero) together with the standard Fin sum and succAbove simplifications. The resulting multivariate polynomial identity is discharged by ring_nf. No external geometric lemmas are required; the equality is purely algebraic.
why it matters
Feeds directly into cmCofactor3_20_eq_poly, which rewrites the geometric cofactor cmCofactor3 a 2 0 as the polynomial cmCofactor3Poly 2 0 a after identifying the submatrix and inserting the cofactor sign (even for index pair $(2,0)$). That equality is one cell of the cofactor-polynomial agreement table used throughout the geometry layer.
In the broader Recognition stack this sits in the Cayley–Menger geometry supporting rigid tetrahedral configurations and dihedral calculus; it is the cofactor analogue of the derivative expansions in CayleyMengerDerivatives. It does not itself touch the forcing chain (T0–T8), but supplies the algebraic substrate for volume and angle identities that later geometry and mass-ladder arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.