phi43_lt

formal source

 284
 285private lemma phi43_gt : (969030000 : ℝ) < Constants.phi ^ (43 : ℕ) := by
 286  rw [phi_eq_goldenRatio]; exact Numerics.phi_pow43_gt
 287private lemma phi43_lt : Constants.phi ^ (43 : ℕ) < (970320000 : ℝ) := by
 288  rw [phi_eq_goldenRatio]; exact Numerics.phi_pow43_lt
 289
 290/-- The proton binding-energy prediction lies in (969, 970.4) MeV. -/
 291theorem proton_mass_bounds :
 292    (969 : ℝ) < proton_binding_pred ∧ proton_binding_pred < (970.4 : ℝ) := by
 293  unfold proton_binding_pred
 294  constructor
 295  · rw [lt_div_iff₀ (by norm_num : (0 : ℝ) < 1000000)]
 296    calc (969 : ℝ) * 1000000 < (969030000 : ℝ) := by norm_num
 297      _ < Constants.phi ^ 43 := phi43_gt
 298  · rw [div_lt_iff₀ (by norm_num : (0 : ℝ) < 1000000)]
 299    calc Constants.phi ^ 43 < (970320000 : ℝ) := phi43_lt
 300      _ < (970400000 : ℝ) := by norm_num
 301      _ = (970.4 : ℝ) * 1000000 := by norm_num
 302
 303/-- The proton prediction (binding-dominated) is within 3.5% of the PDG value.
 304
 305Note: the integer rung 48 is the closest to the proton mass. The ~3.3%
 306overshoot reflects the non-perturbative QCD binding that sits between
 307rungs 47 and 48 on the phi-ladder. -/
 308theorem proton_relative_error :
 309    |proton_binding_pred - m_p_exp| / m_p_exp < 0.035 := by
 310  have hb := proton_mass_bounds
 311  have hexp_pos : (0 : ℝ) < m_p_exp := by unfold m_p_exp; norm_num
 312  rw [div_lt_iff₀ hexp_pos, abs_lt]
 313  unfold m_p_exp
 314  constructor <;> nlinarith [hb.1, hb.2]
 315
 316/-! ## Verification Supersedes mass_ladder_assumption
 317