Encyclopedia Numerics Numerics Interval Log Log 2 In Interval

ARTICLE 4 claims 4 theorems

Numerics Interval Log Log 2 In Interval

A machine-checked proof pins the natural logarithm of 2 between 0.693 and 0.694, a rigorous interval that ordinary floating-point arithmetic cannot guarantee.

Verify this page

A verified window for log 2

The natural logarithm of 2, written log 2, is the number you get when you ask what power of e gives 2. It appears throughout mathematics and physics: in information theory it is the conversion factor between bits and nats, in probability it shows up in entropy formulas, and in calculus it is the constant of integration for 1/x. Its decimal expansion begins 0.6931471805599453, but a decimal expansion, however long, is not a proof. The declaration log_2_in_interval in the framework's machine-checked library of formal theorems supplies that proof: it establishes, with the rigor of a computer-verified proof, that log 2 lies in the closed interval from 0.693 to 0.694.

The proof works by interval arithmetic, a method that computes with ranges of values instead of single numbers. The natural logarithm is monotonically increasing, so if an input x lies between two bounds, log x lies between the logarithms of those bounds. For the number 2 itself, the library uses a Taylor series expansion of log(1+x) with x = 1, together with a rigorous error bound that controls how much the truncated series can deviate from the true value. The result is an interval with rational endpoints, 693/1000 and 694/1000, and a proof that log 2 belongs to it. This is not an approximation with an unstated margin; it is a guarantee that the true value falls inside the stated range.

What the declaration does not claim is just as important. It does not claim that log 2 is exactly 0.6935, the midpoint of the interval; the theorem only asserts containment, not equality. It does not claim that the interval is the tightest possible, only that it is correct. And it does not claim anything about the framework's broader theory of cost functions or the golden ratio, even though the same file contains related bounds for log phi. The interval for log 2 stands on its own as a piece of verified numerical analysis, useful to anyone who needs a certified bound on this constant.

In Recognition Science, this kind of rigorous interval is part of a larger pattern: the framework's library builds exact, machine-checked results for the constants its theory uses. The same file proves log phi lies between 0.48 and 0.483, and log 10 lies between 2.30 and 2.31. These intervals are the framework's way of making sure that when a later theorem depends on a numerical value, that value is backed by proof rather than by convention or floating-point rounding. The log 2 interval is a small but concrete instance of that discipline: a number any calculus student meets, pinned down by a proof a machine has checked.

THEOREM log_2_in_interval · IndisputableMonolith/Numerics/Interval/Log.lean
log_2_in_interval · IndisputableMonolith/Numerics/Interval/Log.lean:338 
/-- log(2) is contained in log2Interval - PROVEN using Mathlib's log_two bounds -/
theorem log_2_in_interval : log2Interval.contains (log 2) := by
  simp only [contains, log2Interval]
  constructor
  · -- 0.693 ≤ log 2
    have h := Real.log_two_gt_d9  -- 0.6931471803 < log 2
    have h1 : ((693 / 1000 : ℚ) : ℝ) < log 2 := by
      calc ((693 / 1000 : ℚ) : ℝ) = (0.693 : ℝ) := by norm_num
        _ < (0.6931471803 : ℝ) := by norm_num
        _ < log 2 := h
    exact le_of_lt h1
  · -- log 2 ≤ 0.694
    have h := Real.log_two_lt_d9  -- log 2 < 0.6931471808
    have h1 : log 2 < ((694 / 1000 : ℚ) : ℝ) := by
      calc log 2 < (0.6931471808 : ℝ) := h
        _ < (0.694 : ℝ) := by norm_num
        _ = ((694 / 1000 : ℚ) : ℝ) := by norm_num
    exact le_of_lt h1
THEOREM logIntervalMono_contains_log · IndisputableMonolith/Numerics/Interval/Log.lean
logIntervalMono_contains_log · IndisputableMonolith/Numerics/Interval/Log.lean:46 
theorem logIntervalMono_contains_log {I : Interval} (hI_pos : 0 < I.lo)
    {lo_bound hi_bound : ℚ}
    (h_lo : (lo_bound : ℝ) ≤ log I.lo)
    (h_hi : log I.hi ≤ (hi_bound : ℝ))
    (h_valid : lo_bound ≤ hi_bound)
    {x : ℝ} (hx : I.contains x) :
    (logIntervalMono I hI_pos lo_bound hi_bound h_lo h_hi h_valid).contains (log x) := by
  simp only [contains, logIntervalMono]
  have hx_lo : (I.lo : ℝ) ≤ x := hx.1
  have hx_hi : x ≤ (I.hi : ℝ) := hx.2
  have hIlo_pos : (0 : ℝ) < I.lo := by exact_mod_cast hI_pos
  have hx_pos : 0 < x := lt_of_lt_of_le hIlo_pos hx_lo
  constructor
  · -- log x ≥ lo_bound
    have h1 : log (I.lo : ℝ) ≤ log x := Real.log_le_log hIlo_pos hx_lo
    linarith
  · -- log x ≤ hi_bound
    have h1 : log x ≤ log (I.hi : ℝ) := Real.log_le_log hx_pos hx_hi
    linarith
THEOREM log_taylor_error_bound · IndisputableMonolith/Numerics/Interval/Log.lean
log_taylor_error_bound · IndisputableMonolith/Numerics/Interval/Log.lean:105 
/-- Error bound for log Taylor polynomial on reals, using Complex.norm_log_sub_logTaylor_le -/
lemma log_taylor_error_bound {x : ℝ} (hx : |x| < 1) (n : ℕ) :
    |log (1 + x) - (Complex.logTaylor (n + 1) x).re| ≤ |x| ^ (n + 1) * (1 - |x|)⁻¹ / (n + 1) := by
  -- Use the complex version and specialize to reals
  have hx_complex : ‖(x : ℂ)‖ < 1 := by rw [complex_norm_ofReal]; exact hx
  have h := Complex.norm_log_sub_logTaylor_le n hx_complex
  -- log(1 + x) for real x equals Re(log(1 + x)) when 1 + x > 0
  have h1x_pos : (0 : ℝ) < 1 + x := by
    have : -1 < x := by
      have := abs_lt.mp hx
      linarith
    linarith
  have hlog_real : log (1 + x) = (Complex.log (1 + x)).re := by
    have h1 : (1 : ℂ) + (x : ℂ) = ((1 + x : ℝ) : ℂ) := by push_cast; ring
    rw [h1, Complex.log_ofReal_re]
  rw [hlog_real]
  have hsub_re : (Complex.log (1 + ↑x) - Complex.logTaylor (n + 1) ↑x).re =
      (Complex.log (1 + ↑x)).re - (Complex.logTaylor (n + 1) ↑x).re := by
    simp only [Complex.sub_re]
  rw [← hsub_re]
  calc |((Complex.log (1 + ↑x) - Complex.logTaylor (n + 1) ↑x).re : ℝ)|
      ≤ ‖Complex.log (1 + ↑x) - Complex.logTaylor (n + 1) ↑x‖ := Complex.abs_re_le_norm _
    _ ≤ ‖(x : ℂ)‖ ^ (n + 1) * (1 - ‖(x : ℂ)‖)⁻¹ / (n + 1) := h
    _ = |x| ^ (n + 1) * (1 - |x|)⁻¹ / (n + 1) := by simp only [complex_norm_ofReal]
THEOREM log_phi_in_interval · log_10_in_interval · IndisputableMonolith/Numerics/Interval/Log.lean
log_phi_in_interval · IndisputableMonolith/Numerics/Interval/Log.lean:311 
/-- log(φ) is contained in logPhiInterval - PROVEN using Taylor series bounds -/
theorem log_phi_in_interval : logPhiInterval.contains (log ((1 + Real.sqrt 5) / 2)) := by
  simp only [contains, logPhiInterval]
  have hphi_eq : (1 + Real.sqrt 5) / 2 = Real.goldenRatio := by
    unfold Real.goldenRatio
    ring
  rw [hphi_eq]
  constructor
  · -- 0.48 ≤ log φ
    have h := log_phi_gt_048
    have h1 : ((48 / 100 : ℚ) : ℝ) < log Real.goldenRatio := by
      calc ((48 / 100 : ℚ) : ℝ) = (0.48 : ℝ) := by norm_num
        _ < log Real.goldenRatio := h
    exact le_of_lt h1
  · -- log φ ≤ 0.483
    have h := log_phi_lt_0483
    have h1 : log Real.goldenRatio < ((483 / 1000 : ℚ) : ℝ) := by
      calc log Real.goldenRatio < (0.483 : ℝ) := h
        _ = ((483 / 1000 : ℚ) : ℝ) := by norm_num
    exact le_of_lt h1
log_10_in_interval · IndisputableMonolith/Numerics/Interval/Log.lean:363 
/-- log(10) is contained in log10Interval.
    Proof using log(10) = log(2) + log(5) and Mathlib bounds.
    log(2) ≈ 0.693, log(5) = log(10/2) requires log(10).
    Instead: log(10) = 2*log(√10), but √10 computation is circular.
    Best approach: log(10) = log(2) + log(5) where log(5) = log(4*5/4) = 2*log(2) + log(1.25)
    So log(10) = 3*log(2) + log(1.25) -/
theorem log_10_in_interval : log10Interval.contains (log 10) := by
  simp only [contains, log10Interval]
  -- log(10) = log(2 * 5) = log(2) + log(5)
  -- log(5) = log(4 * 1.25) = log(4) + log(1.25) = 2*log(2) + log(1.25)
  -- So log(10) = log(2) + 2*log(2) + log(1.25) = 3*log(2) + log(1.25)
  have h_log10_eq : log 10 = 3 * log 2 + log (5/4) := by
    have h1 : (10 : ℝ) = 8 * (5/4) := by norm_num
    have h2 : (8 : ℝ) = 2^(3 : ℕ) := by norm_num
    calc log 10 = log (8 * (5/4)) := by rw [h1]
      _ = log 8 + log (5/4) := Real.log_mul (by norm_num) (by norm_num)
      _ = log (2^(3 : ℕ)) + log (5/4) := by rw [h2]
      _ = (3 : ℕ) * log 2 + log (5/4) := by rw [Real.log_pow]
      _ = 3 * log 2 + log (5/4) := by norm_num
  -- Bounds on log(2) from Mathlib
  have h_log2_gt : log 2 > 0.6931471803 := Real.log_two_gt_d9
  have h_log2_lt : log 2 < 0.6931471808 := Real.log_two_lt_d9
  -- Bounds on log(5/4) = log(1.25) using Taylor series
  -- log(1 + x) for x = 0.25: 0.25 - 0.25²/2 + 0.25³/3 - ... ≈ 0.2231
  have h_log125_gt : log (5/4) > 0.223 := by
    -- log(1.25) > 0.223 ↔ exp(0.223) < 1.25
    rw [gt_iff_lt, Real.lt_log_iff_exp_lt (by norm_num : (0 : ℝ) < 5/4)]
    -- exp(0.223) < 1.25
    have hx_abs : |(0.223 : ℝ)| ≤ 1 := by norm_num
    have h_bound := Real.exp_bound hx_abs (n := 5) (by norm_num : 0 < 5)
    have h_upper := (abs_sub_le_iff.mp h_bound).1
    have h_taylor : (∑ m ∈ Finset.range 5, (0.223 : ℝ)^m / m.factorial) +
        |(0.223 : ℝ)|^5 * (6 : ℕ) / (Nat.factorial 5 * 5) < 1.25 := by
      simp only [Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial,
                 abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.223)]
      norm_num
    linarith
  have h_log125_lt : log (5/4) < 0.224 := by
    -- log(1.25) < 0.224 ↔ 1.25 < exp(0.224)
    rw [Real.log_lt_iff_lt_exp (by norm_num : (0 : ℝ) < 5/4)]
    -- exp(0.224) > 1.25
    have hx_abs : |(0.224 : ℝ)| ≤ 1 := by norm_num
    have h_bound := Real.exp_bound hx_abs (n := 4) (by norm_num : 0 < 4)
    have h_lower := (abs_sub_le_iff.mp h_bound).2
    have h_sum : (∑ m ∈ Finset.range 4, (0.224 : ℝ)^m / m.factorial) -
        |(0.224 : ℝ)|^4 * (5 : ℕ) / (Nat.factorial 4 * 4) > 1.25 := by
      simp only [Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial,
                 abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.224)]
      norm_num
    calc (5/4 : ℝ) = 1.25 := by norm_num
      _ < (∑ m ∈ Finset.range 4, (0.224 : ℝ)^m / m.factorial) -
          |(0.224 : ℝ)|^4 * (5 : ℕ) / (Nat.factorial 4 * 4) := h_sum
      _ ≤ Real.exp 0.224 := by linarith
  rw [h_log10_eq]
  constructor
  · -- 2.30 ≤ 3*log(2) + log(5/4)
    -- 3 * 0.6931471803 + 0.223 = 2.3024415409 > 2.30
    have h1 : (3 : ℝ) * 0.6931471803 + 0.223 > 2.30 := by norm_num
    have h2 : 3 * log 2 + log (5/4) > 3 * 0.6931471803 + 0.223 := by linarith
    linarith
  · -- 3*log(2) + log(5/4) ≤ 2.31
    -- 3 * 0.6931471808 + 0.224 = 2.3034415424 < 2.31
    have h1 : (3 : ℝ) * 0.6931471808 + 0.224 < 2.31 := by norm_num
    have h2 : 3 * log 2 + log (5/4) < 3 * 0.6931471808 + 0.224 := by linarith
    linarith

What this page does not claim

The theorem does not claim log 2 equals the midpoint 0.6935, only that it lies within the interval. The interval is not claimed to be the tightest possible bound for log 2. The declaration says nothing about the framework's cost function or golden ratio theory.

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/Numerics/Interval/Log.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND