alpha_gut_intermediate
The theorem establishes the ordering alpha_s at the Z mass exceeds the GUT-scale value, which exceeds the low-energy electromagnetic coupling. Physicists modeling unification in Recognition Science cite this to confirm the expected hierarchy under phi-ladder scaling. The proof is a direct numerical check obtained by unfolding the three constant definitions and applying norm_num to each side of the conjunction.
claim$0.118 > 1/24 > 1/137.036$, or equivalently the strong coupling at the Z mass exceeds the GUT coupling which exceeds the low-energy electromagnetic fine-structure constant.
background
The module derives running couplings from phi-ladder scaling in Recognition Science, where distinct rungs correspond to energy scales and J-cost optimization varies with rung. Upstream definitions supply the concrete values: alpha_em_low equals 1/137.036, alpha_s_Z equals 0.118, and alpha_GUT equals 1/24. The scale function from LargeScaleStructureFromRS supplies the underlying phi^k construction that assigns these numerical values to different rungs.
proof idea
The term-mode proof unfolds the three constant definitions, splits the conjunction into two goals, and applies norm_num to each inequality. No additional lemmas are invoked beyond the definitions themselves.
why it matters in Recognition Science
The result anchors the unification picture at the GUT scale, where the 1/24 value encodes the eight-tick octave and three spatial dimensions. It supplies the intermediate ordering required for subsequent running-coupling derivations in the QFT module and aligns with the phi-ladder mechanism described in the module documentation.
scope and limits
- Does not derive the beta functions or explicit renormalization-group flow.
- Does not specify the precise energy at which unification occurs.
- Does not incorporate higher-loop corrections or threshold effects.
formal statement (Lean)
141theorem alpha_gut_intermediate :
142 alpha_s_Z > alpha_GUT ∧ alpha_GUT > alpha_em_low := by
proof body
Term-mode proof.
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. -/