cmMinor12Matrix
plain-language theorem explainer
Normal-form 4×4 real matrix for the minor underlying the (1,2) cofactor of a tetrahedron’s Cayley–Menger matrix, written in the six squared edge lengths. Anyone expanding dihedral-angle derivatives into named cofactor polynomials cites it. The body is a direct matrix literal, not a derived construction.
Claim. Given squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ matrix $$\begin{pmatrix}0&1&1&1\\1&a_0&a_3&a_4\\1&a_1&0&a_5\\1&a_2&a_5&0\end{pmatrix}.$$ This is the normal form of the minor used by the $(1,2)$ Cayley–Menger cofactor.
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 name 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 ambient object is the bordered Cayley–Menger matrix of a tetrahedron; cofactors of that matrix control volumes and dihedral angles via classical determinant identities.
The present matrix is the concrete $4\times 4$ block obtained (up to the usual sign conventions) by deleting the row and column that produce the $(1,2)$ cofactor. Its entries are either constants $0,1$ or the six squared lengths $a_0,\ldots,a_5$ placed in the standard edge-index pattern.
proof idea
Pure definition by matrix literal. The four rows are written with the !![\ldots] notation: first row $(0,1,1,1)$, then the three rows that interleave the constant border column of ones with the squared-edge entries $a_0,a_1,a_2,a_3,a_4,a_5$ in the positions required by the $(1,2)$ minor. No lemmas are invoked.
why it matters
Supplies the named normal form that two immediate siblings rely on. The equality theorem identifies this matrix with the concrete submatrix of the full $5\times 5$ Cayley–Menger matrix after deleting row 1 and column 2. The determinant theorem then evaluates $\det$ of the normal form and shows it equals the negative of the already-expanded cofactor polynomial of bidegree $(1,2)$. Together they close the bridge from abstract cofactor extraction to an explicit polynomial in the six edge squares, which is exactly the infrastructure the module advertises for dihedral-angle calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.