dihedralAngle3_regularUnit
plain-language theorem explainer
For every edge of the unit regular tetrahedron, the dihedral angle computed from Cayley–Menger cofactors equals the classical regular-tetrahedron dihedral angle (cosine 1/3). Anyone matching the cofactor pipeline to the existing DihedralAngle API cites this. The proof is a one-line application of the cofactor-check specialization once that check is discharged as a theorem.
Claim. For every edge $e$ of the unit regular tetrahedron, the dihedral angle obtained from the Cayley–Menger cofactor cosine equals the classical regular-tetrahedron dihedral angle $\theta$ with $\cos\theta=1/3$.
background
This module defines tetrahedral dihedral cosines from Cayley–Menger cofactors, replacing a prose reference in the older DihedralAngle API. For an edge $e=(i,j)$, if $(p,q)$ are the opposite vertices, the classical formula is $\cos\theta_e=C_{p,q}/\sqrt{C_{p,p}C_{q,q}}$ on the $5\times5$ Cayley–Menger cofactor matrix (vertex indices shifted by one). The sign convention yields $\cos\theta=1/3$ on the regular tetrahedron.
The unit regular tetrahedron is the non-degenerate tet with all squared edge lengths equal to one. The packaged classical value is the DihedralAngleData record with cosine $1/3$. The cofactor angle is $\arccos$ of the cofactor cosine. Upstream, the regular-unit cofactor check (that every edge’s cofactor cosine equals $1/3$) is already a theorem, not an assumption, and a conditional lemma converts that check into angle equality.
proof idea
One-line term wrapper. Apply the conditional lemma that, given any proof of the regular-unit cofactor check, the cofactor angle on the unit regular tet equals the classical regular dihedral angle, feeding the already-proved regular-unit cofactor check and the edge index $e$. No further rewriting is needed at this layer; the cosine identity and the $\arccos$ unfold live in the conditional lemma.
why it matters
Closes the gap between the cofactor-based dihedral definition and the pre-existing regular-tetrahedron dihedral API: the two agree on the unit regular tet with no external hypotheses. The module doc states the goal explicitly: replace prose by a Lean cofactor definition that recovers $\cos\theta=1/3$. Downstream use is not yet wired in this graph (used_by empty), but the declaration is the clean public equality consumers should cite when routing Regge or discrete-geometry arguments through Cayley–Menger rather than through the hand-packaged cosine. In the broader Recognition geometry stack it certifies that the cofactor pipeline is faithful on the regular cell that anchors curvature and deficit calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.