Encyclopedia Cost Cost Classical Results Neg Log Sin Tendsto At Top At Zero Right
ARTICLE 3 claims 3 theorems
Cost Classical Results Neg Log Sin Tendsto At Top At Zero Right
The logarithm of the sine function grows without bound as its input approaches zero from the right, a fact with a geometric meaning.
A limit at zero
The expression logarithm (the inverse of exponential growth) of the sine function has a simple behavior near zero. As the angle θ approaches 0 from the positive side, the value of sin θ also approaches 0, and the logarithm of a number near zero is a large negative number. Negating that logarithm produces a large positive number. The theorem neg_log_sin_tendsto_atTop_at_zero_right states this precisely: the function −log(sin θ) tends to infinity as θ tends to 0 from the right. This is not a statement about any particular value of θ, but about the trend as θ gets arbitrarily small.
This limit is a standard result in real analysis, the branch of mathematics dealing with limits, continuity, and differentiation. It follows from the continuity of the sine and logarithm functions, and it is used in the framework's library, a machine-checked collection of formal theorems, as a stepping stone. The library records it as a classical mathematical result, one that is well established in textbooks and does not itself encode a physical assumption. It is a tool for later arguments, not a claim about the physical world.
The theorem does not claim that the expression −log(sin θ) is defined at θ = 0. It is not; the sine of zero is zero, and the logarithm of zero is undefined. The statement concerns only the behavior of the function as the input approaches zero from the right, never reaching it. Nor does it assert anything about the limit from the left, where the sine function takes negative values and the logarithm is not defined for real numbers. The result is a one-sided limit, valid only for positive angles.
In the broader context of the framework, this limit appears in arguments about the geometry of a sphere. The expression −log(sin θ) is related to the area of a spherical cap, the portion of a sphere's surface cut off by a plane. As the cap shrinks to a point, its area tends to zero, and the logarithm of that area tends to negative infinity, so the negated logarithm tends to positive infinity. The theorem provides the formal justification for this geometric intuition.
What the declaration does not do is establish any new physics. It is a lemma about real numbers, not a statement about recognition, cost, or any other framework-specific concept. Its role is purely supportive: it supplies a known mathematical fact that later arguments can cite. The framework's own claims about the world rest on its forcing chain of theorems, not on this limit, which is a piece of standard analysis borrowed from the classical literature.
THEOREM neg_log_sin_tendsto_atTop_at_zero_right · IndisputableMonolith/Cost/ClassicalResults.lean
theorem neg_log_sin_tendsto_atTop_at_zero_right :
Filter.Tendsto (fun θ => - Real.log (Real.sin θ)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop := by
-- sin(θ) → 0⁺ as θ → 0⁺, so log(sin(θ)) → -∞, so -log(sin(θ)) → +∞
-- Use: f → -∞ implies -f → +∞
rw [← Filter.tendsto_neg_atBot_iff]
simp only [neg_neg]
-- Now need: log(sin θ) → -∞ as θ → 0⁺
-- sin θ → 0 as θ → 0 (from continuity)
have h_sin_tends_zero : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) := by
have h_cont : Continuous Real.sin := Real.continuous_sin
simpa [Real.sin_zero] using h_cont.tendsto 0 |>.mono_left nhdsWithin_le_nhds
-- sin θ > 0 near 0⁺ (eventually)
have h_sin_pos : ∀ᶠ θ in nhdsWithin 0 (Set.Ioi 0), 0 < Real.sin θ := by
have h_Iio_pi : Set.Iio Real.pi ∈ nhds (0 : ℝ) := Iio_mem_nhds Real.pi_pos
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds h_Iio_pi] with θ hθ_pos hθ_lt_pi
exact Real.sin_pos_of_pos_of_lt_pi hθ_pos hθ_lt_pi
-- Combine: sin θ → 0⁺ as θ → 0⁺
have h_sin_tends_zero_pos :
Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0)) := by
rw [tendsto_nhdsWithin_iff]
exact ⟨h_sin_tends_zero, h_sin_pos⟩
-- log x → -∞ as x → 0⁺
have h_log_atBot := Real.tendsto_log_nhdsGT_zero
-- Compose
exact h_log_atBot.comp h_sin_tends_zero_pos
THEOREM neg_log_sin_tendsto_atTop_at_zero_right · IndisputableMonolith/Cost/ClassicalResults.lean
theorem neg_log_sin_tendsto_atTop_at_zero_right :
Filter.Tendsto (fun θ => - Real.log (Real.sin θ)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop := by
-- sin(θ) → 0⁺ as θ → 0⁺, so log(sin(θ)) → -∞, so -log(sin(θ)) → +∞
-- Use: f → -∞ implies -f → +∞
rw [← Filter.tendsto_neg_atBot_iff]
simp only [neg_neg]
-- Now need: log(sin θ) → -∞ as θ → 0⁺
-- sin θ → 0 as θ → 0 (from continuity)
have h_sin_tends_zero : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) := by
have h_cont : Continuous Real.sin := Real.continuous_sin
simpa [Real.sin_zero] using h_cont.tendsto 0 |>.mono_left nhdsWithin_le_nhds
-- sin θ > 0 near 0⁺ (eventually)
have h_sin_pos : ∀ᶠ θ in nhdsWithin 0 (Set.Ioi 0), 0 < Real.sin θ := by
have h_Iio_pi : Set.Iio Real.pi ∈ nhds (0 : ℝ) := Iio_mem_nhds Real.pi_pos
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds h_Iio_pi] with θ hθ_pos hθ_lt_pi
exact Real.sin_pos_of_pos_of_lt_pi hθ_pos hθ_lt_pi
-- Combine: sin θ → 0⁺ as θ → 0⁺
have h_sin_tends_zero_pos :
Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0)) := by
rw [tendsto_nhdsWithin_iff]
exact ⟨h_sin_tends_zero, h_sin_pos⟩
-- log x → -∞ as x → 0⁺
have h_log_atBot := Real.tendsto_log_nhdsGT_zero
-- Compose
exact h_log_atBot.comp h_sin_tends_zero_pos
THEOREM neg_log_sin_tendsto_atTop_at_zero_right · IndisputableMonolith/Cost/ClassicalResults.lean
theorem neg_log_sin_tendsto_atTop_at_zero_right :
Filter.Tendsto (fun θ => - Real.log (Real.sin θ)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop := by
-- sin(θ) → 0⁺ as θ → 0⁺, so log(sin(θ)) → -∞, so -log(sin(θ)) → +∞
-- Use: f → -∞ implies -f → +∞
rw [← Filter.tendsto_neg_atBot_iff]
simp only [neg_neg]
-- Now need: log(sin θ) → -∞ as θ → 0⁺
-- sin θ → 0 as θ → 0 (from continuity)
have h_sin_tends_zero : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) := by
have h_cont : Continuous Real.sin := Real.continuous_sin
simpa [Real.sin_zero] using h_cont.tendsto 0 |>.mono_left nhdsWithin_le_nhds
-- sin θ > 0 near 0⁺ (eventually)
have h_sin_pos : ∀ᶠ θ in nhdsWithin 0 (Set.Ioi 0), 0 < Real.sin θ := by
have h_Iio_pi : Set.Iio Real.pi ∈ nhds (0 : ℝ) := Iio_mem_nhds Real.pi_pos
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds h_Iio_pi] with θ hθ_pos hθ_lt_pi
exact Real.sin_pos_of_pos_of_lt_pi hθ_pos hθ_lt_pi
-- Combine: sin θ → 0⁺ as θ → 0⁺
have h_sin_tends_zero_pos :
Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0)) := by
rw [tendsto_nhdsWithin_iff]
exact ⟨h_sin_tends_zero, h_sin_pos⟩
-- log x → -∞ as x → 0⁺
have h_log_atBot := Real.tendsto_log_nhdsGT_zero
-- Compose
exact h_log_atBot.comp h_sin_tends_zero_pos
What this page does not claim
The theorem asserts nothing about the value of the expression at θ = 0. The theorem makes no statement about the limit from the left side. The theorem is a mathematical lemma, not a physical claim about recognition or cost.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Cost/ClassicalResults.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- How does the limit of −log(sin θ) relate to the area of a spherical cap?
- In which later arguments within the framework does this limit appear?
- What other classical results are declared as axioms pending formalization?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM neg_log_sin_tendsto_atTop_at_zero_right · IndisputableMonolith/Cost/ClassicalResults.lean
theorem neg_log_sin_tendsto_atTop_at_zero_right : Filter.Tendsto (fun θ => - Real.log (Real.sin θ)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop := by -- sin(θ) → 0⁺ as θ → 0⁺, so log(sin(θ)) → -∞, so -log(sin(θ)) → +∞ -- Use: f → -∞ implies -f → +∞ rw [← Filter.tendsto_neg_atBot_iff] simp only [neg_neg] -- Now need: log(sin θ) → -∞ as θ → 0⁺ -- sin θ → 0 as θ → 0 (from continuity) have h_sin_tends_zero : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) := by have h_cont : Continuous Real.sin := Real.continuous_sin simpa [Real.sin_zero] using h_cont.tendsto 0 |>.mono_left nhdsWithin_le_nhds -- sin θ > 0 near 0⁺ (eventually) have h_sin_pos : ∀ᶠ θ in nhdsWithin 0 (Set.Ioi 0), 0 < Real.sin θ := by have h_Iio_pi : Set.Iio Real.pi ∈ nhds (0 : ℝ) := Iio_mem_nhds Real.pi_pos filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds h_Iio_pi] with θ hθ_pos hθ_lt_pi exact Real.sin_pos_of_pos_of_lt_pi hθ_pos hθ_lt_pi -- Combine: sin θ → 0⁺ as θ → 0⁺ have h_sin_tends_zero_pos : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0)) := by rw [tendsto_nhdsWithin_iff] exact ⟨h_sin_tends_zero, h_sin_pos⟩ -- log x → -∞ as x → 0⁺ have h_log_atBot := Real.tendsto_log_nhdsGT_zero -- Compose exact h_log_atBot.comp h_sin_tends_zero_posThe function −log(sin θ) tends to infinity as θ tends to 0 from the right. neg_log_sin_tendsto_atTop_at_zero_right · IndisputableMonolith/Cost/ClassicalResults.leanTHEOREM neg_log_sin_tendsto_atTop_at_zero_right · IndisputableMonolith/Cost/ClassicalResults.lean
theorem neg_log_sin_tendsto_atTop_at_zero_right : Filter.Tendsto (fun θ => - Real.log (Real.sin θ)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop := by -- sin(θ) → 0⁺ as θ → 0⁺, so log(sin(θ)) → -∞, so -log(sin(θ)) → +∞ -- Use: f → -∞ implies -f → +∞ rw [← Filter.tendsto_neg_atBot_iff] simp only [neg_neg] -- Now need: log(sin θ) → -∞ as θ → 0⁺ -- sin θ → 0 as θ → 0 (from continuity) have h_sin_tends_zero : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) := by have h_cont : Continuous Real.sin := Real.continuous_sin simpa [Real.sin_zero] using h_cont.tendsto 0 |>.mono_left nhdsWithin_le_nhds -- sin θ > 0 near 0⁺ (eventually) have h_sin_pos : ∀ᶠ θ in nhdsWithin 0 (Set.Ioi 0), 0 < Real.sin θ := by have h_Iio_pi : Set.Iio Real.pi ∈ nhds (0 : ℝ) := Iio_mem_nhds Real.pi_pos filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds h_Iio_pi] with θ hθ_pos hθ_lt_pi exact Real.sin_pos_of_pos_of_lt_pi hθ_pos hθ_lt_pi -- Combine: sin θ → 0⁺ as θ → 0⁺ have h_sin_tends_zero_pos : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0)) := by rw [tendsto_nhdsWithin_iff] exact ⟨h_sin_tends_zero, h_sin_pos⟩ -- log x → -∞ as x → 0⁺ have h_log_atBot := Real.tendsto_log_nhdsGT_zero -- Compose exact h_log_atBot.comp h_sin_tends_zero_posThe theorem does not claim that the expression −log(sin θ) is defined at θ = 0. neg_log_sin_tendsto_atTop_at_zero_right · IndisputableMonolith/Cost/ClassicalResults.leanTHEOREM neg_log_sin_tendsto_atTop_at_zero_right · IndisputableMonolith/Cost/ClassicalResults.lean
theorem neg_log_sin_tendsto_atTop_at_zero_right : Filter.Tendsto (fun θ => - Real.log (Real.sin θ)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop := by -- sin(θ) → 0⁺ as θ → 0⁺, so log(sin(θ)) → -∞, so -log(sin(θ)) → +∞ -- Use: f → -∞ implies -f → +∞ rw [← Filter.tendsto_neg_atBot_iff] simp only [neg_neg] -- Now need: log(sin θ) → -∞ as θ → 0⁺ -- sin θ → 0 as θ → 0 (from continuity) have h_sin_tends_zero : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) := by have h_cont : Continuous Real.sin := Real.continuous_sin simpa [Real.sin_zero] using h_cont.tendsto 0 |>.mono_left nhdsWithin_le_nhds -- sin θ > 0 near 0⁺ (eventually) have h_sin_pos : ∀ᶠ θ in nhdsWithin 0 (Set.Ioi 0), 0 < Real.sin θ := by have h_Iio_pi : Set.Iio Real.pi ∈ nhds (0 : ℝ) := Iio_mem_nhds Real.pi_pos filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds h_Iio_pi] with θ hθ_pos hθ_lt_pi exact Real.sin_pos_of_pos_of_lt_pi hθ_pos hθ_lt_pi -- Combine: sin θ → 0⁺ as θ → 0⁺ have h_sin_tends_zero_pos : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0)) := by rw [tendsto_nhdsWithin_iff] exact ⟨h_sin_tends_zero, h_sin_pos⟩ -- log x → -∞ as x → 0⁺ have h_log_atBot := Real.tendsto_log_nhdsGT_zero -- Compose exact h_log_atBot.comp h_sin_tends_zero_posThe result is a one-sided limit, valid only for positive angles. neg_log_sin_tendsto_atTop_at_zero_right · IndisputableMonolith/Cost/ClassicalResults.lean