cmMinor41_submatrix_eq
plain-language theorem explainer
Deleting row 4 and column 1 from the 5×5 Cayley–Menger matrix of a tetrahedron yields a fixed 4×4 matrix written in the six squared edge lengths. Anyone equating abstract CM cofactors to named polynomials needs this identification. The proof is a 16-case matrix extensionality check by finite case split and reflexivity.
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 index $4$ and column index $1$ equals the explicitly tabulated minor matrix whose entries are $0$, $1$, and the coordinates $a_0,\ldots,a_5$ in the standard CM layout.
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so dihedral-angle calculus can cite named polynomial partials rather than opaque Fréchet derivatives.
SqEdges is the type of maps $\mathrm{Fin},6\to\mathbb{R}$ holding the six squared edge lengths. The upstream matrix $C(a)=\mathrm{cmMatrix3}(a)$ is the classical $5\times 5$ bordered Cayley–Menger matrix of a tetrahedron: zeros on the spatial diagonal block corners, ones in the bordering row and column, and squared distances $a_i$ in the interior.
The target minor matrix is the concrete $4\times 4$ array $$\begin{pmatrix}0&1&1&1\1&a_0&a_1&a_2\1&0&a_3&a_4\1&a_3&0&a_5\end{pmatrix},$$ obtained by striking row 4 and column 1 from $C(a)$. Parallel lemmas exist for the other index pairs used by the cofactor table.
proof idea
Pointwise matrix equality: ext i j reduces the claim to equality of all sixteen entries. Nested fin_cases on the two Fin 4 indices enumerates every pair; each residual goal is definitional (rfl) once the succAbove row/column maps and the match-based definition of cmMatrix3 are unfolded. No algebraic lemmas are required beyond finite case analysis.
why it matters
This is the bridge from the abstract submatrix-of-CM definition of a cofactor to the hand-written polynomial matrix used for determinant expansion. The sole direct consumer is cmCofactor3_41_eq_poly, which rewrites the $(4,1)$-cofactor as the named polynomial cmCofactor3Poly 4 1 by substituting this equality and the companion determinant identity det_cmMinor41Matrix, then adjusting the cofactor sign.
In the broader Recognition geometry stack, explicit cofactor polynomials feed dihedral-angle derivatives of the Cayley–Menger determinant. Those derivatives sit under volume and rigidity calculations that eventually constrain spatial dimension (forcing-chain T8) and discrete geometric structure. The lemma itself is pure linear algebra bookkeeping; its value is that it closes one cell of the generated cofactor table without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.