`schwinger_positive`

proved

show as: view math explainer →

module: IndisputableMonolith.Experimental.MuonGMinusTwo
domain: Experimental
line: 31 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Experimental.MuonGMinusTwo on GitHub at line 31.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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 : ℝ :=
  54  (alpha_em / Real.pi) * (phi ^ (-muon_rung)) * gap_1332_factor
  55
  56/-- **THEOREM EA-001.4**: The RS counter-term is positive. -/
  57theorem rs_counter_positive : rs_counter_term > 0 := by
  58  unfold rs_counter_term
  59  have h0 : 0 < alpha_em / Real.pi := by
  60    unfold alpha_em
  61    apply div_pos

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.