dihedralCos3_regularUnit
plain-language theorem explainer
On every edge of the unit regular tetrahedron, the Cayley-Menger cofactor dihedral cosine equals 1/3. Regge-calculus and causal-simplex authors cite this as the classical regular-tet normalization, free of external assumptions. The proof is a one-line application of the cofactor-check specialization to the now-proved regular-unit cofactor identities.
Claim. For every edge $e\in\{0,\ldots,5\}$ of the unit regular tetrahedron, the Cayley-Menger cofactor dihedral cosine equals $1/3$.
background
This module defines tetrahedral dihedral cosines from cofactors of the $5\times 5$ Cayley-Menger matrix. For an edge $e=(i,j)$, if $(p,q)$ are the two opposite vertices (CM indices shifted by one), the classical formula is
$$\cos\theta_e = C_{p,q}/\sqrt{C_{p,p}C_{q,q}}.$$
The sign convention is chosen so the regular tetrahedron yields the standard internal value $\cos\theta=1/3$.
dihedralCos3 evaluates that formula on a nondegenerate tetrahedron. The unit regular tetrahedron is the nondegenerate tet whose six squared edge lengths are all $1$. The structure RegularUnitCofactorCheck packages the six explicit cofactor identities needed to reduce the formula to $1/3$; those identities are now a theorem (regularUnitCofactorCheck), not an assumption.
proof idea
One-line term wrapper. It applies dihedralCos3_regularUnit_of_cofactorCheck to the proved certificate regularUnitCofactorCheck and the given edge $e$. That upstream lemma unfolds the cofactor cosine and denominator, specializes to the unit regular squared edges, and discharges the three cofactor equalities (numerator and two diagonal entries) supplied by the check. No further arithmetic is done here.
why it matters
Closes the regular-tet normalization for the cofactor API: the classical value $\cos\theta=1/3$ is now an unconditional theorem rather than a hypothesis. Downstream, dihedralCos3Sq_alpha_one in the causal-simplex Wick module rewrites the physical-point Euclidean edges to the unit regular tet and quotes this result on every edge and both causal types. The four-tet signed-deficit development uses the same cofactor cosine as its hinge kernel (the rational certificate $(3-2p)/3$), so the regular point $p=1$ is consistent with this lemma. In the broader Recognition geometry stack this anchors Regge hinge angles in $D=3$ (forcing step T8) without external numeric input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.