cmMinor42Matrix
plain-language theorem explainer
Explicit 4×4 matrix equal to the Cayley–Menger minor that deletes row 4 and column 2, written in the six squared edge lengths of a tetrahedron. Cofactor and dihedral-angle calculus cite it so determinants become named polynomials rather than opaque submatrix extractions. The body is a matrix literal; no proof work.
Claim. Given squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the real $4\times 4$ matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & a(1) & a(2) \\ 1 & a(0) & a(3) & a(4) \\ 1 & a(1) & 0 & a(5) \end{pmatrix}.$$ It is the minor of the bordered Cayley–Menger matrix obtained by deleting row index 4 and column index 2.
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 name polynomial partials instead of opaque Fréchet derivatives.
Squared edge data are packaged as SqEdges: maps Fin 6 → ℝ, one coordinate per edge of a tetrahedron. The full bordered Cayley–Menger matrix (imported from the Cayley–Menger matrix module) is 5×5; its 4×4 minors are the carriers of the cofactors that enter volume and dihedral formulae.
Sibling definitions supply the other index pairs (e.g. minors 3-4, 2-4, 2-3). This entry is the concrete matrix for the (4,2) pair.
proof idea
Pure definition: a 4×4 matrix literal whose entries are the constants 0, 1 and the six squared-edge coordinates in the pattern of the (4,2)-minor of the bordered Cayley–Menger matrix. No lemmas or tactics.
why it matters
Named carrier for the (4,2) cofactor polynomial path. Downstream, cmMinor42_submatrix_eq proves the literal equals the actual submatrix of the 5×5 Cayley–Menger matrix after deleting row 4 and column 2 (by exhaustive fin_cases and rfl). Then det_cmMinor42Matrix expands the determinant and identifies it with the named cofactor polynomial cmCofactor3Poly 4 2, via det_succ_row_zero and ring normalization.
Together these close the cofactor-analogue of the Cayley–Menger derivative module: dihedral-angle identities can differentiate named polynomials in the six edge squares rather than symbolic minors. In the broader Recognition geometry stack this supplies the algebraic backbone for volume and angle constraints on tetrahedral cells (eight-tick / D=3 setting), without claiming a new physical law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.