cmMinor03Matrix
plain-language theorem explainer
Explicit 4×4 matrix equal to the (0,3)-minor of the bordered Cayley–Menger matrix of a tetrahedron, written in the six squared edge lengths. Cofactor and dihedral-angle developments cite it so determinants and partials refer to a named matrix rather than an opaque submatrix extraction. The body is a single matrix literal; no proof content.
Claim. Given squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ real matrix whose rows are $(1,0,a_0,a_2)$, $(1,a_0,0,a_4)$, $(1,a_1,a_3,a_5)$, and $(1,a_2,a_4,0)$.
background
The module expands every tetrahedral Cayley–Menger cofactor as an explicit polynomial in the six squared edge coordinates, so downstream dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives.
Squared edge data are packaged as SqEdges: maps $\mathrm{Fin},6\to\mathbb{R}$. The full bordered Cayley–Menger matrix for a tetrahedron is $5\times 5$; deleting one row and one column yields a $4\times 4$ minor whose determinant (up to sign) is a cofactor. This definition writes the minor that drops index $0$ on rows and index $3$ on columns as a concrete matrix in those six coordinates.
Sibling definitions treat the other index pairs the same way (cmMinor34Matrix, cmMinor24Matrix, …), giving a uniform dictionary from cofactor indices to matrix literals.
proof idea
Definition only: the right-hand side is the Mathlib matrix literal with the four rows above. No tactics, no lemmas. Equality to the actual submatrix of the bordered Cayley–Menger matrix is proved separately by exhaustive fin_cases and rfl.
why it matters
Parent results are the identification theorem that this matrix equals the $(0,3)$-submatrix of the bordered Cayley–Menger matrix, and the determinant identity that its det equals the negative of the explicit cofactor polynomial at indices $(0,3)$. Those two facts turn cofactor extraction into ring arithmetic on named polynomials, which is the module’s purpose: feed dihedral-angle derivatives without residual fderiv opacity.
In the broader geometry stack this sits under Cayley–Menger volume and angle machinery used when Recognition Science forces $D=3$ spatial dimensions (forcing chain T8) and needs explicit tetrahedral edge calculus. It does not itself touch the J-cost or the eight-tick octave; it is pure classical geometry scaffolding for later RS geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.