cmMinor32Matrix
plain-language theorem explainer
Explicit 4×4 matrix in the six squared edge lengths that realizes the (3,2)-minor of the tetrahedral Cayley–Menger matrix. Cofactor and dihedral-angle calculus cite it so determinants and partials refer to a named carrier instead of opaque submatrix extractions. The body is a single matrix literal.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ real matrix whose rows are $(0,1,1,1)$, $(1,0,a_1,a_2)$, $(1,a_0,a_3,a_4)$, and $(1,a_2,a_5,0)$.
background
The module expands every tetrahedral Cayley–Menger cofactor into 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, an abbreviation for maps $\mathrm{Fin},6\to\mathbb{R}$. The ambient object is the bordered Cayley–Menger matrix of a tetrahedron; deleting one row and one column yields a $4\times 4$ minor whose determinant is (up to sign) a cofactor polynomial in those six coordinates.
This definition freezes the concrete minor obtained by removing the row indexed $3$ and the column indexed $2$, written out entrywise in the edge coordinates $a_0,\ldots,a_5$.
proof idea
Pure definition: a single $4\times 4$ matrix literal. No lemmas or tactics. Downstream equality to the abstract submatrix is proved by ext plus exhaustive fin_cases and rfl; the determinant identity unfolds the literal and reduces by the usual Laplace expansion along the first row.
why it matters
Supplies the named carrier for the $(3,2)$-cofactor of the tetrahedral Cayley–Menger matrix. Immediate consumers are the submatrix identification theorem (the literal equals the corresponding submatrix of the full bordered matrix) and the determinant theorem (its det equals the negative of the explicit cofactor polynomial at indices $(3,2)$).
Those identities let dihedral-angle derivatives be written as ordinary partials of named polynomials rather than derivatives of opaque matrix constructions, which is the module’s stated purpose. In the broader Recognition geometry stack 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.