regularUnitOffDiagMinorMatrix12
plain-language theorem explainer
Explicit 4×4 real matrix equal to the (1,2)-minor of the Cayley–Menger matrix of a regular unit tetrahedron (all squared edge lengths 1). Geometers computing dihedral cosines via CM cofactors cite it as the concrete off-diagonal block. The body is a literal matrix literal, not a derived construction.
Claim. Let $M$ be the $4\times 4$ real matrix $$M=\begin{pmatrix}0&1&1&1\\1&1&1&1\\1&1&0&1\\1&1&1&0\end{pmatrix}.$$ This is the off-diagonal minor obtained by deleting row/column indices corresponding to the first two edge-label slots from the $5\times 5$ Cayley–Menger matrix of the regular unit tetrahedron.
background
The module realises the tetrahedral Cayley–Menger determinant as an explicit $5\times 5$ matrix whose border is the usual $0/1$ pattern and whose interior holds the six squared edge lengths $a_0,\ldots,a_5$ in the order $(01),(02),(03),(12),(13),(23)$. Minors and cofactors of that matrix feed the classical dihedral-cosine formulae.
A regular unit tetrahedron has every squared edge length equal to $1$. Deleting the pair of rows and columns indexed by the first two non-border slots leaves a concrete $4\times 4$ pattern of zeros and ones; the present definition freezes that pattern as a named matrix so later determinant and equality lemmas can refer to it by a single identifier.
No upstream lemmas are required: the object is pure data.
proof idea
Definition by matrix literal. The four rows are written with Mathlib’s !![·;·] notation; entries are the constants $0$ and $1$ in $\mathbb{R}$. There is no proof obligation beyond type-checking the $4\times 4$ shape on Fin 4.
why it matters
Two immediate consumers sit in the same module. det_regularUnitOffDiagMinorMatrix12 evaluates $\det M=-1$ by expanding along the first row and reducing to a $3\times 3$ determinant. regularUnit_minor_12_eq_offDiag proves that the actual submatrix of cmMatrix3 at the regular-unit edge vector equals this literal matrix, so the determinant result transfers to the geometric minor.
Together they supply the numerical cofactor data needed when the dihedral cosine formula is specialised to the regular tetrahedron. In the broader Recognition geometry layer this is bookkeeping for the rigid simplex whose edge lengths sit on the $\varphi$-ladder; it does not itself invoke T5–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.