regularUnitOffDiagMinorMatrix24
plain-language theorem explainer
Explicit $4\times 4$ real matrix equal to the $(2,4)$-minor of the Cayley-Menger matrix of the regular unit-edge tetrahedron. Geometry proofs that evaluate that minor or its determinant cite this constant. The body is a 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 & 0 \\ 1 & 1 & 1 & 1 \end{pmatrix}.$$ It is the concrete form of the minor obtained by deleting row $2$ and column $4$ from the $5\times 5$ Cayley-Menger matrix of a regular tetrahedron with all squared edge lengths equal to $1$.
background
The module links the explicit tetrahedral Cayley-Menger polynomial cm3 to the genuine $5\times 5$ Cayley-Menger determinant and its cofactors, the layer needed for dihedral cosines. Rows and columns are indexed $0..4$, with border row/column of ones, zeros on the squared-distance diagonal, and off-diagonal entries $a_0,\ldots,a_5$ the six squared edge lengths $(01),(02),(03),(12),(13),(23)$.
For the regular unit case every squared edge is $1$. Deleting row $2$ and column $4$ of that filled matrix yields a fixed $4\times 4$ pattern of zeros and ones; this definition names that pattern so later lemmas can compute its determinant and identify it with the corresponding submatrix of cmMatrix3 regularUnitSqEdges.
proof idea
Pure definition by matrix notation. The four rows are written out as the literal $$!![0,1,1,1;,1,0,1,1;,1,1,1,0;,1,1,1,1]$$ with no lemmas or tactics.
why it matters
Supplies the named matrix that two sibling theorems consume. det_regularUnitOffDiagMinorMatrix24 proves its determinant equals $1$ by expanding along the first row and reducing to a $3\times 3$ determinant. regularUnit_minor_24_eq_offDiag identifies it with the actual $(2,4)$-submatrix of the Cayley-Menger matrix on regular unit squared edges, by exhaustive entrywise check on Fin 4.
Those facts feed the cofactor/dihedral-cosine pipeline for the regular tetrahedron inside the Recognition geometry layer (volume and angle formulae built from Cayley-Menger data). No forcing-chain landmark (T5–T8) is touched directly; the object is pure Euclidean scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.