cmMinor24Matrix
plain-language theorem explainer
Defines the explicit 4×4 normal-form matrix for the Cayley–Menger minor that underlies cofactor (2,4) of a tetrahedron, with entries drawn from the six squared edge lengths. Downstream cofactor and dihedral calculus cite it to replace opaque submatrix extractions by a concrete array. The body is a literal matrix literal, not a derived construction.
Claim. For squared edge lengths $a \in \mathbb{R}^{6}$ of a tetrahedron, the normal-form minor matrix for cofactor $(2,4)$ is the $4\times 4$ real matrix whose first row is $(0,1,1,1)$, second row $(1,0,a_0,a_1)$, third row $(1,a_1,a_3,0)$, and fourth row $(1,a_2,a_4,a_5)$.
background
The ambient setting is explicit Cayley–Menger cofactor polynomials: every tetrahedral cofactor is expanded as a named polynomial in the six squared edge coordinates, so later dihedral-angle calculus can differentiate polynomials rather than opaque Fréchet derivatives.
Squared edge data are packaged as $a:\mathrm{Fin},6\to\mathbb{R}$. The full $5\times 5$ bordered Cayley–Menger matrix of a tetrahedron has a standard cofactor expansion; the minor obtained by deleting row index 2 and column index 4 is the geometric object this definition freezes into a concrete $4\times 4$ array.
The same module supplies the sibling normal form for the $(3,4)$ minor. Both feed determinant identities that identify those minors with the corresponding cofactor polynomials.
proof idea
Pure definition by matrix literal. No lemmas are applied; the six squared-edge slots $a,0,\ldots,a,5$ are placed by hand into the positions that the bordered Cayley–Menger layout assigns to the $(2,4)$ minor. Downstream equality-to-submatrix and determinant theorems simply unfold this literal and compute.
why it matters
Gives a stable normal form so that cmMinor24_submatrix_eq can prove the extracted submatrix of the full Cayley–Menger matrix equals this array by finite case analysis, and so that det_cmMinor24Matrix can evaluate the determinant by row expansion and ring normalization, equating it to the named cofactor polynomial cmCofactor3Poly 2 4.
That polynomial identity is the cofactor analogue of the explicit Cayley–Menger derivative layer: dihedral-angle formulas built from cofactors become ordinary polynomial calculus in the six edge squares. In the broader Recognition geometry stack this keeps volume and angle identities fully algebraic before any continuum limit or forcing-chain step is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.