z_pred

formal source

  70
  71m_Z = rs_mass_MeV(.Electroweak, 1) = 2 × φ^51 / 10^6 -/
  72
  73noncomputable def z_pred : ℝ := rs_mass_MeV .Electroweak 1
  74
  75theorem z_pred_eq : z_pred = 2 * Constants.phi ^ (51 : ℕ) / 1000000 := by
  76  unfold z_pred rs_mass_MeV
  77  simp only [B_pow_Electroweak_eq, r0_Electroweak_eq]
  78  have hphi : Constants.phi ≠ 0 := ne_of_gt phi_pos
  79  have hphi_combine : Constants.phi ^ (-5 : ℤ) * Constants.phi ^ (55 : ℤ) * Constants.phi ^ (1 : ℤ) =
  80      Constants.phi ^ ((51 : ℕ) : ℤ) := by
  81    rw [← zpow_add₀ hphi, ← zpow_add₀ hphi]; norm_num
  82  conv_lhs =>
  83    rw [show (2 : ℝ) ^ (1 : ℤ) * Constants.phi ^ (-5 : ℤ) * Constants.phi ^ (55 : ℤ) * Constants.phi ^ (1 : ℤ)
  84      = (2 : ℝ) ^ (1 : ℤ) * (Constants.phi ^ (-5 : ℤ) * Constants.phi ^ (55 : ℤ) * Constants.phi ^ (1 : ℤ)) from by ring]
  85    rw [hphi_combine, zpow_natCast]
  86  simp only [zpow_one]
  87
  88private lemma phi51_gt : (45537548334 : ℝ) < Constants.phi ^ (51 : ℕ) := by
  89  rw [phi_eq_goldenRatio]; exact Numerics.phi_pow51_gt
  90private lemma phi51_lt : Constants.phi ^ (51 : ℕ) < (45537549354 : ℝ) := by
  91  rw [phi_eq_goldenRatio]; exact Numerics.phi_pow51_lt
  92
  93/-- The Z boson mass prediction lies in (91075.09, 91075.10) MeV. -/
  94theorem z_mass_bounds :
  95    (91075.09 : ℝ) < z_pred ∧ z_pred < (91075.10 : ℝ) := by
  96  rw [z_pred_eq]
  97  constructor
  98  · rw [lt_div_iff₀ (by norm_num : (0 : ℝ) < 1000000)]
  99    calc (91075.09 : ℝ) * 1000000 = (91075090000 : ℝ) := by norm_num
 100      _ < 2 * (45537548334 : ℝ) := by norm_num
 101      _ < 2 * Constants.phi ^ 51 := by nlinarith [phi51_gt]
 102  · rw [div_lt_iff₀ (by norm_num : (0 : ℝ) < 1000000)]
 103    calc 2 * Constants.phi ^ 51 < 2 * (45537549354 : ℝ) := by nlinarith [phi51_lt]