alpha_gut_intermediate
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.