action_small_angle_diverges
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 in Recognition Science
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.
scope and limits
- Does not give the divergence rate or asymptotic expansion.
- Does not apply at θ = 0 or for θ outside (0, π/2].
- Does not incorporate embedding corrections from R3 geometry.
- Does not address integrability conditions used in adjacent path-integral results.
formal statement (Lean)
56theorem action_small_angle_diverges :
57 Tendsto (fun θ => A_of_theta θ) (nhdsWithin 0 (Set.Ioi 0)) atTop := by
proof body
Term-mode proof.
58 simpa [A_of_theta] using
59 IndisputableMonolith.Cost.ClassicalResults.neg_log_sin_tendsto_atTop_at_zero_right
60
61/-- Budget inequality implies the minimal angle threshold. -/