cmMinor23Matrix
plain-language theorem explainer
Normal-form 4×4 real matrix for the (2,3) Cayley–Menger cofactor minor of a tetrahedron, written in the six squared edge lengths. Anyone expanding tetrahedral cofactors into named polynomials cites this literal. The body is a direct matrix constructor, not a derived identity.
Claim. Given squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & a_0 & a_2 \\ 1 & a_1 & a_3 & a_5 \\ 1 & a_2 & a_4 & 0 \end{pmatrix},$$ the normal form of the minor used by cofactor $(2,3)$.
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.
SqEdges is the type of squared edge lengths of a tetrahedron, indexed by Fin 6. The ambient object is the bordered Cayley–Menger matrix whose minors encode volumes and related geometric quantities; cofactor $(i,j)$ is (up to sign) the determinant of the complementary submatrix.
This definition freezes the particular $4\times 4$ pattern that appears when rows/columns corresponding to indices 2 and 3 are deleted, with edge squares placed in the standard CM ordering.
proof idea
Pure definition by matrix literal. No lemmas, tactics, or algebraic reduction: the four rows are written out with the constant border $(0,1,1,1)$ / $(1,\ldots)$ and the six squared-edge slots $a_0,\ldots,a_5$ in the positions required by the $(2,3)$ minor convention.
why it matters
Gives a concrete handle on cofactor $(2,3)$ so downstream results can avoid opaque submatrix notation. Immediately used by the equality theorem that identifies this literal with the actual submatrix of the full CM matrix after deleting row 2 and column 3, and by the determinant identity equating $\det$ of this matrix to $-$ the named cofactor polynomial at $(2,3)$. Those two facts are the cofactor analogue of the explicit CM polynomial/derivative pipeline: they let dihedral and volume calculus work with ring-normalized polynomials rather than fderiv terms. Sibling minors $(3,4)$ and $(2,4)$ play the same role for the other cofactor slots.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.