theta_min_range
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute explicit numerical values of thetaMin for concrete Amax.
- Does not extend the bound to angles outside the Euclidean R3 setting.
- Does not link the threshold to the phi-ladder or forcing-chain constants.
- Does not address divergence of the action kernel itself.
Lean usage
have h := theta_min_range Amax hA; exact h.leftformal statement (Lean)
70theorem theta_min_range {Amax : ℝ} (hA : 0 < Amax) :
71 0 < thetaMin Amax ∧ thetaMin Amax ≤ π/2 := by
proof body
Term-mode proof.
72 simpa [thetaMin] using
73 IndisputableMonolith.Cost.ClassicalResults.theta_min_range Amax hA
74
75/-- If the angle is below the budget threshold, the action exceeds the budget. -/