regularUnitOffDiagMinorMatrix
plain-language theorem explainer
The off-diagonal vertex minor of the regular unit tetrahedron Cayley-Menger matrix is the explicit 4×4 real matrix with 0 on the first three diagonal entries and 1 elsewhere (including the bottom-right corner). Anyone reducing regular-tetrahedron minors for the dihedral cosine formula cites this normal form. It is a pure matrix-literal definition, not a proved identity.
Claim. Let $M$ be the $4\times 4$ real matrix $$M=\begin{pmatrix}0&1&1&1\\1&0&1&1\\1&1&0&1\\1&1&1&1\end{pmatrix}.$$ This is the off-diagonal vertex minor of the Cayley-Menger matrix of the regular tetrahedron with all squared edge lengths equal to $1$.
background
The module links the explicit tetrahedral Cayley-Menger polynomial to the genuine $5\times 5$ Cayley-Menger determinant, supplying the determinant and cofactor layer used by the dihedral cosine formula. The ambient matrix convention borders a zero corner and a row/column of ones around the six squared edge lengths $a_0,\ldots,a_5$ of a tetrahedron.
For the regular unit case every squared edge length equals $1$. Deleting one border index and one vertex index produces a $4\times 4$ minor. The present definition freezes that minor in an explicit off-diagonal normal form: zeros on the first three diagonal slots, ones in every other entry.
Downstream, the $(3,4)$ submatrix of the regular-unit Cayley-Menger matrix is proved equal to this literal, so all later determinant and cofactor calculations can work with a fixed numeric matrix rather than a symbolic submatrix expression.
proof idea
Pure definition by matrix literal. The body is the Mathlib !![...; ...] notation for a $4\times 4$ real matrix; there is no proof obligation, no lemma application, and no tactic script.
why it matters
This normal form is the concrete object whose determinant is evaluated next: the sibling theorem proves $\det M=-1$ by expanding along the first row and reducing to a $3\times 3$ numeric determinant. A second sibling identifies the $(3,4)$ minor of the regular-unit Cayley-Menger matrix with $M$, so the determinant result transfers back to the geometric minor.
Together those facts feed the cofactor layer of the dihedral cosine formula for a regular tetrahedron. In the Recognition Science chain that formula sits inside the geometric consequences of $D=3$ spatial dimensions (forcing step T8) and the eight-tick octave structure that organises discrete edge data. The definition itself closes no open question; it is scaffolding that lets the determinant and minor-identification theorems stay short and numeric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.