cmMinor24_submatrix_eq
plain-language theorem explainer
Deleting row 2 and column 4 from the 5×5 Cayley-Menger matrix of a tetrahedron recovers the explicit 4×4 normal-form minor used for cofactor (2,4). Anyone equating abstract CM cofactors to named edge polynomials cites this identity. The proof is entrywise extensionality plus exhaustive Fin-case discharge.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the submatrix of the $5\times 5$ Cayley-Menger matrix obtained by deleting row index $2$ and column index $4$ equals the explicit normal-form matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & a_0 & a_1 \\ 1 & a_1 & a_3 & 0 \\ 1 & a_2 & a_4 & a_5 \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 data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The ambient object is the $5\times 5$ Cayley-Menger matrix of a tetrahedron, built entrywise from those six lengths (border of ones, zeros on the squared-distance diagonal block, off-diagonal squared lengths). The target normal form for the $(2,4)$ minor is the concrete $4\times 4$ matrix with first row/column the usual CM border and remaining entries $a_0,a_1,a_2,a_3,a_4,a_5$ in the pattern that arises after deleting row 2 and column 4.
This lemma simply identifies the abstract Matrix.submatrix extraction (via Fin.succAbove on indices 2 and 4) with that named normal form.
proof idea
Term-style tactic proof by matrix extensionality: reduce equality of $4\times 4$ matrices to equality of all entries. Then fin_cases on both row and column indices of $\mathrm{Fin},4$, giving sixteen residual goals, each discharged by rfl against the match-definition of the Cayley-Menger matrix and the literal entries of the normal-form minor. No algebraic lemmas beyond definitional unfolding.
why it matters
Parent consumer is cmCofactor3_24_eq_poly, which rewrites the abstract cofactor $(2,4)$ as the named polynomial by substituting this submatrix identity and then the explicit determinant of the normal form (sign handled by parity of $2+4$). That equality is one cell of the module-wide agreement between cofactor extraction and the generated cofactor polynomials.
In the broader Recognition geometry stack these named cofactor polynomials feed dihedral-angle derivatives via Cayley-Menger identities, replacing opaque fderiv terms. The lemma is pure linear-algebra bookkeeping; it does not itself invoke the forcing chain, RCL, or $\varphi$-ladder, but it is infrastructure those geometric layers sit on when they differentiate volume or angle expressions in edge coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.