def
definition
alpha_GUT
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.QFT.RunningCouplings on GitHub at line 135.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
132/-! ## Gauge Coupling Unification -/
133
134/-- At GUT scale, couplings approximately meet at α ≈ 1/24. -/
135noncomputable def alpha_GUT : ℝ := 1/24
136
137/-- **THEOREM**: α_GUT = 1/(8 × 3) - unification of 8-tick and 3 dimensions. -/
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