regular_tet_dihedral_theta
plain-language theorem explainer
The dihedral angle of a regular tetrahedron equals arccos(1/3). Researchers on Regge calculus and simplicial gravity cite this exact evaluation when linearizing curvature deficits at edges. The proof is a direct reflexivity reduction from the cosine definition of the regular tetrahedron.
Claim. Let θ denote the dihedral angle of a regular tetrahedron. Then θ = arccos(1/3).
background
This module defines dihedral angles at edges of simplices from Cayley-Menger data as Phase C2 toward discharging the Regge deficit linearization hypothesis on general simplicial complexes. DihedralAngleData carries a cosine value together with the bounds −1 ≤ cos ≤ 1; the angle is recovered as arccos of that cosine. The regular tetrahedron is supplied by the sibling definition regular_tet_dihedral, which hard-codes cosine exactly 1/3 with trivial norm_num bounds.
proof idea
The proof is a one-line wrapper that applies reflexivity to the theta projection of the regular_tet_dihedral definition.
why it matters
This supplies the concrete numerical angle required by the downstream theorem regular_tet_dihedral_in_open_interval. It completes the unconditional evaluation step in Phase C2 of the simplicial discharge program, feeding directly into Schläfli identities and the flat-sum condition used in Regge calculus. The result is classical geometry placed inside the Recognition framework's exact-constant pipeline for three-dimensional simplices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.