Numerics Interval Log Log Phi In Interval

A certified bound on a famous logarithm

The golden ratio φ = (1 + √5)/2 ≈ 1.6180339887 is the number whose square is itself plus one. Its natural logarithm, written ln(φ) ≈ 0.481211825, appears across mathematics, from the spacing of sunflower seeds to the growth rate of the Fibonacci sequence. The declaration log_phi_in_interval in the Recognition Science library is a machine-checked theorem that certifies this value lies between 0.48 and 0.483. It proves the interval [0.48, 0.483] contains ln(φ), with the proof checked step by step by a computer.

The proof works by bounding the logarithm from both sides. Because the natural logarithm is an increasing function, the value at φ lies between the values at any numbers below and above it. The library uses the Taylor series for ln(1 + x) around x = 0, where x = φ - 1 ≈ 0.618, and bounds the error after ten terms. Simple rational bounds such as ln(x) ≥ 1 - 1/x for x > 0 also contribute. The result is a rigorous interval, not a numerical approximation with unstated error.

This is a statement about real numbers as defined in the library's formal system, not about floating-point arithmetic. The theorem does not claim that 0.48 < ln(φ) < 0.483 in the sense of a decimal expansion; it claims the real number lies in the closed interval. The proof uses rational arithmetic to establish bounds that hold exactly in the real numbers. The interval endpoints are rational numbers, 48/100 and 483/1000, and the theorem states the real logarithm lies between them.

In Recognition Science, this bound is a small piece of a larger structure. The framework derives constants such as the golden ratio from a cost function, and this interval provides a numerical anchor for that derivation. The theorem itself does not depend on any Recognition Science axioms; it is a plain result about the real logarithm. It stands on its own as a certified fact, independent of the framework's larger claims.

The practical consequence is that any computation relying on ln(φ) can use this interval as a verified starting point. A proof that needs a lower bound of 0.48 or an upper bound of 0.483 can cite this theorem and proceed without re-deriving the bound. The interval is narrow enough for many purposes, though wider than the true value by about 0.0018 on each side. For applications needing tighter bounds, the same method extends to more Taylor terms.

/-- 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

/-- 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]

/-- 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 exact decimal expansion of ln(φ) beyond the interval. It does not assert that 0.48 or 0.483 are the tightest possible rational bounds. It does not depend on any Recognition Science axioms; it is a plain result about the real 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: