cmMinor04_submatrix_eq
plain-language theorem explainer
Deleting row 0 and column 4 from the 5×5 Cayley–Menger matrix of a tetrahedron yields a concrete 4×4 matrix of ones and squared edge lengths. Anyone equating abstract CM cofactors to named polynomials cites this identity. The proof is pure index exhaustion: extensionality plus fin_cases, then definitional equality.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the $4\times 4$ submatrix of the Cayley–Menger matrix obtained by deleting row $0$ and column $4$ equals the explicit matrix $$\begin{pmatrix}1&0&a_0&a_1\\1&a_0&0&a_3\\1&a_1&a_3&0\\1&a_2&a_4&a_5\end{pmatrix}.$$
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so dihedral-angle calculus can quote named polynomial partials rather than opaque Fréchet derivatives.
SqEdges is simply Fin 6 → ℝ: the six squared edge lengths of a tetrahedron. The ambient object is the $5\times 5$ Cayley–Menger matrix cmMatrix3 a, whose border is the usual pattern of zeros and ones and whose interior holds the squared distances. The target cmMinor04Matrix a is the hand-written $4\times 4$ array obtained by striking row 0 and column 4 of that pattern.
The comparison uses Mathlib’s Matrix.submatrix with the two Fin.succAbove embeddings that skip index 0 on rows and index 4 on columns.
proof idea
Pointwise equality of matrices. Apply ext i j, then fin_cases on both Fin 4 indices. Each of the sixteen cells reduces by rfl to the corresponding entry of the explicit !![...] definition of cmMinor04Matrix, because cmMatrix3 is itself defined by a match on i.val, j.val and the succAbove embeddings simply select those indices.
why it matters
This is the bridge from the abstract minor Matrix.submatrix (cmMatrix3 a) … to the named matrix whose determinant is expanded as a polynomial. Downstream, cmCofactor3_04_eq_poly rewrites the cofactor cmCofactor3 a 0 4 through this identity and det_cmMinor04Matrix, then adjusts the sign, obtaining cmCofactor3Poly 0 4 a.
In the broader Recognition geometry stack these explicit cofactor polynomials feed dihedral-angle derivatives (the cofactor analogue of CayleyMengerDerivatives). They sit in the classical Cayley–Menger volume/angle calculus that underpins rigid tetrahedral geometry; no T0–T8 forcing step is invoked here, only the algebraic scaffolding those later geometric claims rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.