cmMinor33_submatrix_eq
plain-language theorem explainer
The principal minor of the 5×5 Cayley-Menger matrix obtained by deleting row and column 3 equals the named 4×4 normal-form matrix in the six squared edge lengths. Anyone rewriting abstract tetrahedral cofactors as explicit polynomials cites this matrix identification. The proof is entrywise Fin-case analysis with definitional equality.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the $4\times 4$ submatrix of the Cayley-Menger matrix obtained by deleting row index $3$ and column index $3$ equals the explicit matrix $\begin{pmatrix}0&1&1&1\\1&0&a_0&a_2\\1&a_0&0&a_4\\1&a_2&a_4&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 derivatives.
Squared edge data are an assignment $a:\mathrm{Fin},6\to\mathbb{R}$. The Cayley-Menger matrix of a tetrahedron is the standard $5\times 5$ bordered matrix of ones and squared lengths (border row/column of ones, zero diagonal on the geometric block). The named minor matrix is the fixed $4\times 4$ array with top-left $0$, first row/column of ones, and geometric block filled by $a_0,a_2,a_4$ in the pattern used by cofactor $(3,3)$.
Deleting index $3$ via succAbove is the abstract submatrix construction; this lemma pins that construction to the concrete array.
proof idea
Prove matrix equality by extensionality on entries. Both index types are Fin 4, so run fin_cases on the row and column indices. Each of the sixteen concrete positions reduces by rfl to the matching clause in the definitions of the Cayley-Menger matrix and of the named minor array. No algebraic lemmas are required beyond definitional unfolding.
why it matters
The immediate consumer is the theorem that the abstract $(3,3)$ cofactor equals the named cofactor polynomial: it unfolds the cofactor, rewrites the submatrix via this lemma, then substitutes the explicit determinant of the named minor and simplifies the sign. That step is one brick in the module's programme of replacing opaque cofactor extractions by named polynomials in the six squared edges, which in turn feeds dihedral-angle calculus that needs differentiable closed forms rather than fderiv terms. The result is pure linear-algebra bookkeeping inside the Cayley-Menger geometry layer; it does not itself touch Recognition forcing landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.