Encyclopedia Numerics Numerics Interval Log Log Interval Mono Contains Log
ARTICLE 3 claims 3 theorems
Numerics Interval Log Log Interval Mono Contains Log
A machine-checked theorem wraps the natural logarithm in a narrow interval, proving exactly where its value must lie.
Bounding the logarithm
The natural logarithm, written log(x), answers a simple question: to what power must the number e be raised to get x? For the golden ratio, that power is about 0.4812. The declaration logIntervalMono_contains_log is a formal proof that such a number can be pinned down rigorously, not just approximated. It states that if a positive input interval [lo, hi] is given, and if two rational bounds are known to sandwich log(lo) from below and log(hi) from above, then every x inside [lo, hi] has its logarithm inside the bound interval [lo_bound, hi_bound].
The proof rests on one classical fact: the logarithm is a monotonically increasing function on positive numbers. If x is between lo and hi, then log(x) must be between log(lo) and log(hi). The theorem turns that monotonicity into a machine-checked guarantee. It does not compute the logarithm directly. Instead it takes trusted bounds as inputs and returns a certified interval. The practical payoff appears in companion results: the library proves log(2) lies between 0.693 and 0.694, log(10) between 2.30 and 2.31, and log(φ) between 0.480 and 0.483.
In Recognition Science, this is not a physics claim but a numerical hygiene result. The framework's forcing chain produces the golden ratio as a constant, and later steps need reliable decimal bounds for its logarithm. The theorem supplies those bounds without appeal to unverified floating-point arithmetic. It is a piece of infrastructure, like a calibrated ruler, that keeps later calculations honest.
The declaration does not claim that the bounds are tight. It does not say that log(x) can be computed to arbitrary precision by this method alone. It does not assert anything about the golden ratio's role in physics. It only certifies that a specific interval, built from monotonicity and trusted endpoints, contains the true logarithm of every point in the input range.
THEOREM logIntervalMono_contains_log · IndisputableMonolith/Numerics/Interval/Log.lean
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 logIntervalMono_contains_log · IndisputableMonolith/Numerics/Interval/Log.lean
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_2_in_interval · log_10_in_interval · log_phi_in_interval · IndisputableMonolith/Numerics/Interval/Log.lean
/-- 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
/-- 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
/-- 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
What this page does not claim
The theorem does not claim the bounds are tight or optimal. It does not claim that log(x) can be computed to arbitrary precision by this method alone. It does not assert any physical role for the golden ratio's logarithm.
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:
- How does the framework compute the rational endpoints that sandwich log(lo) and log(hi)?
- What error bound does the Taylor series method guarantee for a given number of terms?
- Where in the forcing chain does the logarithm of the golden ratio first appear?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM logIntervalMono_contains_log · IndisputableMonolith/Numerics/Interval/Log.lean
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 linarithIf a positive input interval [lo, hi] is given, and if two rational bounds are known to sandwich log(lo) from below and log(hi) from above, then every x inside [lo, hi] has its logarithm inside the bound interval [lo_bound, hi_bound]. logIntervalMono_contains_log · IndisputableMonolith/Numerics/Interval/Log.leanTHEOREM logIntervalMono_contains_log · IndisputableMonolith/Numerics/Interval/Log.lean
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 linarithThe proof rests on one classical fact: the logarithm is a monotonically increasing function on positive numbers. logIntervalMono_contains_log · IndisputableMonolith/Numerics/Interval/Log.leanTHEOREM log_2_in_interval · log_10_in_interval · log_phi_in_interval · IndisputableMonolith/Numerics/Interval/Log.lean
/-- 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/-- 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/-- 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 h1The library proves log(2) lies between 0.693 and 0.694, log(10) between 2.30 and 2.31, and log(φ) between 0.480 and 0.483. log_2_in_interval · log_10_in_interval · log_phi_in_interval · IndisputableMonolith/Numerics/Interval/Log.lean