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

gap_24_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)

 358lemma gap_24_bounds
 359    (h_low_phi : log_lower_bound_phi_hypothesis)
 360    (h_high_phi : log_upper_bound_phi_hypothesis)
 361    (h_low_24 : log_15p83_lower_hypothesis)
 362    (h_high_24 : log_15p83_upper_hypothesis) :
 363    (5.737 : ℝ) < gap 24 ∧ gap 24 < (5.74 : ℝ) := by

proof body

Tactic-mode proof.

 364  simp only [gap]
 365  have hphi := phi_bounds
 366  have hlogphi := log_phi_bounds h_low_phi h_high_phi
 367  have h_phi_pos : 0 < phi := phi_pos
 368  have h_log_pos : 0 < Real.log phi := Real.log_pos (by linarith [hphi.1])
 369  -- Bounds on 1 + 24/φ
 370  have h_arg_lower : 1 + 24 / (1.618034 : ℝ) < 1 + 24 / phi := by
 371    have hdiv : (24 : ℝ) / (1.618034 : ℝ) < 24 / phi := by
 372      have hpos : (0 : ℝ) < (24 : ℝ) := by norm_num
 373      exact div_lt_div_of_pos_left hpos h_phi_pos hphi.2
 374    linarith
 375  have h_arg_upper : 1 + 24 / phi < 1 + 24 / (1.618033 : ℝ) := by
 376    have hdiv : (24 : ℝ) / phi < 24 / (1.618033 : ℝ) := by
 377      have hpos : (0 : ℝ) < (24 : ℝ) := by norm_num
 378      exact div_lt_div_of_pos_left hpos (by norm_num : (0 : ℝ) < (1.618033 : ℝ)) hphi.1
 379    linarith
 380  -- Bounds on log(1 + 24/φ) using monotonicity
 381  have h_log_lower : Real.log (1 + 24 / (1.618034 : ℝ)) < Real.log (1 + 24 / phi) := by
 382    apply Real.log_lt_log (by norm_num) h_arg_lower
 383  have h_log_upper : Real.log (1 + 24 / phi) < Real.log (1 + 24 / (1.618033 : ℝ)) := by
 384    have h_pos : 0 < 1 + 24 / phi := by positivity
 385    apply Real.log_lt_log h_pos h_arg_upper
 386  -- Combine with numerical bounds
 387  have h_num_lower : (2.7613 : ℝ) < Real.log (1 + 24 / phi) :=
 388    lt_trans h_low_24 h_log_lower
 389  have h_num_upper : Real.log (1 + 24 / phi) < (2.7615 : ℝ) :=
 390    lt_trans h_log_upper h_high_24
 391  constructor
 392  · -- Lower bound: gap > 5.737
 393    have h_chain : 5.737 * Real.log phi < Real.log (1 + 24 / phi) := by
 394      have h1 : 5.737 * Real.log phi < 5.737 * 0.481213 := by nlinarith [hlogphi.2]
 395      have h2 : (5.737 : ℝ) * 0.481213 < 2.7613 := by norm_num
 396      linarith
 397    exact (lt_div_iff₀ h_log_pos).mpr h_chain
 398  · -- Upper bound: gap < 5.74
 399    have h_chain : Real.log (1 + 24 / phi) < 5.74 * Real.log phi := by
 400      have h1 : 5.74 * 0.481211 < 5.74 * Real.log phi := by nlinarith [hlogphi.1]
 401      have h2 : (2.7615 : ℝ) < 5.74 * 0.481211 := by norm_num
 402      linarith
 403    exact (div_lt_iff₀ h_log_pos).mpr h_chain
 404
 405/-- Bounds on gap(276). -/

depends on (14)

Lean names referenced from this declaration's body.