regularUnitOffDiagMinorMatrix14
plain-language theorem explainer
Explicit 4×4 real matrix that is the off-diagonal minor obtained by deleting row 1 and column 4 from the Cayley–Menger matrix of the regular unit tetrahedron. Anyone computing that minor’s determinant or matching submatrices to closed forms will cite it. The body is a pure matrix literal in Mathlib notation; no proof obligations.
Claim. Define the $4\times 4$ real matrix $$\begin{pmatrix} 0 & 1 & 1 & 1 \\ 1 & 1 & 0 & 1 \\ 1 & 1 & 1 & 0 \\ 1 & 1 & 1 & 1 \end{pmatrix}.$$ It is the concrete off-diagonal minor used for the regular unit tetrahedron (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 layer is required by the dihedral cosine formula.
Row/column convention for the $5\times 5$ matrix places a border of ones around a $4\times 4$ block of squared edge lengths $a_0,\ldots,a_5$ for edges $(01),(02),(03),(12),(13),(23)$, with zeros on the geometric diagonal. For the regular unit tetrahedron every squared edge length is $1$.
Deleting one border row and one geometric column yields a $4\times 4$ minor. The present definition freezes that minor in the regular-unit case as an explicit matrix, so later lemmas can compute its determinant and identify it with a submatrix of the full Cayley–Menger matrix.
proof idea
Definition only: the body is Mathlib’s !![ ... ] matrix literal writing the four rows of reals above. No tactics, no lemmas, no unfolding of other defs inside the body.
why it matters
Two immediate consumers sit in the same module. det_regularUnitOffDiagMinorMatrix14 unfolds this matrix and obtains $\det=-1$ via expansion along the first row and a $3\times 3$ determinant. regularUnit_minor_14_eq_offDiag proves that the $(1,4)$-submatrix of cmMatrix3 regularUnitSqEdges equals this literal, so the determinant result transfers to the geometric minor.
Together those facts feed the cofactor arithmetic that turns the Cayley–Menger determinant into dihedral cosines for the regular tetrahedron. In the broader Recognition geometry stack this is bookkeeping for rigid simplex data (edge lengths, volumes, angles), not a forcing-chain step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.