blind_cone_exists
plain-language theorem explainer
The theorem shows that θmin(Amax) exceeds zero for every positive action budget Amax. Measurement theorists working on recognition cones cite the result to guarantee a non-empty blind region under any finite budget. The argument is a direct extraction of the positivity conjunct from the range theorem for the threshold angle.
Claim. For every real $A>0$, the threshold angle satisfies $0<θ_ min(A)$.
background
The module defines the blind-cone set at a point x for a given action budget Amax as the collection of directions whose required action stays inside Amax. The threshold angle θmin(Amax) is the angular radius of this cone. Upstream, ActionSmallAngle.theta_min_range states that θmin(Amax) is strictly positive and at most π/2 for any Amax>0, obtained by rewriting the classical arcsin positivity result from Cost.ClassicalResults.
proof idea
The proof is a one-line wrapper that applies theta_min_range (Amax := Amax) hA and extracts the left conjunct via exact h.left.
why it matters
The result supplies the minimal existence property required for any blind-cone construction in the measurement layer. It feeds the cap-measure bounds that appear later in the RecognitionAngle development and aligns with the measurement step after the forcing chain (T0-T8). No open scaffolding remains for this specific claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.