cmMinor21Matrix
plain-language theorem explainer
Explicit 4×4 matrix for the (2,1)-minor of the bordered Cayley–Menger matrix of a tetrahedron, written in the six squared edge lengths. Cofactor and dihedral-angle developments cite it so determinants and partials refer to a named array rather than an opaque submatrix. The body is a matrix literal; no algebraic derivation is required.
Claim. Given squared edge lengths $a\colon\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, the $(2,1)$-minor matrix is the $4\times 4$ array $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & a_0 & a_1 & a_2 \\ 1 & a_3 & 0 & a_5 \\ 1 & a_4 & a_5 & 0 \end{pmatrix}.$$ It is the concrete matrix obtained by deleting row 2 and column 1 from the $5\times 5$ bordered Cayley–Menger matrix.
background
The module expands every tetrahedral Cayley–Menger cofactor as an explicit polynomial in the six squared edge coordinates, so dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives.
Squared edge data are packaged as a map $a$ from $\mathrm{Fin},6$ to $\mathbb{R}$ (the six edges of a tetrahedron). The ambient object is the usual $5\times 5$ bordered Cayley–Menger matrix whose determinant (up to scale) is $288 V^2$. Cofactors of that matrix enter classical formulae for face areas and dihedral angles.
This definition freezes the particular minor that deletes row index 2 and column index 1, writing the resulting $4\times 4$ block by hand in the edge coordinates $a_0,\ldots,a_5$.
proof idea
Pure definition: the right-hand side is a matrix literal (!![ ... ]) with constant border row/column and interior entries drawn from the six squared lengths. No lemmas are applied; equality to the abstract submatrix is proved separately by exhaustive fin_cases.
why it matters
Supplies the named matrix used by the submatrix-identity theorem (the minor equals the corresponding submatrix of the full Cayley–Menger matrix) and by the determinant identity that equates its det to the signed explicit cofactor polynomial of bidegree $(2,1)$. Those two results let later dihedral and volume calculus work with ring-normalized polynomials rather than Matrix.submatrix and fderiv. In the Recognition geometry stack this is scaffolding for explicit angle derivatives on the phi-ladder edge data, not a physical claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.