cmMinor10_submatrix_eq
plain-language theorem explainer
The (1,0)-minor of the 5×5 Cayley-Menger matrix of a tetrahedron equals the named 4×4 matrix of ones and squared edge lengths. Anyone expanding tetrahedral cofactors into explicit polynomials cites this identification. The proof is entrywise: extend equality and discharge all Fin-4 index cases by 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 $1$ and column $0$ equals the explicit matrix whose first row and column are ones (off the corner zero pattern) and whose remaining entries are the corresponding squared edges from $a$.
background
The module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates, so dihedral-angle calculus can use named polynomial partials rather than 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 of those squared lengths (zeros on the spatial diagonal block, ones in the bordering row and column, zero at the $(0,0)$ corner).
cmMinor10Matrix a is the hand-written $4\times 4$ matrix
$$\begin{pmatrix}1&1&1&1\ a_0&0&a_3&a_4\ a_1&a_3&0&a_5\ a_2&a_4&a_5&0\end{pmatrix},$$
i.e. the concrete array one obtains by deleting row 1 and column 0 of cmMatrix3 a.
proof idea
Pointwise matrix equality. Apply ext on the two Fin 4 indices, then fin_cases on each index. Every one of the sixteen entries reduces by definition unfolding to the same real, so rfl closes each goal. No algebraic lemmas beyond the definitions of cmMatrix3, Matrix.submatrix via Fin.succAbove, and cmMinor10Matrix.
why it matters
This is the bridge from the abstract minor (submatrix of cmMatrix3) to the named polynomial matrix used in cofactor expansions. Downstream, cmCofactor3_10_eq_poly rewrites the $(1,0)$-cofactor as cmCofactor3Poly 1 0 a by substituting this equality and the determinant identity for cmMinor10Matrix, then simplifying the cofactor sign.
In the broader Recognition geometry stack, explicit cofactor polynomials feed dihedral-angle derivatives and volume-edge relations for tetrahedra. The module is the cofactor analogue of CayleyMengerDerivatives; closing each minor-identification lemma is what makes those polynomials trustworthy rather than opaque.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.