cmMinor00Matrix
plain-language theorem explainer
Defines the explicit 4×4 matrix obtained by deleting the first row and column of the tetrahedral Cayley–Menger matrix, with entries the six squared edge lengths. Downstream cofactor and dihedral calculus cite it as a named polynomial matrix rather than an opaque submatrix. The body is a literal matrix literal in the six coordinates.
Claim. Given six squared edge lengths $a_0,\ldots,a_5$ of a tetrahedron, form the symmetric $4\times 4$ real matrix whose diagonal is zero and whose off-diagonal entries are $a_0,a_1,a_2$ in the first row/column, $a_3,a_4$ in the second, and $a_5$ in the $(2,3)$ block: $$\begin{pmatrix}0&a_0&a_1&a_2\\a_0&0&a_3&a_4\\a_1&a_3&0&a_5\\a_2&a_4&a_5&0\end{pmatrix}.$$
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.
Squared edge data are packaged as a map from $\mathrm{Fin},6$ to $\mathbb{R}$: the six independent squared lengths of a tetrahedron. The full $5\times 5$ Cayley–Menger matrix for a tetrahedron has a bordered structure with a zero diagonal block of squared distances; deleting its first row and column yields a $4\times 4$ principal minor whose entries are exactly those six squared lengths arranged symmetrically.
This definition freezes that minor as a concrete matrix-valued function of the edge vector, matching the pattern used for the other indexed minors in the same file.
proof idea
Pure definition: a matrix literal. No proof obligations. The six coordinates of the squared-edge vector are placed in the unique symmetric positions off the zero diagonal, matching the standard Cayley–Menger minor layout after deleting index 0.
why it matters
Named entry point for the $(0,0)$ cofactor polynomial of the tetrahedral Cayley–Menger determinant. The equality theorem immediately below identifies it with the actual submatrix of the ambient CM matrix, and the determinant theorem equates $\det$ of this matrix to the explicit cofactor polynomial at indices $(0,0)$. Those two results feed the module’s program of replacing opaque cofactors by named polynomials in the six edge squares, which downstream dihedral calculus consumes. Within Recognition geometry this is scaffolding for volume and angle identities on the tetrahedron, not a forcing-chain step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.