Encyclopedia Numerics Numerics Interval Log

ARTICLE 4 claims 4 theorems

Numerics Interval Log

A machine-checked library pins down the natural logarithm of key constants to a few decimal places, with no floating-point guesswork.

Verify this page

Interval arithmetic for logarithms

The natural logarithm, written log(x), answers the question "what power of e gives x?" For the golden ratio φ ≈ 1.618, that value is about 0.4812. The ledger, a discrete record of recognition events, treats this number as a cost: the price of recognizing one object as another. The numerics interval log module computes such costs rigorously, not approximately.

Interval arithmetic replaces a single number with a range that is guaranteed to contain the true value. For log(φ), the module proves the interval [0.48, 0.483] contains the true value. This is not a decimal approximation that might drift; it is a theorem: the logarithm of the golden ratio lies between those two bounds. The proof uses the fact that log is increasing, so log(1.618) must lie between log(1.48) and log(1.483), then bounds those with Taylor series error estimates.

The same technique pins down other constants. The module proves log(2) lies in [0.693, 0.694] and log(10) lies in [2.30, 2.31]. Each interval comes from a machine-checked theorem, meaning a computer verified every step of the reasoning. The framework's library, a collection of formal theorems checked by a computer, contains these results as certified facts, not as calculator outputs.

In Recognition Science, this matters because the golden ratio appears throughout the framework: it is the unique self-similar scaling forced by the cost function. Knowing log(φ) to three decimal places, rigorously, gives the framework a concrete numerical anchor. The interval method also demonstrates a general principle: when a framework makes claims about real numbers, those claims can be verified to any desired precision, with the verification itself checked by machine.

THEOREM log_phi_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
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 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 · 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

What this page does not claim

This module does not derive the golden ratio or the cost function; it only computes a logarithm. The intervals are not proven optimal; they are proven correct.

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