cmMinor30_submatrix_eq
plain-language theorem explainer
The (3,0)-minor of the tetrahedral Cayley-Menger matrix, formed by deleting row 3 and column 0, coincides entrywise with an explicitly tabulated 4×4 matrix in the six squared edge lengths. Anyone expanding CM cofactors into named polynomials cites this identification. The proof is exhaustive Fin-4 case analysis with reflexivity on each entry.
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 index $3$ and column index $0$ equals the explicit matrix $\begin{pmatrix} 1 & 1 & 1 & 1 \\ 0 & a_0 & a_1 & a_2 \\ a_0 & 0 & a_3 & a_4 \\ a_2 & 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 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 form: zeros on the spatial diagonal block corners, ones in the bordering row and column, and squared distances $a_k$ in the off-diagonal spatial entries.
The target object is the concrete $4\times 4$ matrix obtained by writing out that minor by hand: first row all ones, then the three spatial rows filled from $a_0,\ldots,a_5$ in the standard CM indexing. This lemma asserts that the abstract submatrix construction (delete row 3, column 0) reproduces that table.
proof idea
Pointwise extensionality on the $4\times 4$ index set, then fin_cases on both row and column indices. Each of the sixteen residual goals is definitional equality (rfl) between the corresponding entry of the submatrix of $CM_3(a)$ and the hard-coded table. No algebraic lemmas are required; the match is purely by construction of the two matrices.
why it matters
Parent theorem cmCofactor3_30_eq_poly rewrites the abstract $(3,0)$-cofactor as the named polynomial by substituting this identification and then evaluating the explicit $4\times 4$ determinant. That step is one cell in the generated grid that turns every tetrahedral CM cofactor into a polynomial in the six squared edges.
Those named cofactor polynomials are the cofactor analogue of the Cayley-Menger derivative module: they let dihedral-angle identities and partials be stated algebraically rather than as opaque derivatives of determinants. In the broader Recognition geometry stack this keeps volume and angle calculus fully symbolic on the edge-length ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.