regularUnitOffDiagMinorMatrix23
plain-language theorem explainer
Explicit 4×4 real matrix that is the (2,3)-minor of the Cayley–Menger matrix of the regular unit tetrahedron after deleting the corresponding row and column. Anyone computing dihedral cosines or CM determinants for the regular case cites it as the concrete off-diagonal minor. The body is a literal matrix literal, not a derived construction.
Claim. Define the $4\times 4$ real matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 0 & 1 & 1 \\ 1 & 1 & 1 & 1 \\ 1 & 1 & 1 & 0 \end{pmatrix}.$$ It is the candidate for the minor obtained by deleting row 2 and column 3 from the $5\times 5$ Cayley–Menger matrix of the regular tetrahedron with all squared edge lengths equal to $1$.
background
The module builds the determinant and cofactor layer that links the explicit tetrahedral Cayley–Menger polynomial cm3 to the genuine $5\times 5$ Cayley–Menger determinant. That determinant is the algebraic engine behind the dihedral-cosine formula for a tetrahedron.
Row/column convention places a bordering row and column of ones, a zero diagonal on the edge block, and squared edge lengths $a_0,\ldots,a_5$ in the off-diagonal edge positions corresponding to pairs $(01),(02),(03),(12),(13),(23)$. A minor is the $4\times 4$ submatrix after deleting one index from that $5\times 5$ array.
For the regular unit tetrahedron every squared edge length is $1$. The matrix defined here is the concrete numerical minor that arises when indices $2$ and $3$ are deleted; downstream lemmas identify it with the corresponding submatrix of the symbolic CM matrix and evaluate its determinant.
proof idea
Pure definition by matrix literal. The four rows are written with Mathlib’s !![...; ...] notation; no lemmas or tactics are invoked. Downstream proofs unfold the name and either compute the determinant by cofactor expansion along the first row or prove entrywise equality with a submatrix of cmMatrix3 regularUnitSqEdges.
why it matters
Supplies the concrete minor needed for the regular-unit specialization of the Cayley–Menger cofactor calculus. Parent theorem det_regularUnitOffDiagMinorMatrix23 shows its determinant equals $-1$. Parent theorem regularUnit_minor_23_eq_offDiag identifies it with the actual $(2,3)$-minor of cmMatrix3 on regular unit squared edges, so the determinant result transfers to the geometric CM matrix.
That pair of facts is the algebraic checkpoint before dihedral cosines and volume formulae for the regular tetrahedron. In the broader Recognition geometry stack, controlled CM minors feed rigidity and embedding statements that sit under the $D=3$ forcing (T8) and the discrete geometric scaffolding of the framework; this definition is the numerical seed for the regular case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.