Encyclopedia Numerics Numerics Interval Log Log 10 In Interval

ARTICLE 2 claims 2 theorems

Numerics Interval Log Log 10 In Interval

The natural logarithm of 10 is an irrational number, but a machine-checked proof pins it between 2.30 and 2.31.

Verify this page

A certified bound for log 10

The natural logarithm of 10, written log 10, is the number you raise e to in order to get 10. It is about 2.302585, and it appears throughout science whenever a quantity spans several orders of magnitude: decibels, pH, earthquake magnitudes, and half-life calculations all use it. Because log 10 is irrational, no finite decimal expansion ever captures it exactly, so practical work relies on certified bounds: intervals that are guaranteed to contain the true value.

In the Recognition Science framework, the machine-checked library of formal theorems contains a declaration named log_10_in_interval. This theorem proves that log 10 lies in the closed interval from 2.30 to 2.31. The proof does not rely on a calculator's approximation. It builds the bound from first principles: the logarithm is monotonically increasing, so log 10 is bounded by evaluating log at nearby rational points, and the Taylor series for log(1+x) supplies a rigorous error estimate. The result is a formal guarantee, checked by a computer, that the true value cannot escape the stated interval.

The declaration is a ledger, a discrete record of events, of a very specific kind: it records a mathematical fact, not a physical measurement. It establishes a numerical containment, nothing more. It does not claim that log 10 is rational, does not give its exact value, and does not connect log 10 to any physical constant or to the golden ratio. The theorem is a piece of numerical infrastructure: a certified building block that other results in the library can rely on when they need a rigorous bound for log 10.

What the declaration does not claim is as precise as what it claims. It does not assert that 2.30 and 2.31 are the tightest possible bounds; a sharper interval may exist. It does not say anything about the decimal expansion beyond the containment. And it makes no claim about the Recognition Science framework's broader ambitions, such as deriving physical constants from first principles. The theorem is a narrow, exact statement: log 10 is between 2.30 and 2.31, and the proof is machine-checked.

THEOREM log_10_in_interval · IndisputableMonolith/Numerics/Interval/Log.lean
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
THEOREM logIntervalMono_contains_log · log_taylor_error_bound · 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
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]

What this page does not claim

The declaration does not claim that 2.30 and 2.31 are the tightest possible bounds for log 10. The declaration does not connect log 10 to any physical constant or to the golden ratio. The declaration does not provide the exact decimal expansion of log 10.

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