dihedralAngle3_regularUnit_of_cofactorCheck
plain-language theorem explainer
Under the regular-unit cofactor check, the Cayley-Menger cofactor dihedral angle on the unit regular tetrahedron equals the standard regular-tetrahedron dihedral (arccos of 1/3). Cite this when bridging the cofactor formula to the existing DihedralAngle API. The proof unfolds the angle wrappers and rewrites by the companion cosine identity.
Claim. If the regular-unit cofactor check holds (for every edge, the opposite-vertex cofactors of the unit regular Cayley-Menger matrix satisfy $C_{p,q}=1$ and $C_{p,p}=C_{q,q}=-3$), then for every edge $e\in\{0,\ldots,5\}$ the cofactor dihedral angle of the unit regular tetrahedron equals $\arccos(1/3)$.
background
This module defines tetrahedral dihedral cosines from Cayley-Menger cofactors, replacing a prose reference in the DihedralAngle layer. For an edge $e=(i,j)$, let $(p,q)$ be the two opposite vertices. Vertex rows in the $5\times 5$ Cayley-Menger matrix are shifted by one, and 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 $\cos\theta=1/3$.
The hypothesis RegularUnitCofactorCheck packages the three cofactor evaluations needed for that reduction: opposite-pair cofactor $1$ and diagonal cofactors $-3$ on every edge. The existing API object regular_tet_dihedral is the DihedralAngleData record with cosine $1/3$ and the corresponding arccos angle. The companion lemma already shows the cofactor cosine equals $1/3$ under the same check.
proof idea
Short tactic proof. Unfold the cofactor angle definition, the theta projection of DihedralAngleData, and the regular-tetrahedron API record, so both sides become arccos of a cosine. Rewrite the cosine by the sibling lemma dihedralCos3_regularUnit_of_cofactorCheck applied to the same cofactor-check hypothesis and edge. Equality of the angles follows immediately.
why it matters
Closes the angle-level half of the cofactor bridge: once the cosine identity is in hand, the arccos wrappers match the pre-existing regular-tetrahedron dihedral API. The sole downstream consumer is dihedralAngle3_regularUnit, which discharges the cofactor-check hypothesis via the proved certificate regularUnitCofactorCheck and states the equality with no external assumptions. That unconditional form is what geometry and Regge-calculus consumers should cite. In the broader Recognition stack this anchors discrete 3-geometry (T8 forces $D=3$) to a fully expanded Cayley-Menger definition rather than a prose constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.