neg_log_sin_tendsto_atTop_at_zero_right
plain-language theorem explainer
The limit of -log(sin θ) as θ approaches 0 from above equals +∞. Researchers modeling small-angle kernels in Recognition Science cite it to establish divergence of the action functional A_of_theta. The tactic proof rewrites the negated limit, shows sin θ tends to 0⁺ via continuity and positivity, then composes with the standard log limit to -∞ as the argument tends to 0⁺.
Claim. $lim_{θ→0⁺} (-log(sin θ)) = +∞$
background
The module collects textbook results from real analysis for use in cost and measurement layers. These are treated as standard facts with references to Rudin and Apostol, not new physical assumptions. Upstream composition operations in CostAlgebra and Octave support the functional chaining that appears in the limit argument here.
proof idea
The tactic proof rewrites via tendsto_neg_atBot_iff to reduce to log(sin θ) tending to -∞. It establishes sin tending to 0 by continuity of Real.sin at 0, then proves eventual positivity in the right neighborhood using sin_pos_of_pos_of_lt_pi. The final step composes with Real.tendsto_log_nhdsGT_zero.
why it matters
The result is invoked directly by action_small_angle_diverges to prove divergence of the kernel action A_of_theta as θ→0⁺. It supplies the small-angle divergence needed for the minimal angle threshold in the RecognitionAngle module, consistent with the framework's handling of cost functions near the phi-ladder base. No open scaffolding questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.