cmMinor21_submatrix_eq
plain-language theorem explainer
Deleting row 2 and column 1 from the 5×5 tetrahedral Cayley-Menger matrix yields exactly the named explicit 4×4 minor built from the six squared edge lengths. Anyone equating the (2,1)-cofactor to a closed polynomial cites this identification. 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 $M(a)$ obtained by deleting row index $2$ and column index $1$ equals the explicitly tabulated minor whose entries are $0$, $1$, and coordinates of $a$.
background
The ambient module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates, so downstream dihedral-angle calculus can quote named polynomial partials rather than opaque Fréchet derivatives.
Squared edge data are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The full $5\times 5$ Cayley-Menger matrix $M(a)$ places a bordering row and column of ones around the squared-distance block (diagonal zeros). The companion definition cmMinor21Matrix hard-codes the $4\times 4$ array obtained by striking row 2 and column 1:
$$\begin{pmatrix}0&1&1&1\1&a_0&a_1&a_2\1&a_3&0&a_5\1&a_4&a_5&0\end{pmatrix}.$$
Fin.succAbove k is the standard order-preserving embedding that skips index $k$, so the left-hand side is precisely that geometric minor.
proof idea
Apply matrix extensionality to reduce equality of $4\times 4$ matrices to pointwise equality of entries. For each pair of indices in $\mathrm{Fin},4$, run fin_cases on both coordinates; each of the sixteen residual goals is definitional (rfl) once the match clauses of cmMatrix3 and the literal array of cmMinor21Matrix are unfolded. No algebraic lemmas are required beyond the indexing conventions of succAbove.
why it matters
The immediate consumer is cmCofactor3_21_eq_poly, which rewrites the abstract cofactor cmCofactor3 a 2 1 as the named polynomial cmCofactor3Poly 2 1 a by substituting this submatrix identity and then evaluating the explicit $4\times 4$ determinant. That step is one tile in the module-wide programme of replacing every tetrahedral Cayley-Menger cofactor by a concrete polynomial in the six squared edges, the cofactor analogue of the derivative expansions used for dihedral-angle calculus. Without the submatrix match, the cofactor-to-polynomial bridge for index pair $(2,1)$ cannot fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.