det_regularUnitOffDiagMinorMatrix12
plain-language theorem explainer
The 4×4 off-diagonal normal-form matrix for the regular unit tetrahedron's (1,2) Cayley-Menger minor has determinant exactly −1. Anyone computing the corresponding cofactor (and thence the dihedral cosine) cites this evaluation. The proof unfolds the matrix, expands the determinant along the first row, and reduces to an explicit 3×3 determinant.
Claim. Let $M$ be the $4\times 4$ real matrix $$M=\begin{pmatrix}0&1&1&1\\1&1&1&1\\1&1&0&1\\1&1&1&0\end{pmatrix}.$$ Then $\det M=-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 matrix. Rows and columns are indexed $0..4$ with the standard bordering by a zero and a row/column of ones; the six squared edge lengths occupy the off-diagonal $4\times 4$ block.
For the regular unit tetrahedron every squared edge equals $1$. The $(1,2)$-minor of that matrix is congruent (after deleting the bordering structure) to the concrete $4\times 4$ off-diagonal normal form displayed above. The present lemma simply evaluates its determinant.
Upstream, the matrix itself is introduced as an explicit constant; the cofactor pipeline later multiplies the determinant by the usual sign $(-1)^{i+j}$.
proof idea
Unfold the named matrix constant. Rewrite the $4\times 4$ determinant by Laplace expansion along row zero (Matrix.det_succ_row_zero). The resulting sum over the four cofactors collapses under Fin.sum_univ_succ and Fin.succAbove to a single nonzero term whose $3\times 3$ block is evaluated by Matrix.det_fin_three. The arithmetic yields $-1$.
why it matters
The identity is the sole numeric input to regularUnit_cofactor_12, which proves that the $(1,2)$-cofactor of the regular-unit Cayley-Menger matrix equals $+1$. That cofactor appears in the classical formula for the cosine of a dihedral angle of a tetrahedron. Inside Recognition Science the same regular-unit geometry supplies the reference edge lengths against which curvature and hinge defects are measured; a clean cofactor value therefore anchors the discrete-geometry side of the forcing chain that later forces $D=3$ and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.