cmMinor02_submatrix_eq
plain-language theorem explainer
Deleting row 0 and column 2 from the 5×5 Cayley-Menger matrix of a tetrahedron yields a named explicit 4×4 matrix in the six squared edge lengths. Anyone equating Cayley-Menger cofactors to closed-form polynomials cites this identity. The proof is entrywise exhaustion on Fin 4 × Fin 4 by reflexivity after matrix extensionality.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the $4\times 4$ submatrix of the Cayley-Menger matrix $C(a)$ obtained by deleting row $0$ and column $2$ equals the explicit matrix $\begin{pmatrix} 1 & 0 & a_1 & a_2 \\ 1 & a_0 & a_3 & a_4 \\ 1 & a_1 & 0 & a_5 \\ 1 & a_2 & a_5 & 0 \end{pmatrix}$.
background
The ambient module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates. Downstream dihedral-angle calculus can then refer to named polynomial partials instead of opaque Fréchet derivatives.
Squared edge lengths are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The $5\times 5$ Cayley-Menger matrix $C(a)$ is the standard bordered Gram matrix of a tetrahedron: zeros on the spatial diagonal block corners, ones in the bordering row and column, and squared distances off-diagonal. The target object is the hand-written $4\times 4$ minor matrix obtained by striking row 0 and column 2, with entries filled directly from the six edge coordinates $a_0,\ldots,a_5$.
This lemma simply identifies Mathlib's generic submatrix construction (via Fin.succAbove) with that named matrix, so later determinant and cofactor identities can unfold against a concrete array rather than an abstract deletion.
proof idea
Purely computational. Apply matrix extensionality to reduce equality of $4\times 4$ matrices to pointwise equality of entries. For each of the sixteen index pairs $(i,j)\in\mathrm{Fin},4\times\mathrm{Fin},4$, case-split with fin_cases and discharge by rfl: both sides evaluate to the same literal real expression built from $a$. No algebraic lemmas are required beyond the definitions of the Cayley-Menger matrix and the named minor.
why it matters
This is the bridge from abstract matrix deletion to the explicit cofactor polynomial pipeline. The sole downstream consumer is cmCofactor3_02_eq_poly, which rewrites the $(0,2)$-cofactor of the Cayley-Menger matrix as the named polynomial cmCofactor3Poly 0 2 by substituting this submatrix identity, evaluating the $4\times 4$ determinant, and inserting the cofactor sign (even, since $0+2$ is even).
In the broader Recognition geometry stack, explicit cofactor polynomials feed dihedral-angle derivatives and volume-edge relations for tetrahedra. The module is the cofactor analogue of the Cayley-Menger derivative expansions: once every minor is pinned to a polynomial, partials with respect to edge lengths become ordinary polynomial calculus rather than symbolic fderiv terms. The result is local bookkeeping, not a forcing-chain step, but it is required scaffolding for any later claim that equates geometric angles or volumes to closed forms on the edge ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.