cmMinor34_submatrix_eq
plain-language theorem explainer
Deleting row 3 and column 4 from the 5×5 Cayley–Menger matrix of a tetrahedron yields exactly the explicit 4×4 normal form used for cofactor (3,4). Anyone computing tetrahedral cofactors as polynomials in the six squared edges cites this identification. The proof is entrywise exhaustion on Fin 4 × Fin 4 by reflexivity.
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 row $3$ and column $4$ equals the explicit normal-form matrix whose entries are $0$, $1$, and the coordinates of $a$ in the standard pattern for cofactor $(3,4)$.
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 squared edge lengths of a tetrahedron, indexed by Fin 6. The Cayley–Menger matrix cmMatrix3 a is the standard $5\times 5$ bordered matrix built from those six squared lengths (zeros on the spatial diagonal block, ones in the bordering row and column, and squared distances off-diagonal).
Cofactor $(3,4)$ is $(-1)^{3+4}$ times the determinant of the minor that deletes row $3$ and column $4$. That minor is written abstractly via Matrix.submatrix and Fin.succAbove. The sibling definition cmMinor34Matrix packages the same $4\times 4$ array in an explicit !![...] normal form with concrete placements of $a,0,\ldots,a,5$.
proof idea
Pointwise matrix extensionality on indices $i,j:\mathrm{Fin},4$. Each index is discharged by fin_cases, giving a $4\times 4$ grid of goals. Every goal is definitional equality between the corresponding entry of the succAbove submatrix of cmMatrix3 a and the matching entry of cmMinor34Matrix a, closed by rfl. No algebraic lemmas are needed beyond the definitions of the two matrices.
why it matters
This lemma is the bridge from the abstract cofactor (submatrix-plus-sign) to the named polynomial form. Downstream, cmCofactor3_34_eq_poly rewrites the abstract minor via this equality, applies the explicit determinant identity det_cmMinor34Matrix, and simplifies the sign, proving that cofactor $(3,4)$ equals the packaged polynomial cmCofactor3Poly 3 4. That agreement is the numerator side for edge $0$ in the cofactor-polynomial calculus that feeds dihedral-angle derivatives.
In the broader Recognition geometry stack, explicit Cayley–Menger cofactors support hinge-aware and Regge-type calculations on tetrahedral complexes. The result itself is pure linear algebra of the CM matrix; it does not invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it supplies the concrete algebraic substrate those geometric layers consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.