cmMinor30Matrix
plain-language theorem explainer
Explicit 4×4 real matrix in the six squared edge lengths of a tetrahedron, equal (by a sibling lemma) to the Cayley–Menger minor that deletes row 3 and column 0. Anyone computing tetrahedral cofactors or dihedral-angle partials as named polynomials cites it. The body is a matrix literal; no proof work.
Claim. Given squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ matrix $$\begin{pmatrix} 1 & 1 & 1 & 1 \\ 0 & a(0) & a(1) & a(2) \\ a(0) & 0 & a(3) & a(4) \\ a(2) & a(4) & a(5) & 0 \end{pmatrix}.$$
background
The 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 ambient object is the bordered Cayley–Menger matrix of a tetrahedron; cofactors of that matrix control volumes and dihedral angles.
This definition isolates the concrete $4\times 4$ block obtained by deleting one border row and one border column. Sibling definitions do the same for other index pairs (e.g. minors 34 and 24).
proof idea
Definition only: a single matrix literal whose entries are the constants $0,1$ and the six squared-edge coordinates $a(0),\ldots,a(5)$ in the standard Cayley–Menger layout for the $(3,0)$-minor. No tactics or lemmas are invoked at the definition site.
why it matters
It is the named carrier for the $(3,0)$-cofactor polynomial. The equality theorem cmMinor30_submatrix_eq identifies it with the corresponding submatrix of the full Cayley–Menger matrix, and det_cmMinor30Matrix proves that its determinant equals $-$ the explicit cofactor polynomial at indices $(3,0)$.
Those two results let downstream geometry replace matrix-minor bookkeeping by ring arithmetic on a fixed polynomial in the six edges. In the broader Recognition geometry stack this is scaffolding for dihedral-angle derivatives and volume identities that feed continuum limits, not a forcing-chain landmark itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.