regularUnitOffDiagMinorMatrix13
plain-language theorem explainer
Explicit 4×4 real matrix equal to the (1,3)-minor of the Cayley–Menger matrix of the regular unit tetrahedron (all squared edges 1). Geometers computing tetrahedral dihedral cosines via cofactors cite it as the concrete off-diagonal block. It is a pure 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&0&1\\1&1&1&1\\1&1&1&0\end{pmatrix}.$$ This is the matrix obtained by deleting row index $1$ and column index $3$ from the $5\times 5$ Cayley–Menger matrix of the regular unit tetrahedron (all six 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 classical tool for volume and, via cofactors, for dihedral cosines.
Row/column layout of the full matrix is fixed: index $0$ is the bordering $0/1$ row and column; indices $1..4$ carry the six squared edge lengths $a_0,\ldots,a_5$ corresponding to edges $(01),(02),(03),(12),(13),(23)$, with zeros on the spatial diagonal. A regular unit tetrahedron sets every $a_i=1$.
Deleting one bordering-spatial pair of indices leaves a $4\times 4$ minor. The present definition records that minor for the concrete pair (row $1$, column $3$) after the regular-unit specialization, written as an explicit matrix literal so later determinant and equality proofs can unfold it by name.
proof idea
Definition by matrix notation only. The body is the four-row literal
!![0,1,1,1; 1,1,0,1; 1,1,1,1; 1,1,1,0]
with no lemmas, tactics, or computation. Downstream theorems unfold this name and evaluate entries or the determinant directly.
why it matters
Supplies the concrete $4\times 4$ block needed by two sibling results in the same module. det_regularUnitOffDiagMinorMatrix13 proves its determinant equals $1$ by expanding along the first row and reducing to a $3\times 3$ determinant. regularUnit_minor_13_eq_offDiag identifies it with the actual submatrix of cmMatrix3 regularUnitSqEdges after deleting indices $1$ and $3$ via Fin.succAbove.
Those facts feed the cofactor arithmetic behind the dihedral-cosine formula for a regular tetrahedron. In the broader Recognition geometry stack this is scaffolding for rigid simplex geometry (edge-length constraints, volume signs, angle extraction), not a forcing-chain step itself. It closes the gap between the symbolic polynomial cm3 and entrywise matrix algebra Mathlib can decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.