cmMinor43_submatrix_eq
plain-language theorem explainer
Deleting row 4 and column 3 from the 5×5 Cayley–Menger matrix of a tetrahedron yields a fixed 4×4 matrix whose entries are 0, 1, or the six squared edge lengths. Anyone equating abstract CM cofactors to named polynomials cites this identification. The proof is entrywise: extensionality plus exhaustive Fin 4 case splits, each reducing by definitional equality.
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 $4$ and column $3$ equals the explicit matrix $$\begin{pmatrix}0&1&1&1\\1&0&a_0&a_2\\1&a_0&0&a_4\\1&a_1&a_3&a_5\end{pmatrix}.$$
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives.
SqEdges is the type of squared edge lengths of a tetrahedron, indexed by Fin 6. The ambient object is the $5\times 5$ Cayley–Menger matrix $C(a)=\mathrm{cmMatrix3}(a)$, whose border is the usual $0/1$ pattern and whose interior holds the squared distances. The target minor matrix is the hardcoded $4\times 4$ array cmMinor43Matrix a with first row/column $(0,1,1,1)$ and interior filled by $a_0,a_1,a_2,a_3,a_4,a_5$ in the pattern that arises from deleting index $4$ from rows and index $3$ from columns.
Fin.succAbove k is the order-preserving embedding $\mathrm{Fin},4\hookrightarrow\mathrm{Fin},5$ that skips $k$. Composing both embeddings with $C(a)$ is exactly the classical submatrix delete-row-$4$/delete-column-$3$.
proof idea
Pure definitional check. Apply matrix extensionality to reduce equality of $4\times 4$ matrices to equality of all sixteen entries. For each pair of indices $(i,j)\in\mathrm{Fin},4\times\mathrm{Fin},4$, run fin_cases on both coordinates; each of the sixteen residual goals is rfl against the match-table definition of cmMatrix3 and the literal array definition of cmMinor43Matrix. No algebraic lemmas are required.
why it matters
Parent theorem cmCofactor3_43_eq_poly rewrites the abstract cofactor cmCofactor3 a 4 3 by unfolding the minor, replacing the submatrix with this explicit matrix, then invoking the closed-form determinant det_cmMinor43Matrix and the cofactor sign. Without the submatrix identification, the cofactor-to-polynomial bridge for the $(4,3)$ slot cannot fire.
In the broader Recognition geometry stack this is scaffolding for dihedral-angle derivatives of the Cayley–Menger volume form: once every cofactor is a named polynomial in the six squared edges, partials become ordinary multivariable calculus rather than abstract fderiv terms. It is one of a family of sibling equalities (cmMinor34_submatrix_eq, cmMinor24_submatrix_eq, …) that together discharge the full cofactor table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.