cmMinor13Matrix
plain-language theorem explainer
Explicit 4×4 normal-form matrix for the (1,3) cofactor minor of a tetrahedron's Cayley–Menger matrix, written in the six squared edge lengths. Anyone expanding CM cofactors into named polynomials for dihedral-angle calculus cites it. The body is a direct matrix literal, not a derived construction.
Claim. Given squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, the matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & a(0) & 0 & a(4) \\ 1 & a(1) & a(3) & a(5) \\ 1 & a(2) & a(4) & 0 \end{pmatrix}$$ is the normal form of the minor used by cofactor $(1,3)$.
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates. Downstream dihedral-angle calculus can then cite named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges, the type $\mathrm{Fin},6\to\mathbb{R}$: six real numbers packing the edge lengths of a tetrahedron. The ambient object is the bordered Cayley–Menger matrix whose minors control volumes and dihedral cosines.
Cofactor $(1,3)$ is one of the entries needed for those dihedral formulae. This definition freezes the corresponding $4\times 4$ minor into a concrete matrix so later lemmas can equate it to a submatrix extraction and evaluate its determinant by ring normalisation.
proof idea
Pure definition: a single matrix literal of type $\mathrm{Matrix},(\mathrm{Fin},4),(\mathrm{Fin},4),\mathbb{R}$. Entries are constants $0,1$ and selected components of the squared-edge vector $a$. No lemmas are applied; the construction is the normal form itself.
why it matters
Anchors the explicit-polynomial pipeline for cofactor $(1,3)$. Two immediate consumers: the theorem that this matrix equals the submatrix of the full CM matrix obtained by deleting row 1 and column 3, and the theorem that its determinant equals the named cofactor polynomial cmCofactor3Poly 1 3. Those equalities let dihedral-angle derivatives work with ring-normalised polynomials rather than symbolic fderiv terms, which is the module's stated purpose (cofactor analogue of CayleyMengerDerivatives).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.