cmMinor33Matrix
plain-language theorem explainer
Defines the explicit 4×4 normal-form matrix for the (3,3) diagonal minor of the tetrahedral Cayley–Menger matrix, with entries in the six squared edge lengths. Downstream cofactor and dihedral calculus cite it to replace opaque submatrix extractions by a concrete array. The body is a literal matrix literal in those coordinates.
Claim. For squared edge lengths $a \in \mathbb{R}^{6}$ of a tetrahedron, let $M_{33}(a)$ be the $4\times 4$ real matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & a_0 & a_2 \\ 1 & a_0 & 0 & a_4 \\ 1 & a_2 & a_4 & 0 \end{pmatrix}.$$ This is the normal form of the principal minor used by the Cayley–Menger cofactor at index $(3,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.
Squared edge data are packaged as SqEdges, an abbreviation for maps $\mathrm{Fin},6\to\mathbb{R}$. The ambient object is the bordered Cayley–Menger matrix of a tetrahedron; deleting row/column 3 yields a $4\times 4$ minor whose determinant is the corresponding cofactor polynomial.
This definition freezes that minor in a fixed coordinate order (border row of ones, then the three relevant squared lengths $a_0,a_2,a_4$ on the off-diagonals), matching the indexing used by the generated cofactor polynomials.
proof idea
Pure definition: a matrix literal. No proof obligations. The array is written with Mathlib’s !![·;·] syntax so that later simp and ring_nf steps on determinants see concrete entries rather than Matrix.submatrix projections.
why it matters
Feeds two immediate results in the same module: the equality theorem that identifies this array with the genuine submatrix of the full Cayley–Menger matrix after deleting index 3, and the determinant identity that equates $\det M_{33}(a)$ with the named cofactor polynomial at $(3,3)$. Those identities let dihedral-angle derivatives be rewritten as ordinary partials of explicit polynomials in the six edge squares, which is the module’s stated purpose (cofactor analogue of the Cayley–Menger derivative layer). In the broader Recognition geometry stack this supplies the algebraic substrate for volume and angle identities on the tetrahedron without leaving residual fderiv terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.