cmMinor12_submatrix_eq
plain-language theorem explainer
Deleting row index 1 and column index 2 from the 5×5 Cayley–Menger matrix of a tetrahedron yields a fixed 4×4 normal-form matrix in the six squared edge lengths. Anyone equating abstract CM cofactors to explicit polynomials cites this identity. The proof is a finite case split on the remaining indices with definitional equality.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the $4\times 4$ submatrix of the Cayley–Menger matrix $C(a)$ obtained by deleting row $1$ and column $2$ equals the explicit normal-form matrix whose entries are $0$, $1$, and the coordinates of $a$ in the standard cofactor-$(1,2)$ layout.
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.
SqEdges is the type of squared edge lengths of a tetrahedron (maps Fin 6 → ℝ). The Cayley–Menger matrix cmMatrix3 a is the standard $5\times 5$ bordered matrix built from those lengths: zeros on the geometric diagonal block corners, ones in the bordering row and column, and squared distances off-diagonal.
The target normal form cmMinor12Matrix a is the concrete $4\times 4$ matrix
$$\begin{pmatrix}0&1&1&1\1&a_0&a_3&a_4\1&a_1&0&a_5\1&a_2&a_5&0\end{pmatrix},$$
the layout used for cofactor $(1,2)$.
proof idea
Pointwise extensionality on the $4\times 4$ index set, then exhaustive fin_cases on both remaining indices. Each of the sixteen entries reduces by rfl to the corresponding clause of cmMatrix3 versus the hard-coded normal form, so the submatrix obtained by succAbove 1 on rows and succAbove 2 on columns is definitionally the named minor matrix.
why it matters
Feeds directly into cmCofactor3_12_eq_poly, which rewrites the abstract cofactor cmCofactor3 a 1 2 as the named polynomial cmCofactor3Poly 1 2 a by substituting this submatrix identity and the determinant expansion of the normal form. That equality is the cofactor analogue of the Cayley–Menger derivative expansions: once every minor is pinned to a polynomial, partial derivatives of dihedral data become ordinary polynomial calculus on squared edges. Sibling lemmas do the same for the other index pairs needed by the full cofactor table. No Recognition forcing-chain step is touched here; the result is pure classical geometry scaffolding for later RS geometric identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.