alpha_em_pos

formal source

  20noncomputable def alpha_em : ℝ := 1 / 137.036
  21
  22/-- **THEOREM EA-001.1**: alpha_em is positive. -/
  23theorem alpha_em_pos : alpha_em > 0 := by
  24  unfold alpha_em
  25  norm_num
  26
  27/-- The Schwinger term: α/(2π). -/
  28noncomputable def schwinger_term : ℝ := alpha_em / (2 * Real.pi)
  29
  30/-- **THEOREM EA-001.2**: The Schwinger term is positive. -/
  31theorem schwinger_positive : schwinger_term > 0 := by
  32  unfold schwinger_term
  33  apply div_pos
  34  · exact alpha_em_pos
  35  · positivity
  36
  37/-! ## II. The RS Counter-Term -/
  38
  39/-- The muon rung on the φ-ladder. -/
  40noncomputable def muon_rung : ℝ := 13
  41
  42/-- The gap-1332 resonance factor. -/
  43noncomputable def gap_1332_factor : ℝ := 1 / (1332 * phi)
  44
  45/-- **THEOREM EA-001.3**: The gap-1332 factor is positive. -/
  46theorem gap_factor_pos : gap_1332_factor > 0 := by
  47  unfold gap_1332_factor
  48  apply div_pos
  49  · norm_num
  50  · nlinarith [phi_pos]
  51
  52/-- The RS counter-term for muon g-2. -/
  53noncomputable def rs_counter_term : ℝ :=