cmMinor11Matrix
plain-language theorem explainer
Normal-form 4×4 real matrix for the principal minor underlying the (1,1) tetrahedral Cayley-Menger cofactor, written in the six squared edge lengths. Cited by anyone expanding CM cofactors as explicit polynomials or feeding dihedral-angle calculus. The body is a matrix literal: border of ones, zeros on the 3×3 diagonal block, and edge squares a₃,a₄,a₅ off-diagonal.
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 & 0 & a(3) & a(4) \\ 1 & a(3) & 0 & a(5) \\ 1 & a(4) & a(5) & 0 \end{pmatrix}.$$ This is the normal form of the diagonal minor used by the $(1,1)$ Cayley-Menger cofactor.
background
The 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 lengths are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$): the six edge squares of a tetrahedron. The ambient object is the bordered Cayley-Menger matrix whose cofactors encode volume and face geometry; the $(1,1)$ cofactor is (up to sign) the determinant of the principal minor obtained by deleting the corresponding row and column.
This definition freezes that minor in a fixed coordinate order so later lemmas can equate it to a submatrix extraction and evaluate its determinant as a named polynomial.
proof idea
Pure definition: a $4\times 4$ matrix literal. First row/column is the standard CM border $(0,1,1,1)$; the remaining $3\times 3$ block has zeros on the diagonal and the three squared edges $a(3),a(4),a(5)$ in the off-diagonal slots that survive after deleting index 1 from the full $5\times 5$ CM matrix. No lemmas or tactics.
why it matters
Gives a concrete handle on the $(1,1)$ CM minor so the module can prove two facts: (i) it equals the submatrix of the full CM matrix after deleting row/column 1 via succAbove, and (ii) its determinant equals the explicit cofactor polynomial cmCofactor3Poly 1 1. Those equalities let dihedral-angle derivatives be written as ordinary partials of named polynomials rather than abstract fderiv terms, which is the module's stated purpose (cofactor analogue of Cayley-MengerDerivatives). Sibling minors (23, 24, 34, …) follow the same pattern for the remaining cofactors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.