`alpha_em`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Experimental.MuonGMinusTwo on GitHub at line 20.

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

  17/-! ## I. Fine-Structure Constant -/
  18
  19/-- Fine-structure constant α ≈ 1/137.036 -/
  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]

papers checked against this theorem

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