cmMinor40_submatrix_eq
plain-language theorem explainer
The 4×4 submatrix of the tetrahedral Cayley-Menger matrix obtained by deleting row 4 and column 0 equals the named explicit minor matrix in the six squared edge lengths. Anyone equating the (4,0)-cofactor to a closed-form polynomial cites this identification. Proof is entrywise Fin-case exhaustion with reflexivity.
Claim. For every assignment $a$ of six squared edge lengths, the $4\times 4$ submatrix of the Cayley-Menger matrix $CM_3(a)$ obtained by deleting row index $4$ and column index $0$ equals the explicitly written minor whose first row is $(1,1,1,1)$, whose remaining diagonal vanishes, and whose off-diagonal entries are the six squared edges $a_0,\ldots,a_5$ in the standard Cayley-Menger layout.
background
The ambient module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates, so downstream dihedral-angle calculus can quote named polynomial partials rather than opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The $5\times 5$ Cayley-Menger matrix $CM_3(a)$ has the usual border of ones, zero diagonal, and off-diagonal squared lengths. The target minor matrix is the concrete $4\times 4$ array with first row $(1,1,1,1)$, zero on the remaining diagonal, and the six edges $a_0,\ldots,a_5$ filling the Cayley-Menger pattern after row 4 and column 0 are removed.
Deleting index $k$ via Fin.succAbove k is the standard Mathlib encoding of a principal-complement submatrix; the theorem asserts that this abstract deletion coincides with the hand-written array.
proof idea
Term-mode proof by matrix extensionality: reduce equality of $4\times 4$ matrices to equality of all entries. Exhaust the two Fin 4 indices with fin_cases; each of the sixteen residual goals is definitional (rfl) once both the submatrix projection of $CM_3(a)$ and the explicit minor array are unfolded.
why it matters
Feeds the parent identity that the $(4,0)$-cofactor of $CM_3$ equals the named cofactor polynomial: that proof unfolds the cofactor, rewrites by this submatrix equality, then applies the explicit determinant of the minor and simplifies the sign. The same pattern appears for the sibling minors (indices 3-4, 2-4, 2-3, …), so the module can export a full table of cofactor polynomials. Those polynomials are the cofactor analogue of the Cayley-Menger derivative suite and are the algebraic substrate for dihedral-angle calculus on the tetrahedron inside the Recognition geometry stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.