det_regularUnitOffDiagMinorMatrix13
plain-language theorem explainer
The 4×4 off-diagonal minor that appears when deleting row 1 and column 3 from the regular unit tetrahedron Cayley–Menger matrix has determinant exactly 1. Anyone computing cofactors or dihedral cosines for the regular unit case cites this evaluation. The proof unfolds the explicit matrix, expands along the first row, and finishes by the closed 3×3 determinant formula.
Claim. Let $M$ be the explicit $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}.$$ Then $\det M=1$.
background
The module builds the determinant and cofactor layer that links the tetrahedral Cayley–Menger polynomial cm3 to the genuine $5\times 5$ Cayley–Menger matrix. Rows and columns are indexed $0..4$, with the border of ones and squared edge lengths $a_0..a_5$ in the interior block.
For the regular unit tetrahedron every squared edge equals 1. The minor obtained by deleting row 1 and column 3 is not the raw submatrix of that Cayley–Menger matrix; after the usual sign and reordering conventions it becomes the concrete $4\times 4$ matrix displayed above (called the regular-unit off-diagonal minor matrix for indices 1,3).
That matrix is supplied as an explicit definition; the present theorem simply evaluates its determinant.
proof idea
Term-mode proof. Unfold the named matrix definition, then rewrite by the Laplace expansion along the first row (Matrix.det_succ_row_zero). The resulting sum over a Fin 4 index collapses by Fin.sum_univ_succ and Fin.succAbove; each surviving $3\times 3$ block is evaluated by Matrix.det_fin_three. The arithmetic simplifies to 1.
why it matters
Feeds directly into regularUnit_cofactor_13, which asserts that the $(1,3)$-cofactor of the regular-unit Cayley–Menger matrix equals 1. That cofactor is an ingredient of the dihedral-cosine formula for a regular tetrahedron, the geometric side of the Recognition Science forcing chain that recovers $D=3$ spatial dimensions (T8) and the eight-tick octave structure. Without the determinant evaluation the cofactor identity cannot close, so the regular-unit specialisation of the whole cofactor layer would remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.