cmMinor42_submatrix_eq
plain-language theorem explainer
Deleting row 4 and column 2 from the 5×5 tetrahedral Cayley-Menger matrix recovers the named 4×4 minor matrix in the six squared edge lengths. Anyone equating cofactors to explicit polynomials cites this bridge. The proof is pure index exhaustion: extend equality and discharge all Fin-4 cases by rfl.
Claim. For every assignment $a$ of six squared edge lengths, the submatrix of the $5\times 5$ Cayley-Menger matrix of $a$ obtained by deleting row $4$ and column $2$ equals the explicitly tabulated $4\times 4$ minor whose entries are $0,1$ on the bordered first row/column and the appropriate $a_i$ in the interior.
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 simply Fin 6 → ℝ: the six squared edge lengths of a tetrahedron. The ambient object is cmMatrix3 a, the standard $5\times 5$ bordered Cayley-Menger matrix of those lengths (zeros on the point-point diagonal block, ones on the bordering row and column, and squared distances off-diagonal).
The target cmMinor42Matrix a is the concrete $4\times 4$ array
$$\begin{pmatrix}0&1&1&1\1&0&a_1&a_2\1&a_0&a_3&a_4\1&a_1&0&a_5\end{pmatrix}.$$
The theorem asserts that this array is exactly the submatrix of cmMatrix3 a after deleting index 4 from the rows and index 2 from the columns via Fin.succAbove.
proof idea
Pointwise matrix equality. Apply ext i j to reduce to entries indexed by i,j : Fin 4. Then fin_cases on both indices enumerates the sixteen concrete positions; each residual goal is definitional (rfl) once the match clauses of cmMatrix3 and the literal entries of cmMinor42Matrix are unfolded. No algebraic lemma is required.
why it matters
This is the structural bridge used by cmCofactor3_42_eq_poly, which rewrites the abstract cofactor cmCofactor3 a 4 2 into the named polynomial cmCofactor3Poly 4 2 a by substituting the submatrix identity and the already-proved determinant expansion of the minor. Parallel siblings exist for the other index pairs (34, 24, …), so the whole cofactor table becomes an explicit polynomial table. In the Recognition geometry stack those polynomials feed dihedral-angle derivatives and volume/angle identities built on the Cayley-Menger determinant; the present lemma is pure linear-algebra bookkeeping that makes those later equalities computable rather than opaque.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.