cmMinor40Matrix
plain-language theorem explainer
Explicit 4×4 matrix whose entries are 0, 1, or the six squared edge lengths of a tetrahedron, realizing the Cayley–Menger minor that deletes row 4 and column 0. Downstream cofactor and dihedral calculus cite it as a named polynomial matrix rather than an opaque submatrix. The body is a literal matrix literal; no proof work.
Claim. For squared edge lengths $a\colon\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ real matrix $$\begin{pmatrix}1&1&1&1\\0&a_0&a_1&a_2\\a_0&0&a_3&a_4\\a_1&a_3&0&a_5\end{pmatrix}.$$
background
The ambient module expands every tetrahedral Cayley–Menger cofactor into 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, an abbreviation for maps $\mathrm{Fin},6\to\mathbb{R}$. The full $5\times 5$ bordered Cayley–Menger matrix of a tetrahedron has a first row/column of ones and off-diagonal blocks filled by those six squared lengths; cofactors are determinants of $4\times 4$ minors obtained by deleting one row and one column.
This definition writes the concrete minor that deletes index 4 from the row set and index 0 from the column set, with zeros on the geometric diagonal blocks and the six edge squares placed in the standard CM ordering.
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$, arranged exactly as the $(4,0)$-minor of the bordered Cayley–Menger matrix. No lemmas or tactics are invoked.
why it matters
Named minors let the cofactor polynomials be computed by ordinary $4\times 4$ determinants rather than by abstract Matrix.submatrix expressions. Immediately downstream, cmMinor40_submatrix_eq proves the literal equals the corresponding submatrix of the full CM matrix, and det_cmMinor40Matrix identifies its determinant with the explicit cofactor polynomial cmCofactor3Poly 4 0. Those identities feed the module’s larger program: every tetrahedral CM cofactor becomes a concrete polynomial in the six edge squares, enabling symbolic differentiation for dihedral angles without residual fderiv opacity. In the Recognition geometry stack this is bookkeeping infrastructure for volume and angle identities on the phi-ladder, not a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.