cmMinor22_submatrix_eq
plain-language theorem explainer
The (2,2) minor of the tetrahedral Cayley-Menger matrix, formed by deleting row and column index 2, equals a fixed 4×4 normal-form matrix in the six squared edge lengths. Anyone matching Cayley-Menger cofactors to named polynomials cites this identification. The proof is an entrywise 4×4 case split that collapses to 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 $CM_3(a)$ obtained by deleting row and column index $2$ equals the explicit normal-form matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & a_1 & a_2 \\ 1 & a_1 & 0 & a_5 \\ 1 & a_2 & 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 name polynomial partials instead of opaque Fréchet derivatives.
Squared edge lengths of a tetrahedron are packaged as a map $a:\mathrm{Fin},6\to\mathbb{R}$. The associated $5\times 5$ Cayley-Menger matrix $CM_3(a)$ has the usual bordered pattern: zeros on the first diagonal entry and on the geometric diagonal blocks, ones on the bordering row and column, and squared lengths off-diagonal. Cofactor $(2,2)$ is (up to sign) the determinant of the minor that deletes row and column index 2.
The normal-form matrix for that minor is the concrete $4\times 4$ array with first row/column $(0,1,1,1)$, geometric diagonal zero, and off-diagonal entries $a_1,a_2,a_5$ in the positions forced by the Cayley-Menger indexing. This theorem asserts that the abstract submatrix extraction recovers exactly that array.
proof idea
Extensionality on matrix entries reduces the claim to equality at each pair $(i,j)$ in $\mathrm{Fin},4\times\mathrm{Fin},4$. Nested fin_cases enumerates all sixteen pairs; each residual goal is definitional (rfl) once the submatrix reindexing succAbove 2 and the match-clauses of $CM_3$ and of the normal-form matrix are unfolded. No algebraic lemmas are required.
why it matters
Parent theorem cmCofactor3_22_eq_poly rewrites the abstract cofactor as the named polynomial by substituting this submatrix identity and then evaluating the $4\times 4$ determinant. That step is the cofactor analogue of the derivative expansions in CayleyMengerDerivatives: once every minor is pinned to a polynomial, partials of dihedral data become ordinary polynomial calculus in the six edge squares.
Within Recognition geometry this supplies the algebraic backbone for volume and angle identities on the tetrahedron, which feed the discrete geometric side of the forcing chain (eight-tick octave, $D=3$) rather than the $J$-cost side. The declaration itself is pure linear algebra; its value is that it closes the bridge from the opaque matrix minor to a referee-checkable polynomial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.