cmMinor22Matrix
plain-language theorem explainer
Normal form of the 4×4 Cayley–Menger minor obtained by deleting index 2 from the bordered distance matrix of a tetrahedron. Anyone expanding the (2,2) cofactor as a polynomial in the six squared edge lengths cites this matrix. The body is a direct matrix literal in those coordinates; no proof is required.
Claim. Given squared edge lengths $a$ of a tetrahedron (six real coordinates), the normal form of the diagonal minor for the $(2,2)$ Cayley–Menger cofactor is the $4\times 4$ real matrix whose first row/column is the usual border $(0,1,1,1)$, whose $(1,1)$ block entry is $0$, and whose off-diagonal squared-distance entries are $a_1$, $a_2$, and $a_5$ in the standard edge indexing.
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 quote named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data are packaged as SqEdges: a map from Fin 6 to $\mathbb{R}$. The full $5\times 5$ Cayley–Menger matrix of a tetrahedron is bordered by a row and column of ones (with a zero corner); its cofactors encode volumes and, after normalization, cosines of dihedral angles.
The present matrix is the concrete $4\times 4$ minor that appears when the second row and column of that bordered matrix are deleted. Edge indices $1,2,5$ are exactly the three squared lengths that survive in that minor under the module’s fixed labeling of the six edges.
proof idea
Pure definition: a $4\times 4$ matrix literal. The first row and column are the standard Cayley–Menger border $(0,1,1,1)$; the remaining $3\times 3$ block places zeros on the diagonal and inserts the three surviving squared edges $a_1$, $a_2$, $a_5$ off-diagonal. No lemmas are invoked.
why it matters
This normal form is the bridge between the abstract submatrix of the full Cayley–Menger matrix and the named cofactor polynomial. Two immediate consumers sit in the same module: the theorem that the submatrix obtained by deleting index 2 equals this matrix entrywise, and the theorem that its determinant equals the explicit polynomial cmCofactor3Poly 2 2. Those identities let dihedral-angle derivatives be written as ordinary partials of a polynomial in the six squared edges, which is the module’s stated purpose (cofactor analogue of the Cayley–Menger derivative development).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.