cmMinor44_submatrix_eq
plain-language theorem explainer
The (4,4) minor of the tetrahedral Cayley-Menger matrix, formed by deleting the last row and column, equals an explicit 4×4 normal-form matrix in the six squared edge lengths. Anyone expanding the (4,4) cofactor as a polynomial cites this identification. The proof is matrix extensionality followed by exhaustive Fin-4 case analysis and reflexivity.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the submatrix of the $5\times 5$ Cayley-Menger matrix of $a$ obtained by deleting row $4$ and column $4$ equals the explicit $4\times 4$ matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & a_0 & a_1 \\ 1 & a_0 & 0 & a_3 \\ 1 & a_1 & a_3 & 0 \end{pmatrix}.$$
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 derivative terms.
Squared edge lengths are packaged as a map $a:\mathrm{Fin},6\to\mathbb{R}$. The $5\times 5$ Cayley-Menger matrix of a tetrahedron is the standard bordered matrix of ones and squared distances (zeros on the spatial diagonal, ones in the bordering row and column). The normal form for the diagonal minor used by cofactor $(4,4)$ is the concrete $4\times 4$ matrix with first row/column $(0,1,1,1)$ and spatial block filled by $a_0,a_1,a_3$ in the usual edge indexing.
Deleting index $4$ from $\mathrm{Fin},5$ via $\mathrm{succAbove}$ is the standard way to form that principal minor as a Mathlib submatrix; this lemma asserts the submatrix coincides with the hand-written normal form.
proof idea
Apply matrix extensionality to reduce equality to agreement of all entries. Both sides are indexed by $\mathrm{Fin},4\times\mathrm{Fin},4$. Exhaustively case-split on the row and column indices with fin_cases, then each of the sixteen entries matches by definitional unfolding (rfl). No algebraic lemmas are needed beyond the definitions of the Cayley-Menger matrix and the normal-form minor.
why it matters
This is the bridge from the abstract submatrix minor to the named normal form whose determinant is expanded as a polynomial. The immediate parent is the theorem equating the $(4,4)$ cofactor of the tetrahedral Cayley-Menger matrix to the corresponding explicit cofactor polynomial: it rewrites the minor via this identification, then applies the determinant expansion of the normal form and simplifies the cofactor sign.
In the broader geometry stack, explicit cofactor polynomials feed dihedral-angle derivatives and volume-edge relations without leaving residual fderiv terms. The result is pure classical Euclidean geometry scaffolding inside the Recognition monolith; it does not itself invoke the forcing chain, $J$-cost, or $\varphi$-ladder, but it supplies the algebraic substrate those geometric layers consume when angles and volumes are differentiated against edge data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.