theta_nonneg
plain-language theorem explainer
Dihedral angle data carries a cosine in [-1, 1] and recovers the angle via arccos. The result shows this angle is nonnegative. Workers on Regge calculus and simplicial geometry cite it when confirming angle ranges for tetrahedra. The proof is a one-line wrapper that invokes the standard nonnegativity of arccos.
Claim. Let $d$ be a dihedral angle datum whose cosine $c$ satisfies $-1 ≤ c ≤ 1$. Then the angle $θ = arccos(c)$ obeys $0 ≤ θ$.
background
The module defines dihedral angles for simplices from Cayley-Menger minors as Phase C2 toward discharging the Regge deficit linearization hypothesis on general simplicial complexes. DihedralAngleData is a structure that stores a real cosine together with explicit bounds proving it lies in [-1, 1]; the angle is recovered by applying arccos to this cosine value. The module also records the flat-space sum condition at non-singular edges and evaluates the regular-tetrahedron and cube cases unconditionally.
proof idea
The proof is a one-line wrapper that applies Real.arccos_nonneg directly to the cosine field of the input datum.
why it matters
The theorem is called inside dihedralAngleCert to assemble the full range statement used for cubic-lattice flat-sum and zero-deficit checks. It supplies the lower half of the [0, π] interval required by the geometry layer before Schläfli's identity and the final simplicial discharge. In the Recognition framework it closes the angle-range prerequisite for Regge-calculus linearization on three-dimensional simplicial complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.