dihedral_from_cosine
plain-language theorem explainer
Defines the dihedral angle as the arccosine of the cosine field inside a DihedralAngleData structure. Discrete gravity researchers cite it when building hinge contributions to the Regge action on the RS lattice. The definition is a direct one-line wrapper around the real arccos function applied to the bounded cosine parameter.
Claim. For dihedral angle data $d$ with cosine field $c$ satisfying $-1 ≤ c ≤ 1$, the angle is $θ = arccos(c)$.
background
The module formalizes exact Regge calculus for the RS discrete gravity programme on a Z^3 × Z lattice with edge lengths from the J-cost defect field. Curvature concentrates on codimension-2 hinges, and the Regge action is the sum over hinges of area times deficit angle. DihedralAngleData is the structure holding the cosine of the angle between the two faces sharing a tetrahedron edge, with the explicit bound -1 ≤ cosine ∧ cosine ≤ 1.
proof idea
One-line definition that applies the real arccos function directly to the cosine field of the input DihedralAngleData structure.
why it matters
Supplies the basic dihedral angle extraction required to assemble the Regge action S_Regge = sum A_h * delta_h. It implements the exact DihedralAngle component listed in the module documentation and supports downstream results such as regge_action_nonneg_flat for flat configurations and deficit_from_dihedral.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.