cmMinor32_submatrix_eq
plain-language theorem explainer
The (3,2)-minor of the tetrahedral Cayley-Menger matrix, formed by deleting row 3 and column 2, coincides entrywise with a named 4×4 matrix in the six squared edge lengths. Anyone expanding CM cofactors into explicit polynomials cites this identification. The proof is exhaustive case analysis on the 4×4 index set, then reflexivity on each entry.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the $4\times 4$ submatrix of the Cayley-Menger matrix $CM_3(a)$ obtained by deleting row index $3$ and column index $2$ equals the explicit matrix $\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & a_1 & a_2 \\ 1 & a_0 & a_3 & a_4 \\ 1 & a_2 & a_5 & 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 Fréchet derivatives.
Squared edge lengths of a tetrahedron are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The ambient object is the $5\times 5$ Cayley-Menger matrix $CM_3(a)$: border of ones, zero diagonal on the geometric block, and off-diagonal geometric entries equal to the squared edge lengths. The target minor matrix is the hand-written $4\times 4$ array with first row/column the usual CM border and interior filled by $a_0,\ldots,a_5$ in the pattern that remains after deleting row 3 and column 2.
This lemma simply certifies that Mathlib's generic Matrix.submatrix applied to $CM_3(a)$ with the two succAbove deletions recovers that named array.
proof idea
Pointwise extensionality on the $4\times 4$ index set, then fin_cases on both indices. Each of the sixteen concrete entries reduces by definition unfolding of $CM_3$ and of the named minor matrix to an identical real literal or edge coordinate, discharged by rfl. No algebraic lemmas are required.
why it matters
Parent theorem cmCofactor3_32_eq_poly rewrites the abstract $(3,2)$-cofactor of $CM_3$ as the determinant of this named minor (with the usual cofactor sign). That equality is one cell of the module-wide dictionary from opaque CM cofactors to explicit polynomials in the six squared edges.
Those polynomials feed dihedral-angle calculus on the tetrahedron: once cofactors are polynomial, partial derivatives with respect to edge lengths become ordinary polynomial differentiation rather than abstract fderiv terms. The same pattern appears for the sibling minors $(3,4)$, $(2,4)$, $(2,3)$, etc. Within Recognition geometry this is pure classical support: Cayley-Menger volume and angle formulae expressed in RS edge data, not a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.