`gap_factor_pos`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Experimental.MuonGMinusTwo on GitHub at line 46.

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

  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
  62    · norm_num
  63    · positivity
  64  have h1 : 0 < phi ^ (-muon_rung : ℝ) := by
  65    apply Real.rpow_pos_of_pos
  66    exact phi_pos
  67  have h2 : 0 < gap_1332_factor := gap_factor_pos
  68  have h3 : 0 < (alpha_em / Real.pi) * (phi ^ (-muon_rung : ℝ)) := mul_pos h0 h1
  69  exact mul_pos h3 h2
  70
  71/-! ## III. The RS Prediction -/
  72
  73/-- The SM reference point used here: Schwinger + hadronic seed. -/
  74noncomputable def sm_reference : ℝ := schwinger_term + 0.000711317
  75
  76/-- The RS prediction for muon g-2. -/

papers checked against this theorem

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