cmMinor23_submatrix_eq
plain-language theorem explainer
The 4×4 submatrix of the tetrahedral Cayley–Menger matrix obtained by deleting row 2 and column 3 equals the named normal-form minor for cofactor (2,3). Anyone expanding CM cofactors into explicit polynomials in the six squared edges cites this identification. Proof is entrywise Fin-case analysis with reflexivity.
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 $2$ and column index $3$ equals the explicit normal-form matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & a_0 & a_2 \\ 1 & a_1 & a_3 & a_5 \\ 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 Fréchet derivatives.
Squared edge lengths live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The $5\times 5$ Cayley–Menger matrix $CM_3(a)$ is the standard bordered matrix of those squared lengths (zeros on the spatial diagonal, ones in the bordering row/column). The named minor matrix for cofactor $(2,3)$ is the hard-coded $4\times 4$ array with entries $0,1$ and the six edge squares $a_0,\ldots,a_5$ in the positions that survive after deleting row 2 and column 3.
This lemma simply asserts that Mathlib’s generic submatrix of $CM_3(a)$ along succAbove 2 and succAbove 3 recovers that normal form.
proof idea
Pointwise matrix extensionality on the $4\times 4$ index type. Both indices are exhausted by fin_cases; each of the sixteen concrete entries reduces by rfl to the corresponding clause of the Cayley–Menger matrix definition versus the hard-coded normal-form array. No algebraic lemmas are required beyond definitional equality of the match arms.
why it matters
Feeds the parent theorem that equates the abstract cofactor $C_{2,3}(CM_3(a))$ with the named polynomial cmCofactor3Poly 2 3 a: that proof rewrites the minor via this identification, then applies the explicit determinant of the normal-form matrix and the cofactor sign. The same pattern is repeated for the sibling minors $(3,4)$ and $(2,4)$. Together they close the cofactor half of the explicit-polynomial bridge that lets dihedral-angle derivatives be written as ordinary partials of named polynomials rather than as fderiv terms. No Recognition-forcing landmark (T5–T8, RCL, $\varphi$) is touched; the result is pure classical geometry scaffolding inside the RS geometry stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.