cmMinor14Matrix
plain-language theorem explainer
Normal-form 4×4 matrix for the Cayley–Menger minor tied to cofactor (1,4), written in the six squared edge lengths of a tetrahedron. Anyone expanding CM cofactors into explicit polynomials, or matching them to bordered-matrix minors, cites this. The body is a concrete matrix literal; no proof work.
Claim. Given squared edge lengths $a\colon\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ real 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}.$$ This is the normal form of the minor used by the Cayley–Menger cofactor at index pair $(1,4)$.
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 live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$): the six edge lengths squared of a tetrahedron. The ambient object is the usual $5\times 5$ bordered Cayley–Menger matrix built from those edges; cofactors of that matrix control volumes and dihedral geometry.
Index pair $(1,4)$ selects one such cofactor. The present definition freezes the corresponding $4\times 4$ minor in a fixed coordinate order so later identities can compare submatrices and determinants without chasing succAbove bookkeeping.
proof idea
Pure definition: a matrix literal of type Matrix (Fin 4) (Fin 4) ℝ. Entries are the constant border row/column $(0,1,1,1)$ and the squared-edge slots $a_0,a_1,a_2,a_3,a_4,a_5$ placed in the pattern that matches deletion of row index 1 and column index 4 from the full CM matrix. No lemmas are applied.
why it matters
Gives a named normal form so the cofactor polynomial pipeline can stay algebraic. Downstream, cmMinor14_submatrix_eq proves this literal equals the actual submatrix of the $5\times 5$ CM matrix after removing row 1 and column 4 (via ext and fin_cases). Then det_cmMinor14Matrix identifies its determinant with $-$ the explicit cofactor polynomial at $(1,4)$, by unfolding and a short ring normalization on the Laplace expansion along the zero border row.
Together those facts discharge the cofactor-analogue of the derivative module: dihedral formulas can quote a polynomial in the six $a_i$ rather than an abstract minor. Sibling minors (23, 24, 34, …) play the same role for the other index pairs. No Recognition forcing-chain landmark (T5–T8, RCL) is touched; this is pure classical CM algebra supporting later geometric calculus in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.