cmMinor00_submatrix_eq
plain-language theorem explainer
The (0,0)-minor of the 5×5 Cayley–Menger matrix of a tetrahedron equals the explicit 4×4 matrix of squared edge lengths written by hand. Anyone computing the (0,0) cofactor as a polynomial cites this identification. The proof is pure case analysis on Fin 4 indices, each entry matching by definition.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the $4\times 4$ submatrix of the Cayley–Menger matrix obtained by deleting the first row and first column equals the explicit matrix $$\begin{pmatrix}0&a_0&a_1&a_2\\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 use named polynomial partials rather than opaque Fréchet derivatives.
Squared edge lengths are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The $5\times 5$ Cayley–Menger matrix cmMatrix3 has a zero in the $(0,0)$ corner, ones along the rest of the border, and the six squared lengths (with zeros on the diagonal) in the lower-right $4\times 4$ block. The named matrix cmMinor00Matrix is exactly that lower-right block written as a literal $4\times 4$ array.
This lemma asserts that deleting row 0 and column 0 via Matrix.submatrix recovers that literal array, so later determinant and cofactor identities can switch freely between the abstract minor and the concrete polynomial matrix.
proof idea
Term-mode proof by extensionality on matrix entries. After ext i j, both indices run over Fin 4. Nested fin_cases exhausts the sixteen pairs; each goal reduces to definitional equality (rfl) between the corresponding entry of the submatrix of cmMatrix3 and the hard-coded entry of cmMinor00Matrix. No algebraic lemmas are required.
why it matters
Feeds directly into cmCofactor3_00_eq_poly, which rewrites the abstract $(0,0)$ cofactor of the Cayley–Menger matrix as the named polynomial cmCofactor3Poly 0 0. That equality is the cofactor analogue of the derivative expansions in CayleyMengerDerivatives: once the minor is identified with an explicit matrix, its determinant becomes a concrete polynomial in the six squared edges, and partial derivatives needed for dihedral-angle calculus are ordinary polynomial derivatives.
In the broader Recognition geometry stack this sits under the Cayley–Menger infrastructure used for tetrahedral volume and angle identities; it does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law, but it clears scaffolding so those geometric identities can be stated without opaque matrix minors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.