regularUnit_minor_12_eq_offDiag
plain-language theorem explainer
For the unit regular tetrahedron, the Cayley–Menger 5×5 matrix with row 1 and column 2 deleted equals an explicit 4×4 off-diagonal minor matrix. Anyone computing the (1,2) cofactor or dihedral cosine for the regular case cites this identification. The proof is entrywise exhaustion on Fin 4 via fin_cases 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$). Then the $4\times 4$ submatrix obtained by deleting row $1$ and column $2$ equals the explicit matrix $$\begin{pmatrix}0&1&1&1\\1&1&1&1\\1&1&0&1\\1&1&1&0\end{pmatrix}.$$
background
This module links the explicit tetrahedral Cayley–Menger polynomial cm3 to the genuine $5\times 5$ Cayley–Menger determinant, the determinant/cofactor layer used by the dihedral cosine formula. Rows and columns are indexed $0..4$, with border ones in the first row/column, zeros on the spatial diagonal, and the six squared edge lengths $(01),(02),(03),(12),(13),(23)$ filling the off-diagonal spatial block.
cmMatrix3 builds that matrix from a six-tuple of squared lengths. regularUnitSqEdges is the constant tuple of ones: the unit regular tetrahedron. regularUnitOffDiagMinorMatrix12 is the concrete $4\times 4$ matrix that the deleted-(1,2) minor is claimed to equal, written with Mathlib matrix notation.
The minor itself is formed by Matrix.submatrix with Fin.succAbove 1 on rows and Fin.succAbove 2 on columns, i.e. the standard delete-row-$i$/delete-column-$j$ embedding of $\mathrm{Fin},4$ into $\mathrm{Fin},5$.
proof idea
Entrywise identity on $\mathrm{Fin},4\times\mathrm{Fin},4$. Apply ext i j, then fin_cases on both indices (sixteen constant cases). Each case reduces by simp unfolding regularUnitOffDiagMinorMatrix12, cmMatrix3, regularUnitSqEdges, and Fin.succAbove, so the deleted-row/column indexing and the all-ones edge data match the hardcoded entries. No external lemmas beyond definitional unfolding.
why it matters
Feeds directly into regularUnit_cofactor_12, which proves that the $(1,2)$ cofactor of the unit-regular Cayley–Menger matrix equals $1$. That proof rewrites the minor via this equality, then evaluates det_regularUnitOffDiagMinorMatrix12 and normalizes.
In the broader geometry stack, cofactors of the Cayley–Menger matrix enter the dihedral cosine formula for a tetrahedron. The regular unit case is the calibration point (classical volume $\sqrt{2}/12$, Cayley–Menger value $4$). Pinning the off-diagonal minor by a proved matrix identity keeps the cofactor computation fully formal rather than by hand inspection.
Within Recognition Science geometry, this is infrastructure for rigid simplex geometry on the phi-ladder side, not a forcing-chain step (T0–T8) itself; it closes a concrete determinant identity needed before cosine or volume corollaries can cite a Lean cofactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.