`alpha_gut_intermediate`

proved

show as: view math explainer →

module: IndisputableMonolith.QFT.RunningCouplings
domain: QFT
line: 141 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.RunningCouplings on GitHub at line 141.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 138theorem gut_24_from_8_times_3 : (24 : ℕ) = 8 * 3 := rfl
 139
 140/-- **THEOREM**: α_GUT is between the weak and strong couplings. -/
 141theorem alpha_gut_intermediate :
 142    alpha_s_Z > alpha_GUT ∧ alpha_GUT > alpha_em_low := by
 143  unfold alpha_GUT alpha_s_Z alpha_em_low
 144  constructor
 145  · norm_num
 146  · norm_num
 147
 148/-! ## QCD Scale -/
 149
 150/-- The QCD scale Λ_QCD in MeV. -/
 151noncomputable def lambda_QCD : ℝ := 200  -- MeV
 152
 153/-- **THEOREM**: Λ_QCD is of order 100-300 MeV. -/
 154theorem lambda_qcd_scale : 100 < lambda_QCD ∧ lambda_QCD < 300 := by
 155  unfold lambda_QCD
 156  constructor <;> norm_num
 157
 158/-! ## Dimensional Transmutation -/
 159
 160/-- Dimensional transmutation: a dimensionless coupling g generates
 161    a mass scale Λ through running. The proton mass m_p ~ Λ_QCD
 162    emerges from the gauge coupling through RG evolution. -/
 163def dimensionalTransmutationDescription : String :=
 164  "m_proton ~ Λ_QCD ~ M_Planck × exp(-const/α_s)"
 165
 166/-- The ratio of proton mass to QCD scale. -/
 167noncomputable def protonToQCDRatio : ℝ := 938 / lambda_QCD
 168
 169/-- **THEOREM**: Proton mass is ~ 5 × Λ_QCD. -/
 170theorem proton_qcd_ratio : 4 < protonToQCDRatio ∧ protonToQCDRatio < 6 := by
 171  unfold protonToQCDRatio lambda_QCD

papers checked against this theorem

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