theta_nonneg
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the upper bound θ ≤ π.
- Does not compute explicit numerical values for any polyhedron.
- Does not treat dihedral angles outside three-dimensional Euclidean space.
- Does not incorporate curvature or Regge deficit data.
formal statement (Lean)
65theorem theta_nonneg (d : DihedralAngleData) : 0 ≤ d.theta :=
proof body
One-line wrapper that applies Real.arccos_nonneg.
66 Real.arccos_nonneg d.cosine
67