det_regularUnitOffDiagMinorMatrix24
plain-language theorem explainer
The determinant of a fixed 4×4 real matrix arising as the (2,4) off-diagonal minor of the regular unit tetrahedron Cayley–Menger matrix equals 1. Anyone computing cofactors or dihedral cosines for the regular unit case cites this. The proof unfolds the matrix, expands the determinant along the first row, and evaluates the resulting 3×3 determinants by direct arithmetic.
Claim. Let $M$ be the $4\times 4$ real matrix $$M=\begin{pmatrix}0&1&1&1\\1&0&1&1\\1&1&1&0\\1&1&1&1\end{pmatrix}.$$ Then $\det M=1$.
background
This module links the explicit tetrahedral Cayley–Menger polynomial cm3 to the genuine $5\times 5$ Cayley–Menger determinant. The row/column layout places a border of ones around the $4\times 4$ block of squared edge lengths $a_0,\ldots,a_5$ for edges $(01),(02),(03),(12),(13),(23)$. Minors and cofactors of that matrix feed the dihedral-cosine formula.
The matrix in view is the concrete $4\times 4$ obtained by deleting row 2 and column 4 of the Cayley–Menger matrix of the regular unit tetrahedron (all squared edge lengths equal to 1) and retaining the resulting off-diagonal pattern. It is defined entrywise as the constant matrix displayed above; no symbolic edge lengths remain.
proof idea
Unfold the named matrix definition so the four rows are explicit. Expand the determinant along the zeroth row via Matrix.det_succ_row_zero. The resulting sum over the four cofactors collapses, after Fin.sum_univ_succ and the closed $3\times 3$ determinant formula Matrix.det_fin_three, to a pure arithmetic identity that evaluates to 1. The whole argument is a short tactic script with no external geometric lemmas.
why it matters
The immediate consumer is regularUnit_cofactor_24, which asserts that the $(2,4)$-cofactor of the regular-unit Cayley–Menger matrix equals 1. That cofactor identity is obtained by reducing the minor to the present matrix and invoking this determinant evaluation. Together they supply the numerical cofactor data needed for the regular tetrahedron’s dihedral cosine, closing the determinant/cofactor layer that the module advertises as prerequisite for the dihedral formula. Within Recognition Science geometry this is pure Euclidean bookkeeping; it does not invoke the forcing chain, $\varphi$, or the eight-tick octave, but it is required scaffolding for any later geometric rigidity or volume statements that specialise to the regular unit case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.