pith. machine review for the scientific record. sign in
lemma proved tactic proof

gap_276_bounds

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 406lemma gap_276_bounds
 407    (h_low_phi : log_lower_bound_phi_hypothesis)
 408    (h_high_phi : log_upper_bound_phi_hypothesis)
 409    (h_low_276 : log_171p6_lower_hypothesis)
 410    (h_high_276 : log_171p6_upper_hypothesis) :
 411    (10.689 : ℝ) < gap 276 ∧ gap 276 < (10.691 : ℝ) := by

proof body

Tactic-mode proof.

 412  simp only [gap]
 413  have hphi := phi_bounds
 414  have hlogphi := log_phi_bounds h_low_phi h_high_phi
 415  have h_phi_pos : 0 < phi := phi_pos
 416  have h_log_pos : 0 < Real.log phi := Real.log_pos (by linarith [hphi.1])
 417  -- Bounds on 1 + 276/φ
 418  have h_arg_lower : 1 + 276 / (1.618034 : ℝ) < 1 + 276 / phi := by
 419    have hdiv : (276 : ℝ) / (1.618034 : ℝ) < 276 / phi := by
 420      have hpos : (0 : ℝ) < (276 : ℝ) := by norm_num
 421      exact div_lt_div_of_pos_left hpos h_phi_pos hphi.2
 422    linarith
 423  have h_arg_upper : 1 + 276 / phi < 1 + 276 / (1.618033 : ℝ) := by
 424    have hdiv : (276 : ℝ) / phi < 276 / (1.618033 : ℝ) := by
 425      have hpos : (0 : ℝ) < (276 : ℝ) := by norm_num
 426      exact div_lt_div_of_pos_left hpos (by norm_num : (0 : ℝ) < (1.618033 : ℝ)) hphi.1
 427    linarith
 428  -- Bounds on log(1 + 276/φ) using monotonicity
 429  have h_log_lower : Real.log (1 + 276 / (1.618034 : ℝ)) < Real.log (1 + 276 / phi) := by
 430    apply Real.log_lt_log (by norm_num) h_arg_lower
 431  have h_log_upper : Real.log (1 + 276 / phi) < Real.log (1 + 276 / (1.618033 : ℝ)) := by
 432    have h_pos : 0 < 1 + 276 / phi := by positivity
 433    apply Real.log_lt_log h_pos h_arg_upper
 434  -- Combine with numerical bounds
 435  have h_num_lower : (5.1442 : ℝ) < Real.log (1 + 276 / phi) :=
 436    lt_trans h_low_276 h_log_lower
 437  have h_num_upper : Real.log (1 + 276 / phi) < (5.1444 : ℝ) :=
 438    lt_trans h_log_upper h_high_276
 439  constructor
 440  · -- Lower bound: gap > 10.689
 441    have h_chain : 10.689 * Real.log phi < Real.log (1 + 276 / phi) := by
 442      have h1 : 10.689 * Real.log phi < 10.689 * 0.481213 := by nlinarith [hlogphi.2]
 443      have h2 : (10.689 : ℝ) * 0.481213 < 5.1442 := by norm_num
 444      linarith
 445    exact (lt_div_iff₀ h_log_pos).mpr h_chain
 446  · -- Upper bound: gap < 10.691
 447    have h_chain : Real.log (1 + 276 / phi) < 10.691 * Real.log phi := by
 448      have h1 : 10.691 * 0.481211 < 10.691 * Real.log phi := by nlinarith [hlogphi.1]
 449      have h2 : (5.1444 : ℝ) < 10.691 * 0.481211 := by norm_num
 450      linarith
 451    exact (div_lt_iff₀ h_log_pos).mpr h_chain
 452
 453end IntervalBounds
 454
 455end RSBridge
 456end IndisputableMonolith

depends on (15)

Lean names referenced from this declaration's body.