cmMinor20Matrix
plain-language theorem explainer
Explicit 4×4 real matrix for the (2,0) minor of the tetrahedral Cayley–Menger matrix, written in the six squared edge lengths. Anyone expanding CM cofactors into named polynomials (for dihedral-angle derivatives) cites this matrix. The body is a literal matrix constructor, not a proof.
Claim. For squared edge lengths $a\colon\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ matrix $$M_{20}(a)=\begin{pmatrix}1&1&1&1\\0&a_0&a_1&a_2\\a_1&a_3&0&a_5\\a_2&a_4&a_5&0\end{pmatrix}.$$
background
The ambient module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates. Downstream dihedral-angle calculus can then name polynomial partials instead of opaque Fréchet derivatives.
SqEdges is the type of squared edge lengths of a tetrahedron, indexed by Fin 6. The full 5×5 Cayley–Menger matrix cmMatrix3 is built from those six values; its cofactors control volumes and dihedral geometry.
The index pair (2,0) means: delete row 2 and column 0 of that 5×5 matrix. The resulting 4×4 block is written out entrywise above so that its determinant can be expanded by hand into a named polynomial.
proof idea
Pure definition: a matrix literal !![...] with constant first row of ones and the remaining entries filled by the six squared-edge coordinates (and structural zeros). No tactics or lemmas are invoked at the definition site. Equality to the abstract submatrix and the determinant expansion are proved in the two immediate downstream theorems.
why it matters
This matrix is the concrete carrier for the (2,0) cofactor polynomial. Downstream, cmMinor20_submatrix_eq identifies it with Matrix.submatrix (cmMatrix3 a) (Fin.succAbove 2) (Fin.succAbove 0), and det_cmMinor20Matrix proves that its determinant equals the named polynomial cmCofactor3Poly 2 0 a (via row expansion and ring_nf).
Those named cofactor polynomials are the cofactor analogue of CayleyMengerDerivatives: they let dihedral-angle identities and partials be stated algebraically in the six edge squares rather than as opaque derivatives of a determinant. In the broader Recognition geometry stack this supplies the explicit algebraic feedstock for volume and angle calculus on tetrahedra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.