electron_pred_pos

formal source

  48/-- Predicted dimensionless ratio from the φ-ladder. -/
  49noncomputable def mu_pred : ℝ := proton_binding_pred / electron_pred
  50
  51private lemma electron_pred_pos : 0 < electron_pred := by
  52  have hb := electron_mass_bounds
  53  linarith [hb.1]
  54
  55private lemma proton_pred_pos : 0 < proton_binding_pred := by
  56  have hb := proton_mass_bounds
  57  linarith [hb.1]
  58
  59theorem mu_pred_pos : 0 < mu_pred :=
  60  div_pos proton_pred_pos electron_pred_pos
  61
  62/-! ## Predicted ratio bracket
  63
  64We prove `1898 < μ_pred < 1904`. The proof strategy: multiply through
  65by `electron_pred` (positive) to convert ratio bounds into
  66multiplicative bounds, then apply the two mass-bound theorems plus
  67arithmetic.
  68-/
  69
  70theorem mu_pred_lower : (1898 : ℝ) < mu_pred := by
  71  unfold mu_pred
  72  have he_pos : 0 < electron_pred := electron_pred_pos
  73  rw [lt_div_iff₀ he_pos]
  74  -- want: 1898 * electron_pred < proton_binding_pred
  75  have he_hi : electron_pred < (0.5102 : ℝ) := electron_mass_bounds.2
  76  have hp_lo : (969 : ℝ) < proton_binding_pred := proton_mass_bounds.1
  77  -- 1898 * electron_pred < 1898 * 0.5102 = 968.3596 < 969 < proton_binding_pred
  78  have step1 : (1898 : ℝ) * electron_pred < (1898 : ℝ) * (0.5102 : ℝ) := by
  79    have h1898 : (0 : ℝ) < 1898 := by norm_num
  80    exact mul_lt_mul_of_pos_left he_hi h1898
  81  have step2 : (1898 : ℝ) * (0.5102 : ℝ) < (969 : ℝ) := by norm_num