action_small_angle_diverges
plain-language theorem explainer
The theorem establishes that the kernel action A(θ) = −log(sin θ) diverges to +∞ as θ approaches 0 from above. Modelers of angular resolution limits and budget-constrained recognition thresholds cite it to derive positive lower bounds on admissible angles. The proof is a one-line term wrapper that substitutes the definition of A and invokes the classical limit for −log(sin θ).
Claim. $A(θ) := −log(sin θ)$ satisfies $lim_{θ→0^+} A(θ) = +∞$.
background
The Recognition Angle module introduces A_of_theta(θ) := −log(sin θ) on (0, π/2] as the kernel action that quantifies directional recognition cost. It also defines thetaMin(Amax) := arcsin(exp(−Amax)) as the budget-dependent minimal angle. The upstream theorem neg_log_sin_tendsto_atTop_at_zero_right from Cost.ClassicalResults states that −log(sin θ) tends to +∞ as θ → 0⁺, supplying the required real-analysis fact.
proof idea
The proof is a one-line term-mode wrapper. It applies simpa with the definition of A_of_theta to reduce the claim directly to the upstream limit theorem neg_log_sin_tendsto_atTop_at_zero_right.
why it matters
This result anchors the recognition-angle program by confirming unbounded cost for arbitrarily small angles, which justifies the thetaMin threshold and the infeasibility statements below it. It fits the cost-based measurement model in Recognition Science and supports finite-budget constraints on resolvable directions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.