dihedralCos3_regularUnit_of_cofactorCheck
plain-language theorem explainer
Under the regular-tetrahedron cofactor check, the Cayley-Menger cofactor cosine of the dihedral angle equals 1/3 on every edge of the unit regular tetrahedron. Anyone aligning the cofactor dihedral API with the classical regular-tet value cites this. The proof substitutes the three cofactor identities from the check and reduces the resulting radical by elementary arithmetic.
Claim. If the regular unit tetrahedron satisfies the cofactor identities $C_{p,q}=1$ and $C_{p,p}=C_{q,q}=-3$ for the opposite-vertex pair $(p,q)$ of every edge $e$, then the Cayley-Menger cofactor formula gives $\cos\theta_e=1/3$ on that tetrahedron.
background
This module defines tetrahedral dihedral cosines from Cayley-Menger cofactors, replacing a prose reference in the older dihedral-angle API. For an edge $e$, let $(p,q)$ be the two vertices opposite that edge (CM indices shifted by one from vertex labels). The classical formula is $\cos\theta_e=C_{p,q}/\sqrt{C_{p,p}C_{q,q}}$, with the sign convention that yields $\cos\theta=1/3$ on the regular tetrahedron.
The denominator is the product of diagonal cofactors under a square root; the numerator is the off-diagonal cofactor. The unit regular tetrahedron is the nondegenerate tet whose squared edge lengths are all one. The hypothesis RegularUnitCofactorCheck packages, for every edge, the three numerical cofactor values $C_{p,q}=1$, $C_{p,p}=-3$, $C_{q,q}=-3$ on those unit squared edges, isolating the expensive minor expansions so downstream proofs need not repeat them.
proof idea
Unfold the cofactor cosine, its squared-edge form, and the denominator. Simplify on the unit regular tet so the formula is written in cofactors of the unit squared-edge data. Case-split the check at the given edge to obtain the three equalities $C_{p,q}=1$, $C_{p,p}=-3$, $C_{q,q}=-3$. Rewrite those into the expression, leaving $1/\sqrt{(-3)(-3)}=1/\sqrt{9}$. Prove $\sqrt{9}=3$ via $\sqrt{3^2}=3$ for nonnegative $3$, then finish by numeric normalization to $1/3$.
why it matters
This is the conditional bridge from the cofactor formula to the classical regular-tet cosine. Downstream, dihedralAngle3_regularUnit_of_cofactorCheck rewrites the cofactor angle to the existing regular-tet dihedral API once this cosine identity is in hand, and dihedralCos3_regularUnit discharges the hypothesis via the proved cofactor check, giving an assumption-free $\cos\theta=1/3$.
In the broader geometry stack the result anchors Regge-style hinge data: regular tetrahedra are the reference cells whose dihedral deficit feeds discrete curvature. Matching the cofactor construction to the known $1/3$ value certifies that the CM-based angle agrees with the classical internal dihedral, so later curvature and zero-mode arguments can use either API interchangeably.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.