cmMinor02Matrix
plain-language theorem explainer
Explicit 4×4 real matrix whose entries are constants and the six squared edge lengths of a tetrahedron, realizing the (0,2) Cayley–Menger minor. Geometers and anyone computing tetrahedral cofactors or dihedral-angle partials cite it as the concrete matrix whose determinant is the named cofactor polynomial. The body is a literal matrix literal; no proof.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ matrix $$M_{02}(a)=\begin{pmatrix}1&0&a_1&a_2\\1&a_0&a_3&a_4\\1&a_1&0&a_5\\1&a_2&a_5&0\end{pmatrix}.$$
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 SqEdges: a map from Fin 6 to $\mathbb{R}$. The ambient object is the bordered Cayley–Menger matrix of a tetrahedron (five rows/columns after the usual 0-1 border). Deleting row 0 and column 2 yields a $4\times 4$ minor; the present definition writes that minor with every entry expanded in the six edge squares.
Sibling definitions do the same for the other index pairs used by the third cofactor row. Downstream lemmas identify this literal matrix with Matrix.submatrix of the full Cayley–Menger matrix and equate its determinant to the named cofactor polynomial.
proof idea
Pure definition: a single matrix literal of type Matrix (Fin 4) (Fin 4) ℝ. Entries are the constants 0 and 1 together with the six components of the squared-edge vector a, placed exactly where the (0,2) minor of the tetrahedral Cayley–Menger matrix puts them. No tactics, no lemmas.
why it matters
Supplies the concrete matrix that two immediate theorems consume. cmMinor02_submatrix_eq proves the literal equals the abstract submatrix obtained by deleting row 0 and column 2 from the full Cayley–Menger matrix. det_cmMinor02Matrix then shows that the determinant equals the explicit cofactor polynomial cmCofactor3Poly 0 2, via expansion along the first row and ring normalization.
Those equalities let the rest of the cofactor-polynomial module treat dihedral and volume derivatives as ordinary multivariate polynomials in edge squares, which is the module’s stated purpose. In the broader Recognition geometry stack this is scaffolding for exact (non-numeric) curvature and angle identities on the tetrahedron, not a forcing-chain landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.