cmMinor04Matrix
plain-language theorem explainer
Explicit 4×4 matrix in the six squared edge lengths equal to the Cayley–Menger minor that deletes row 0 and column 4. Cofactor and dihedral-angle developments cite it so determinants and partials land on a named carrier rather than an opaque submatrix. The body is a matrix literal; no proof obligations.
Claim. Given squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ real matrix whose rows are $(1,0,a_0,a_1)$, $(1,a_0,0,a_3)$, $(1,a_1,a_3,0)$, and $(1,a_2,a_4,a_5)$. It is the minor of the bordered Cayley–Menger matrix after deleting index-0 row and index-4 column.
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives.
Squared edge data are packaged as SqEdges: maps $\mathrm{Fin},6\to\mathbb{R}$, one coordinate per edge of a tetrahedron. The ambient object is the standard $5\times 5$ bordered Cayley–Menger matrix built from those six squares; cofactors are determinants of its $4\times 4$ minors.
This declaration freezes the concrete minor for the $(0,4)$ index pair as a matrix literal in those six coordinates, matching the submatrix obtained by succAbove deletion of row 0 and column 4.
proof idea
Definition only: a single !![...; ...] matrix literal whose twelve nontrivial entries are the constants $0,1$ and the six squared-edge coordinates $a,0,\ldots,a,5$ in the Cayley–Menger layout. No tactics, no lemmas.
why it matters
Supplies the named carrier used by two immediate parents in the same module. cmMinor04_submatrix_eq proves the literal equals the actual submatrix of the bordered Cayley–Menger matrix after deleting row 0 and column 4. det_cmMinor04Matrix then evaluates that determinant by row expansion and ring normalization, identifying it with the explicit cofactor polynomial cmCofactor3Poly 0 4.
Together those steps discharge the cofactor-polynomial programme stated in the module header: every tetrahedral CM cofactor becomes a concrete polynomial in the six edge squares, ready for named partial derivatives in dihedral-angle calculus. The construction is local geometry scaffolding inside Recognition Science; it does not itself invoke the forcing chain, $\varphi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.