electron_rg_val_hypothesis

formal source

  64/-! ## The Electron Case -/
  65
  66/-- For the electron, the perturbative residue is approx 0.0494. -/
  67def electron_rg_val_hypothesis : Prop :=
  68  -- Predicate for the specific electron value.
  69  True
  70
  71/-- The derived recognition strength for the electron. -/
  72def electron_strength (rg_val : ℝ) : ℝ := recognition_strength Fermion.e rg_val
  73
  74/-- Lower bound on the geometric residue for the electron (from the proven gap bounds). -/
  75theorem electron_geo_gt_13_953 : (13.953 : ℝ) < geometric_residue Fermion.e := by
  76  -- ZOf e = 1332, so this is exactly the lower bound on gap(1332).
  77  have hZ : ZOf Fermion.e = 1332 := by native_decide
  78  simpa [geometric_residue, hZ] using (gap_1332_bounds).1
  79
  80/-- A basic (non-universal) strength statement: if `rg_val = 0.04942583`,
  81then the ratio `F(Z)/f_RG` is certainly > 100 for the electron. -/
  82theorem electron_strength_gt_100 (rg_val : ℝ) (h_rg : rg_val = 0.04942583) :
  83    (100 : ℝ) < electron_strength rg_val := by
  84  unfold electron_strength recognition_strength
  85  -- rewrite rg residue value
  86  rw [h_rg]
  87  have hden_pos : (0 : ℝ) < (0.04942583 : ℝ) := by norm_num
  88  have hnum_gt : (13.953 : ℝ) < geometric_residue Fermion.e := electron_geo_gt_13_953
  89  -- It suffices to show 100 * 0.04942583 < 13.953.
  90  have h100 : (100 : ℝ) * (0.04942583 : ℝ) < (13.953 : ℝ) := by norm_num
  91  have hnum_gt' : (100 : ℝ) * (0.04942583 : ℝ) < geometric_residue Fermion.e :=
  92    lt_trans h100 hnum_gt
  93  -- divide by positive denominator
  94  exact (lt_div_iff₀ hden_pos).2 hnum_gt'
  95
  96/-! ## Structural Dominance -/
  97