cmMinor11_submatrix_eq
plain-language theorem explainer
Removing row and column index 1 from the 5×5 Cayley–Menger matrix of a tetrahedron yields a fixed 4×4 normal-form minor written in the six squared edge lengths. Anyone equating abstract CM cofactors to explicit polynomials cites this identity. The proof is entrywise: extensionality plus exhaustive Fin 4 case analysis, all reducing by 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 $C(a)$ obtained by deleting row $1$ and column $1$ equals the explicit matrix $$\begin{pmatrix}0&1&1&1\\1&0&a_3&a_4\\1&a_3&0&a_5\\1&a_4&a_5&0\end{pmatrix}.$$
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 use 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 first row and column are the usual bordering pattern $(0,1,\ldots,1)$ and whose interior $4\times 4$ block carries the squared distances (with zeros on the diagonal).
The target normal form cmMinor11Matrix a hard-codes the concrete $4\times 4$ array obtained by striking out the second row and second column (0-based index 1) of that matrix. The present lemma asserts that the abstract Matrix.submatrix construction coincides with this hand-written array.
proof idea
Purely definitional. Apply matrix extensionality to reduce equality of $4\times 4$ matrices to equality of all sixteen entries. For each pair of indices in Fin 4, run fin_cases on both coordinates; every goal is then rfl against the match-clauses of cmMatrix3 and the literal entries of cmMinor11Matrix. No algebraic lemmas are required.
why it matters
This is the bridge from the abstract minor used by the cofactor cmCofactor3 a 1 1 to the named polynomial cmCofactor3Poly 1 1. The immediate consumer cmCofactor3_11_eq_poly rewrites the cofactor via this identity, evaluates the determinant of the normal-form matrix, and simplifies the sign factor. Parallel lemmas exist for the other cofactor slots (cmMinor34_submatrix_eq, cmMinor24_submatrix_eq, …), forming the cofactor half of the explicit-polynomial infrastructure that feeds dihedral-angle derivatives in the Recognition geometry stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.