cmMinor14_submatrix_eq
plain-language theorem explainer
Deleting row index 1 and column index 4 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 expanding tetrahedral cofactors into explicit polynomials cites this equality. The proof is entrywise: extend equality of matrices and discharge all sixteen Fin-4 cases by definitional reduction.
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 $4$ equals the explicit matrix $$\begin{pmatrix}0&1&1&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 that dihedral-angle calculus can use named polynomial partials rather than opaque Fréchet derivatives.
Squared edge data are an assignment $a:\mathrm{Fin},6\to\mathbb{R}$. The associated $5\times 5$ Cayley–Menger matrix $C(a)$ has the usual bordered pattern: zeros on the leading diagonal block of geometric entries, a border of ones, and off-diagonal geometric entries equal to squared lengths. Cofactor $(1,4)$ is (up to sign) the determinant of the minor that deletes row 1 and column 4. That minor is packaged here as a concrete $4\times 4$ matrix whose entries are $0$, $1$, or selected components of $a$.
The present statement simply identifies the abstract submatrix extraction with that normal-form matrix, so later determinant expansions can be written by hand against a fixed array rather than against a submatrix term.
proof idea
Prove matrix equality by extensionality on indices $i,j:\mathrm{Fin},4$. For each pair, run exhaustive case analysis on the four possible values of $i$ and of $j$. Every one of the sixteen entries reduces definitionally to the corresponding entry of the normal-form minor, so rfl closes each goal. No algebraic lemmas are required beyond the definitions of the Cayley–Menger matrix, the normal-form minor, and Matrix.submatrix with Fin.succAbove.
why it matters
This is a bookkeeping bridge inside the cofactor-polynomial layer. Downstream, cmCofactor3_14_eq_poly unfolds the abstract cofactor, rewrites the minor via this equality, evaluates the determinant of the normal form, and inserts the cofactor sign, obtaining an explicit polynomial in the six squared edges. That polynomial is the cofactor analogue of the derivative expansions used for dihedral-angle calculus on tetrahedra.
In the broader Recognition geometry stack, Cayley–Menger determinants encode volumes and angles from edge data alone; making cofactors polynomial lets later rigidity and curvature arguments stay inside algebraic identities rather than calculus black boxes. The result does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is pure classical geometry scaffolding that those layers can call when they need tetrahedral angles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.