regularUnit_minor_13_eq_offDiag
plain-language theorem explainer
The (1,3)-minor of the 5×5 Cayley-Menger matrix for the unit regular tetrahedron equals an explicit 4×4 off-diagonal pattern matrix. Anyone computing regular-tetrahedron cofactors or dihedral cosines cites this. The proof is pure entrywise exhaustion: extensionality plus 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$). Deleting row $1$ and column $3$ yields exactly the fixed $4\times 4$ matrix $$\begin{pmatrix}0&1&1&1\\1&1&0&1\\1&1&1&1\\1&1&1&0\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/columns are indexed $0..4$, with the usual border of zeros and ones and the six squared edge lengths $a_0..a_5$ filling the interior.
cmMatrix3 builds that matrix from any six-tuple of squared lengths. regularUnitSqEdges is the constant-1 edge data (unit regular tetrahedron). The target matrix regularUnitOffDiagMinorMatrix13 is the concrete $4\times 4$ pattern obtained by deleting row 1 and column 3 of that regular case.
The minor is formed by Matrix.submatrix with the two Fin.succAbove maps that skip indices 1 and 3 respectively.
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 off-diagonal target matrix, cmMatrix3, regularUnitSqEdges (every squared length is 1), and Fin.succAbove. No external lemmas beyond definitional unfolding.
why it matters
Feeds directly into regularUnit_cofactor_13, which unfolds the cofactor, inserts the even-sign factor, rewrites the minor via this equality, and evaluates the determinant of the off-diagonal pattern to conclude the 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 anchors the regular-unit special case used when relating edge data to solid angles and volume identities (classically $288V^2=4$ for the unit regular tetrahedron).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.