cmMinor20_submatrix_eq
plain-language theorem explainer
The 4×4 submatrix of the tetrahedral Cayley-Menger matrix obtained by deleting row 2 and column 0 equals the named explicit minor in the six squared edge lengths. Anyone expanding the (2,0)-cofactor as a polynomial cites this identification. Proof is entrywise exhaustion on Fin 4 × Fin 4 by reflexivity after ext.
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 $0$ equals the explicit matrix $\begin{pmatrix} 1 & 1 & 1 & 1 \\ 0 & a_0 & a_1 & a_2 \\ a_1 & a_3 & 0 & a_5 \\ a_2 & a_4 & 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 use named polynomial partials instead of opaque Fréchet derivatives.
SqEdges is the type of squared edge lengths of a tetrahedron, indexed by Fin 6. The Cayley-Menger matrix cmMatrix3 a is the standard $5\times 5$ bordered matrix built from those six squared lengths (zeros on the geometric diagonal, ones in the bordering row and column). The companion definition cmMinor20Matrix a hard-codes the $4\times 4$ array obtained by striking row 2 and column 0 of that matrix, written as an explicit !![...] literal in the edge coordinates $a_0,\ldots,a_5$.
This lemma is the bridge between the abstract Matrix.submatrix construction (via Fin.succAbove) and that named literal matrix.
proof idea
Term-level matrix extensionality: ext i j reduces equality of $4\times 4$ matrices to equality of all entries. Nested fin_cases on the two Fin 4 indices enumerates the sixteen positions; each case closes by rfl because the succAbove indexing of cmMatrix3 matches the hard-coded entries of cmMinor20Matrix definitionally.
why it matters
Feeds the parent theorem cmCofactor3_20_eq_poly, which rewrites the abstract cofactor cmCofactor3 a 2 0 as the named polynomial cmCofactor3Poly 2 0 a by unfolding the minor, applying this submatrix identification, then the determinant expansion det_cmMinor20Matrix, and simplifying the cofactor sign (even parity of 2). That equality is one cell of the module-wide agreement between abstract Cayley-Menger cofactors and their explicit polynomial forms, the cofactor analogue of the derivative expansions used for dihedral-angle calculus on the tetrahedron. No Recognition forcing-chain landmark is touched directly; the result is pure classical geometry scaffolding inside the RS geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.