cmMinor34Matrix
plain-language theorem explainer
Explicit 4×4 normal-form matrix for the Cayley–Menger minor that underlies cofactor (3,4) of a tetrahedron, written in the six squared edge lengths. Downstream cofactor-polynomial and dihedral-angle work cites it as the concrete matrix whose determinant is the named cofactor polynomial. The body is a matrix literal, not a derived construction.
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 & 0 & a_0 & a_1 \\ 1 & a_0 & 0 & a_3 \\ 1 & a_2 & a_4 & a_5 \end{pmatrix}.$$ This is the normal form of the minor obtained by deleting row $3$ and column $4$ from the $5\times 5$ Cayley–Menger matrix.
background
The ambient module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates. It is the cofactor analogue of the derivative module: dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives.
Squared edge data are packaged as SqEdges, i.e. maps $\mathrm{Fin},6\to\mathbb{R}$. The full Cayley–Menger matrix of a tetrahedron is $5\times 5$; cofactor $(i,j)$ is (up to sign) the determinant of the $4\times 4$ minor after deleting row $i$ and column $j$. This definition freezes the $(3,4)$ minor into a fixed entry pattern in those six coordinates.
Edge indexing follows the standard tetrahedron pairing used throughout the Cayley–Menger polynomial development: off-diagonal blocks hold the squared lengths $a_0,\ldots,a_5$ in the order that matches the ambient matrix construction.
proof idea
Pure definition by matrix literal. The four rows are written with !![·;·;·;·] notation: first row $(0,1,1,1)$, then the three edge-length rows that remain after deleting row 3 and column 4 from the Cayley–Menger pattern. No lemmas are applied; equality to the succAbove submatrix and the determinant identity are proved in sibling theorems.
why it matters
Gives a named, inspectable matrix so cofactor $(3,4)$ is not an opaque submatrix term. Two immediate consumers: the theorem that the raw Fin.succAbove submatrix of the Cayley–Menger matrix equals this normal form (proved by exhaustive fin_cases), and the theorem that its determinant equals $-$ the named cofactor polynomial cmCofactor3Poly 3 4. Those identities let dihedral-angle and hinge calculus differentiate and evaluate cofactors as ordinary polynomials in the six squared edges, which is the module’s stated purpose relative to Regge/TT geometry downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.