theta_min_range
plain-language theorem explainer
The theorem states that for any budget Amax > 0 the threshold angle thetaMin(Amax) = arcsin(exp(-Amax)) is strictly positive and at most π/2. Researchers bounding the blind cone or minimal recognizable angle in the recognition-angle program cite it to guarantee a well-defined positive threshold. The proof is a one-line wrapper that unfolds the local definition of thetaMin and invokes the corresponding classical cost result.
Claim. For any real $A>0$, $0 < arcsin(e^{-A}) ∧ arcsin(e^{-A}) ≤ π/2$.
background
The module defines the action kernel A_of_theta(θ) := -log(sin θ) and the budget-dependent threshold thetaMin(Amax) := arcsin(exp(-Amax)). These objects formalize the minimal sensor angle admissible under a finite action budget Amax in the recognition-angle measurement setting. The local result restates a classical bound on the arcsin of an exponentially decaying argument, ensuring the threshold lies in (0, π/2].
proof idea
One-line wrapper that applies the classical theta_min_range theorem after simpa unfolding of the local thetaMin definition.
why it matters
The bound supplies the left and right conjuncts used by blind_cone_exists and theta_min_le_pi_half to establish a strictly positive blind cone capped at π/2. It closes the threshold properties required for the small-angle action divergence and cap-measure estimates in the recognition-angle program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.