det_regularUnitOffDiagMinorMatrix23
plain-language theorem explainer
The 4×4 off-diagonal minor matrix of the regular unit tetrahedron has determinant −1. Anyone computing Cayley–Menger cofactors for the regular unit edge set cites this evaluation. The proof unfolds the explicit matrix and reduces the 4×4 determinant via the first-row Laplace expansion and the closed 3×3 formula.
Claim. Let $M$ be the $4\times 4$ real matrix $$M=\begin{pmatrix}0&1&1&1\\1&0&1&1\\1&1&1&1\\1&1&1&0\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, supplying the determinant and cofactor layer used by the dihedral cosine formula. Rows and columns are indexed $0..4$ with the usual border of ones and squared edge lengths $a_0..a_5$ in the interior.
The matrix in view is the concrete $4\times 4$ minor that appears when the regular unit squared-edge configuration is specialized and the $(2,3)$ minor is extracted and rewritten in off-diagonal form. Its entries are only $0$ and $1$: a zero diagonal except for a single interior $1$, with ones elsewhere. Evaluating its determinant is a pure linear-algebra step before the cofactor sign is attached.
proof idea
Term-mode proof. Unfold the named matrix definition to the explicit $4\times 4$ array. Rewrite the determinant by the first-row Laplace expansion (Matrix.det_succ_row_zero). Finish with simp using the finite-sum recursion on Fin, the closed formula for $3\times 3$ determinants, and Fin.succAbove to resolve the deleted-column indices. No external geometric lemmas are required; the identity is pure matrix arithmetic.
why it matters
Feeds directly into regularUnit_cofactor_23, which concludes that the $(2,3)$ Cayley–Menger cofactor of the regular unit squared-edge list equals $+1$. That cofactor is the algebraic ingredient needed when the dihedral cosine is read off from ratios of Cayley–Menger minors for the regular tetrahedron.
In the broader Recognition geometry stack this sits inside the determinant/cofactor layer that turns the symbolic polynomial cm3 into concrete numerical cofactors. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is infrastructure for the tetrahedral geometry used downstream when edge lengths and angles are specialized to Recognition-native configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.