cmMinor31Matrix
plain-language theorem explainer
Explicit 4×4 matrix whose entries are the squared edge lengths of a tetrahedron (plus the usual Cayley–Menger border of 0s and 1s), corresponding to the minor that deletes row 3 and column 1 of the 5×5 Cayley–Menger matrix. Anyone computing tetrahedral cofactors or dihedral-angle polynomials cites it. The body is a pure matrix literal in the six squared-edge coordinates.
Claim. Given squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ real matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & a_0 & a_1 & a_2 \\ 1 & 0 & a_3 & a_4 \\ 1 & a_4 & a_5 & 0 \end{pmatrix}.$$
background
The ambient module expands every cofactor of the tetrahedral Cayley–Menger matrix into an explicit polynomial in the six squared edge lengths. Downstream dihedral-angle calculus can then quote named 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×5 Cayley–Menger matrix (imported from the Cayley–Menger matrix module) borders a Gram-like block of those squared lengths with a row and column of ones and a zero corner; its minors are the classical volume and cofactor ingredients.
This definition simply writes out one such minor by hand: the submatrix obtained by striking row index 3 and column index 1.
proof idea
Pure definition: the right-hand side is a concrete $4\times 4$ matrix literal built from the constant border $(0,1,1,1)$ and the six squared-edge coordinates $a_0,\ldots,a_5$ placed in the standard Cayley–Menger pattern for that minor. No lemmas or tactics are involved.
why it matters
It is the named carrier for the $(3,1)$-cofactor of the tetrahedral Cayley–Menger matrix. The immediate consumers are the equality theorem that identifies it with the corresponding submatrix of the full 5×5 matrix, and the determinant theorem that equates $\det$ of this matrix with the explicit cofactor polynomial cmCofactor3Poly 3 1. Those identities let later dihedral and volume calculus work with ring-normalized polynomials rather than abstract minors. Within Recognition geometry this is scaffolding for exact edge-to-angle maps on the tetrahedron, not a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.