log_phi_in_interval
The theorem confirms that the natural logarithm of the golden ratio lies inside the closed rational interval logPhiInterval. Numerics researchers verifying bounds on phi for Recognition Science calculations would cite it when composing interval proofs. The tactic proof equates the input to Real.goldenRatio, then splits the containment into independent lower and upper inequalities supplied by prior lemmas.
claim$log((1 + sqrt(5))/2)$ satisfies the containment predicate for the interval whose lower and upper rational endpoints are fixed by logPhiInterval, i.e., lower endpoint ≤ value ≤ upper endpoint.
background
The module supplies interval arithmetic for the natural logarithm on positive reals, using monotonicity of log together with Taylor remainder estimates for log(1+x) when 0 < x < 1. Here x = phi - 1 ≈ 0.618. The structure Interval is a closed interval with rational endpoints lo ≤ hi; the predicate contains asserts that a real lies between those endpoints. Upstream lemmas log_phi_gt_048 and log_phi_lt_0483 establish the strict inequalities 0.48 < log phi and log phi < 0.483 via exp monotonicity and separate phi bounds; the present theorem tightens them into a single interval statement.
proof idea
The tactic first rewrites ((1 + sqrt 5)/2) to Real.goldenRatio by ring. Constructor splits the conjunction inside contains. The lower half converts the rational 48/100 to real, invokes log_phi_gt_048, and closes with le_of_lt after norm_num. The upper half invokes log_phi_lt_0483, converts 483/1000, and closes with le_of_lt after norm_num.
why it matters in Recognition Science
The result supplies the verified containment fact that downstream tactic lemmas (log_phi_interval_contains, log_phi_gt_048, log_phi_lt_049) directly invoke. It supports numerical checks on phi, the self-similar fixed point forced at step T6 of the unified forcing chain. The module doc-comment notes that the bounds rest on Taylor error estimates for log(1+x) with x = phi - 1.
scope and limits
- Does not supply a closed-form expression for log phi.
- Does not extend the interval bounds to any constant other than phi.
- Does not treat complex logarithms or branch cuts.
- Does not claim the interval is the tightest possible rational enclosure.
Lean usage
theorem log_phi_interval_contains : logPhiInterval.contains (Real.log ((1 + Real.sqrt 5) / 2)) := log_phi_in_intervalformal statement (Lean)
312theorem log_phi_in_interval : logPhiInterval.contains (log ((1 + Real.sqrt 5) / 2)) := by
proof body
Tactic-mode proof.
313 simp only [contains, logPhiInterval]
314 have hphi_eq : (1 + Real.sqrt 5) / 2 = Real.goldenRatio := by
315 unfold Real.goldenRatio
316 ring
317 rw [hphi_eq]
318 constructor
319 · -- 0.48 ≤ log φ
320 have h := log_phi_gt_048
321 have h1 : ((48 / 100 : ℚ) : ℝ) < log Real.goldenRatio := by
322 calc ((48 / 100 : ℚ) : ℝ) = (0.48 : ℝ) := by norm_num
323 _ < log Real.goldenRatio := h
324 exact le_of_lt h1
325 · -- log φ ≤ 0.483
326 have h := log_phi_lt_0483
327 have h1 : log Real.goldenRatio < ((483 / 1000 : ℚ) : ℝ) := by
328 calc log Real.goldenRatio < (0.483 : ℝ) := h
329 _ = ((483 / 1000 : ℚ) : ℝ) := by norm_num
330 exact le_of_lt h1
331
332/-- Interval containing log(2) ≈ 0.693 -/