regularUnit_minor_24_eq_offDiag
plain-language theorem explainer
The (2,4)-minor of the 5×5 Cayley-Menger matrix for the unit regular tetrahedron equals an explicit 4×4 matrix with a characteristic off-diagonal pattern. Anyone computing that cofactor (or the dihedral cosine) cites this identification. The proof is pure entrywise exhaustion: extensionality, fin_cases on both indices, and simp against the matrix definitions.
Claim. Let $M$ be the $5\times 5$ Cayley-Menger matrix of the unit regular tetrahedron (all six squared edge lengths equal to $1$). Deleting row $2$ and column $4$ yields the $4\times 4$ matrix $$\begin{pmatrix}0&1&1&1\\1&0&1&1\\1&1&1&0\\1&1&1&1\end{pmatrix}.$$
background
This module links the explicit tetrahedral Cayley-Menger polynomial cm3 to the genuine $5\times 5$ determinant and its cofactors, the layer needed by the dihedral cosine formula. Rows and columns are indexed $0..4$, with the border of ones in the zeroth row/column and the six squared edge lengths $a_0..a_5$ filling the lower-right $4\times 4$ block in the standard order $(01),(02),(03),(12),(13),(23)$.
cmMatrix3 is that matrix as a function of the six squared lengths. regularUnitSqEdges is the constant edge data with every squared length equal to $1$ (the unit regular tetrahedron; classically $288V^2=4$). The target matrix regularUnitOffDiagMinorMatrix24 is the hardcoded $4\times 4$ array that the deleted-$(2,4)$ submatrix is claimed to equal.
proof idea
Term-mode proof by matrix extensionality. After ext i j, both indices run over Fin 4. Nested fin_cases expands all sixteen entries; each reduces by simp against the definitions of the target off-diagonal matrix, of cmMatrix3, of the constant unit edge data, and of Fin.succAbove (which implements row/column deletion). No external lemmas beyond those unfoldings are required.
why it matters
Immediate parent is regularUnit_cofactor_24, which unfolds the cofactor, inserts the even-parity sign, rewrites via this equality, and evaluates det_regularUnitOffDiagMinorMatrix24 to conclude that the $(2,4)$-cofactor equals $1$. That cofactor value is part of the determinant/cofactor layer the module supplies for the dihedral cosine formula on a tetrahedron. In the Recognition geometry stack this is concrete linear-algebra bookkeeping for the regular unit case, not a forcing-chain step, but it closes an explicit matrix identity needed before volume and angle identities can be read off the Cayley-Menger determinant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.