cmMinor03_submatrix_eq
plain-language theorem explainer
The (0,3)-minor of the tetrahedral Cayley-Menger matrix, formed by deleting row 0 and column 3, equals an explicitly written 4×4 matrix in the six squared edge lengths. Anyone equating abstract cofactors to named polynomials cites this identification. The proof is entrywise case analysis on Fin 4 indices, each 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 $CM_3(a)$ obtained by deleting row $0$ and column $3$ equals the explicit matrix $\begin{pmatrix} 1 & 0 & a_0 & a_2 \\ 1 & a_0 & 0 & a_4 \\ 1 & a_1 & a_3 & a_5 \\ 1 & a_2 & a_4 & 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 refer to named polynomial partials instead of opaque Fréchet derivatives.
The Cayley-Menger matrix of a tetrahedron is the standard $5\times 5$ bordered matrix of squared distances (four vertices plus a bordering row and column of ones), written as a function of SqEdges (squared edge lengths indexed by Fin 6). The companion definition hard-codes the $4\times 4$ array that should arise on deleting row index 0 and column index 3.
This lemma is the bridge between the abstract Matrix.submatrix construction (via Fin.succAbove) and that concrete array.
proof idea
Pointwise matrix extensionality on the two Fin 4 indices, then exhaustive fin_cases on each index. All sixteen entries match by rfl against the corresponding clause of the Cayley-Menger matrix and the literal entries of the explicit minor. No algebraic rewriting is required; once indices are concrete the equality is definitional.
why it matters
Downstream, the theorem equating the abstract cofactor at $(0,3)$ to the named polynomial rewrites through this identification and the determinant of the explicit minor. That step is part of the module program of replacing opaque cofactors by explicit polynomials for tetrahedral dihedral calculus (the cofactor analogue of the Cayley-Menger derivative expansions).
In the Recognition geometry stack this supports volume and angle identities built from Cayley-Menger determinants. It does not itself invoke the forcing chain (T0–T8), the J-cost, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.