cmMinor01_submatrix_eq
plain-language theorem explainer
The 4×4 submatrix of the tetrahedral Cayley-Menger matrix obtained by deleting row 0 and column 1 equals the named explicit minor matrix in the six squared edge lengths. Cofactor-to-polynomial expansions cite this identification before taking determinants. The proof is a finite case check: matrix extensionality plus sixteen reflexive entry equalities.
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 $0$ and column $1$ equals $\begin{pmatrix} 1 & a_0 & a_1 & a_2 \\ 1 & 0 & a_3 & a_4 \\ 1 & a_3 & 0 & a_5 \\ 1 & a_4 & a_5 & 0 \end{pmatrix}$.
background
This 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 instead of opaque Fréchet derivatives.
Squared edge lengths are packaged as $a:\mathrm{Fin},6\to\mathbb{R}$. The Cayley-Menger matrix $C(a)$ is the standard $5\times 5$ bordered matrix of squared distances for a tetrahedron (zeros on the distance block diagonal, a bordering row and column of ones, and a zero corner). The companion definition hard-codes the $4\times 4$ array obtained by striking row 0 and column 1 of that matrix.
The lemma equates the abstract submatrix construction (delete indices via successor-above maps on $\mathrm{Fin},5$) with that concrete matrix literal, so later determinant expansions can unfold a named array rather than a generic submatrix.
proof idea
Term proof by matrix extensionality. After extending equality at indices $i,j:\mathrm{Fin},4$, nested finite case splits enumerate all sixteen pairs. Each entry reduces by definitional unfolding of the Cayley-Menger matrix, the submatrix map, the index-deletion maps, and the explicit minor matrix to a reflexive equality. No external lemmas are required beyond the definitions.
why it matters
Direct input to the theorem that equates the $(0,1)$-cofactor of the Cayley-Menger matrix with the named polynomial cofactor in the six squared edges. That step rewrites the abstract cofactor through this submatrix identity, then through the explicit determinant of the minor matrix, and finally adjusts the cofactor sign. The same pattern is repeated for sibling index pairs (23, 24, 34, ...), giving a complete dictionary from cofactors to polynomials.
In the Recognition geometry stack this supplies closed-form edge polynomials for tetrahedral volumes and dihedral angles, which sit under the $D=3$ spatial forcing (T8) and feed any later calculus that differentiates those angles with respect to edge data. The present lemma itself is pure classical Cayley-Menger algebra: it closes one matrix-identification gap in that dictionary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.