cmMinor41Matrix
plain-language theorem explainer
Explicit 4×4 real matrix in the six squared edge lengths of a tetrahedron, realizing the minor that deletes row 4 and column 1 of the 5×5 Cayley–Menger matrix. Geometry and dihedral-angle calculus cite it when expanding the corresponding cofactor as a named polynomial. The body is a direct matrix literal; no proof is required.
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_1 & a_2 \\ 1 & 0 & a_3 & a_4 \\ 1 & a_3 & 0 & a_5 \end{pmatrix}.$$ It is the concrete minor used for the $(4,1)$-cofactor of the tetrahedral Cayley–Menger matrix.
background
The ambient 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: maps $\mathrm{Fin},6\to\mathbb{R}$. The full $5\times 5$ Cayley–Menger matrix (bordered by a row/column of ones and a zero corner) has determinant proportional to the squared volume; its cofactors enter classical formulae for face areas and dihedral angles.
This definition freezes the minor obtained by deleting the last row index and the second column index, written out entrywise in the six edge squares so later determinant and submatrix identities can unfold by pure algebra.
proof idea
Pure definition: a $4\times 4$ matrix literal. Entries are the constant border $0,1$ together with the six squared lengths $a_0,\ldots,a_5$ placed exactly where the corresponding Cayley–Menger submatrix puts them. No lemmas or tactics are involved.
why it matters
It is the named carrier for the $(4,1)$-cofactor expansion. Immediately downstream, a submatrix identity proves this literal equals the actual minor of the full Cayley–Menger matrix after deleting those indices, and a determinant theorem shows $\det$ of the literal equals the negative of the explicit cofactor polynomial at indices $(4,1)$. Those two facts let dihedral-angle derivatives work with ring-normalized polynomials rather than symbolic minors. Sibling minors (e.g. $(3,4)$, $(2,4)$, $(2,3)$) play the same role for the other cofactors in the same generated suite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.