cmMinor01Matrix
plain-language theorem explainer
Names the explicit 4×4 real matrix obtained by deleting the first row and second column of the tetrahedral Cayley–Menger matrix, with entries filled from the six squared edge lengths. Downstream cofactor and dihedral calculus cites it to replace opaque submatrix extractions by a concrete array. The body is a literal matrix literal; no proof.
Claim. For squared edge lengths $a\colon\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, define the $4\times 4$ matrix $$M_{01}(a)=\begin{pmatrix}1&a_0&a_1&a_2\\1&0&a_3&a_4\\1&a_3&0&a_5\\1&a_4&a_5&0\end{pmatrix}.$$
background
The ambient module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so dihedral-angle calculus can quote named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data are packaged as SqEdges: a map from Fin 6 into $\mathbb{R}$, one coordinate per edge of the complete graph $K_4$. The full $5\times 5$ bordered Cayley–Menger matrix (imported from the Cayley–Menger matrix module) has first row/column of the form $(0,1,1,1,1)$ and off-diagonal blocks filled by those squared lengths. Deleting row index $0$ and column index $1$ yields a concrete $4\times 4$ minor whose determinant is (up to sign) the $(0,1)$-cofactor polynomial.
This definition simply writes that minor out entrywise, so later equalities and determinant expansions never have to re-derive the pattern of zeros and ones.
proof idea
Pure definition: a single matrix literal whose twelve nontrivial entries are the six squared lengths $a_0,\ldots,a_5$ placed in the standard Cayley–Menger pattern, with zeros on the three diagonal slots that correspond to vertex self-distances. No lemmas or tactics are invoked.
why it matters
Feeds two immediate parents in the same module. The first proves that the abstract submatrix of the full Cayley–Menger matrix obtained by succAbove 0 on rows and succAbove 1 on columns equals this named array, discharging the bookkeeping once and for all. The second expands its determinant and identifies it with $-$ the explicit cofactor polynomial cmCofactor3Poly 0 1, via the usual Laplace expansion along the first row and a ring normalization.
Those cofactor polynomials are the algebraic backbone for dihedral-angle derivatives in the Recognition geometry stack: once every minor is a named polynomial in the six edge squares, partial derivatives become ordinary polynomial calculus rather than symbolic fderiv terms. The construction is the cofactor-side twin of the earlier Cayley–Menger derivative module and sits entirely inside classical Euclidean tetrahedron geometry; it does not itself invoke the forcing chain or $\varphi$-ladder, but supplies the coordinate algebra those later geometric claims rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.