cmMinor10Matrix
plain-language theorem explainer
Explicit 4×4 matrix whose entries are the six squared edge lengths of a tetrahedron (plus a border of ones), equal to the Cayley–Menger matrix with row 1 and column 0 deleted. Downstream cofactor and dihedral calculus cite it to replace opaque submatrix extractions by a named polynomial object. The body is a literal matrix literal, not a derived construction.
Claim. For squared edge lengths $a\colon\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ real matrix $$\begin{pmatrix} 1 & 1 & 1 & 1 \\ 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.
SqEdges is the type of maps from six indices to reals: the squared lengths of the six edges of a tetrahedron. The ambient object is the bordered Cayley–Menger matrix cmMatrix3 built from those lengths; cofactors of that matrix control volume and dihedral geometry.
This definition freezes the concrete $4\times 4$ minor obtained by deleting row index 1 and column index 0 of that $5\times 5$ matrix, writing every entry directly in the six edge coordinates.
proof idea
Pure definition by matrix literal. No lemmas are applied: the four rows are written out with ones on the border row and the squared-edge coordinates $a_0,\ldots,a_5$ in the pattern matching the $(1,0)$-minor of the Cayley–Menger matrix. Downstream equality to Matrix.submatrix is proved separately by exhaustive fin_cases.
why it matters
Feeds two immediate parents: the submatrix identity equating this literal to the deleted-row/column minor of cmMatrix3, and the determinant identity det = -cmCofactor3Poly 1 0, which expands that cofactor as an explicit polynomial.
Those expansions are the cofactor analogue of the Cayley–Menger derivative module: once every cofactor is a named polynomial in the six squared edges, partial derivatives needed for dihedral-angle formulae become ordinary polynomial calculus rather than abstract fderiv terms. In the Recognition geometry stack this keeps tetrahedral volume and angle identities fully algebraic in the edge ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.