regularUnit_vertex_diag_cofactor
plain-language theorem explainer
For the regular unit tetrahedron, every diagonal Cayley-Menger cofactor at a vertex index equals -3. Anyone deriving dihedral cosines from the 5×5 Cayley-Menger matrix cites this vertex-diagonal evaluation. The proof unfolds cofactor into sign times minor, notes the diagonal sign is +1, reduces the minor to a fixed normal-form matrix, and quotes its determinant -3.
Claim. Let $C_{r,c}$ be the Cayley-Menger cofactor of the regular unit tetrahedron (all six squared edge lengths equal to $1$). For every vertex index $p\in\{1,2,3,4\}$ (any row other than the border row $0$), the diagonal cofactor satisfies $C_{p,p}=-3$.
background
This module links the explicit tetrahedral Cayley-Menger polynomial cm3 to the genuine $5\times 5$ Cayley-Menger determinant and its cofactors, the layer required by the dihedral cosine formula. The matrix convention places a zero border entry at $(0,0)$, ones along the rest of the border, and the six squared edge lengths $a_0,\ldots,a_5$ in the lower-right $4\times 4$ block.
A cofactor $C_{r,c}$ is the signed minor obtained by deleting row $r$ and column $c$: the sign is $(-1)^{r+c}$ (realized as a real $\pm 1$), and the minor is the determinant of the resulting $4\times 4$ submatrix. On the diagonal $r=c=p$ the exponent $2p$ is always even, so the sign is $+1$.
The regular unit case specializes every squared edge length to $1$. Upstream, the diagonal vertex minor is identified with a fixed normal-form matrix whose determinant equals $-3$.
proof idea
Unfold the cofactor into sign times minor. For a diagonal entry the parity $p+p$ is even (witnessed by $p$ itself), so the sign simplifies to $+1$. Rewrite the minor via the normal-form identification for regular-unit diagonal minors (valid once $p\neq 0$), then apply the already-proved fact that the normal-form matrix has determinant $-3$. The product is therefore $-3$.
why it matters
The result supplies the four vertex-diagonal cofactor values needed by the regular-unit cofactor check in the dihedral Cayley-Menger module. That check is recorded downstream as a theorem rather than an assumption, closing a hypothesis interface for the cosine-of-dihedral-angle identities on the regular tetrahedron.
In the broader Recognition geometry stack this sits inside the determinant/cofactor layer that turns the abstract Cayley-Menger polynomial into concrete $3$-simplex data. The ambient setting is three-dimensional Euclidean geometry (the $D=3$ landmark of the forcing chain), where the regular tetrahedron is the model simplex whose edge and dihedral data feed later rigidity and volume arguments. It does not itself force dimension; it evaluates a fixed numerical cofactor once the regular unit edges are given.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.