theta_min_range
plain-language theorem explainer
For any positive Amax the quantity arcsin of exp of negative Amax lies strictly above zero and at most pi over two. Modelers of recognition angles in action budgets cite the bound to guarantee a positive threshold angle inside the first quadrant. The short proof reduces the two sides of the conjunction to the positivity of the exponential and the standard upper bound on arcsine.
Claim. For all $A>0$, $0 < arcsin(e^{-A}) land arcsin(e^{-A}) leq pi/2$.
background
This declaration lives in the ClassicalResults module, which assembles textbook facts from real analysis for use in the RecognitionAngle development. The module treats these facts as standard rather than derived from the core Recognition Science primitives such as the J-cost or the forcing chain. thetaMin is defined in the sibling ActionSmallAngle module by the expression arcsin of exp of negative Amax.
proof idea
The term proof introduces the positive Amax, splits the conjunction with constructor, rewrites the positivity side via the arcsin_pos lemma to the positivity of the exponential, and closes the upper bound with the arcsin_le_pi_div_two lemma.
why it matters
It is called by the theta_min_range theorem in ActionSmallAngle and thereby supports blind_cone_exists together with theta_min_le_pi_half in BlindCone. These steps secure the positive threshold angle required for cone existence and cap-measure bounds in the small-angle regime of the recognition model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.