det_regularUnitOffDiagMinorMatrix14
plain-language theorem explainer
The 4×4 off-diagonal minor matrix that appears when deleting row 1 and column 4 of the regular unit tetrahedron Cayley–Menger matrix has determinant −1. Anyone computing cofactors or dihedral cosines for the regular unit case cites this evaluation. The proof unfolds the explicit matrix, expands the first-row Laplace expansion, and reduces to a 3×3 determinant identity.
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&0\\1&1&1&1\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 border of ones and zeros standard for Cayley–Menger, and the six squared edge lengths $a_0..a_5$ filling the interior.
For the regular unit tetrahedron every squared edge length equals $1$. The minor obtained by deleting row $1$ and column $4$ is not quite the plain principal block; after the usual reindexing it becomes the concrete $4\times 4$ matrix regularUnitOffDiagMinorMatrix14 displayed above (first row $(0,1,1,1)$, then a nearly all-ones block with two strategically placed zeros).
That matrix is the sole upstream dependency of the present theorem. Downstream, its determinant feeds the cofactor identity needed for the dihedral-cosine formula at the regular unit point.
proof idea
Term-mode proof in three steps. Unfold the definition of the explicit $4\times 4$ matrix. Apply Matrix.det_succ_row_zero (Laplace expansion along the first row of a successor-indexed matrix). The resulting sum collapses by Fin.sum_univ_succ together with the closed $3\times 3$ determinant formula Matrix.det_fin_three and the reindexing map Fin.succAbove; simp finishes and yields $-1$.
why it matters
The result is the numerical engine inside regularUnit_cofactor_14, which asserts that the $(1,4)$-cofactor of the regular-unit Cayley–Menger matrix equals $+1$. That cofactor is the algebraic ingredient of the dihedral cosine extracted from the Cayley–Menger determinant; without the sign and magnitude fixed here the regular-unit specialization of the cosine formula would remain unevaluated.
In the broader Recognition geometry stack this sits in the pure Euclidean layer that later supports volume, angle, and rigidity statements. It does not itself invoke the forcing chain (T0–T8), the $J$-cost, or the $\varphi$-ladder; it is ordinary linear algebra serving those higher geometric claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.