spherical_cap_pos
plain-language theorem explainer
The lemma shows that 2π(1 - cos θ_min) is nonnegative for every θ_min in the closed interval from 0 to π/2. It is invoked by the spherical cap measure bounds theorem in the same module to establish a lower bound on a geometric measure. The short tactic proof chains the standard fact cos θ ≤ 1 with preservation of nonnegativity under multiplication by a positive constant.
Claim. $0 ≤ 2π(1 - cos θ_min)$ for all $θ_min ∈ [0, π/2]$.
background
The lemma lives inside the ClassicalResults module, which gathers textbook facts from real analysis for later use in cost calculations. The expression 2π(1 - cos θ) is the standard solid-angle measure of a spherical cap of angular radius θ on the unit sphere. The module document notes that such results are drawn from references such as Rudin’s Principles of Mathematical Analysis and Apostol’s Mathematical Analysis; they are treated as established rather than newly derived.
proof idea
The tactic proof applies Real.cos_le_one to obtain cos θ_min ≤ 1, then uses linarith to conclude 1 - cos θ_min ≥ 0. Positivity gives 2 * Real.pi ≥ 0, after which mul_nonneg combines the two nonnegative factors to finish the goal.
why it matters
The result supplies the nonnegativity step required by the spherical_cap_measure_bounds theorem, which itself appears in cost estimates inside the Cost domain. In the Recognition Science setting it supports geometric measure arguments that align with the three-dimensional spatial structure (D = 3) and the angular aspects of the forcing chain. No open scaffolding questions are closed by this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.