cmMinor31_submatrix_eq
plain-language theorem explainer
The 4×4 submatrix of the tetrahedral Cayley-Menger matrix obtained by deleting row 3 and column 1 equals the named explicit minor matrix in the six squared edge lengths. Anyone equating the (3,1)-cofactor to a closed polynomial cites this identification. Proof is entrywise: extensionality on Fin 4 × Fin 4, then case split with reflexivity.
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 $3$ and column index $1$ equals the explicit minor matrix whose entries are $0$, $1$, and the coordinates $a_0,\ldots,a_5$ in the standard Cayley-Menger positions.
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 name polynomial partials instead of opaque derivative terms.
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 $CM_3(a)$, whose border is the usual $0/1$ pattern and whose interior holds the six squared lengths. The target cmMinor31Matrix is the hand-written $4\times 4$ matrix obtained by striking row 3 and column 1 of that pattern:
$$\begin{pmatrix}0&1&1&1\1&a_0&a_1&a_2\1&0&a_3&a_4\1&a_4&a_5&0\end{pmatrix}.$$
Deleting a row and column of a Fin-indexed matrix is Matrix.submatrix along Fin.succAbove, so the claim is that the abstract submatrix constructor reproduces this concrete array.
proof idea
Term-level matrix equality is reduced by ext i j to pointwise equality of real entries. Both index types are Fin 4, so fin_cases i followed by fin_cases j enumerates all sixteen positions. Each residual goal is definitional: the corresponding match arm of cmMatrix3 after succAbove agrees with the literal entry of cmMinor31Matrix, discharged by rfl. No algebraic lemmas are required.
why it matters
This is one of the sibling submatrix-identification lemmas (cmMinor34_submatrix_eq, cmMinor24_submatrix_eq, …) that unlock explicit cofactor polynomials. Its sole recorded consumer is cmCofactor3_31_eq_poly, which unfolds the abstract cofactor, rewrites the minor via this equality, evaluates the determinant of the explicit matrix, and simplifies the cofactor sign. That chain is the cofactor analogue of the Cayley-Menger derivative expansions: once every cofactor is a named polynomial in the six squared edges, dihedral-angle formulas become ordinary multivariable calculus on those polynomials rather than formal derivatives of determinants. In the broader Recognition geometry stack this keeps tetrahedral volume and angle identities fully algebraic in edge data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.