gut_above_ew

formal source

 218  h_pos : 0 < μ_GUT
 219
 220/-- The GUT scale is above the electroweak scale. -/
 221theorem gut_above_ew (gut : GUTUnification) :
 222    rs_anchor_scale < gut.μ_GUT → 0 < gut.μ_GUT :=
 223  fun h => by unfold rs_anchor_scale at h; linarith
 224
 225/-! ## QCD Mass Running (Leading Order)
 226
 227The QCD mass anomalous dimension governs how quark masses change with
 228renormalization scale.  At one loop:
 229
 230    m(μ₂) = m(μ₁) × (α_s(μ₂)/α_s(μ₁))^(γ₀/(2b₀))
 231
 232where γ₀ = 8 is the universal one-loop anomalous dimension and b₀ depends
 233on the number of active flavors n_f.  Flavor thresholds (at m_c, m_b, m_t)
 234require matching the running across regions with different n_f.
 235
 236This infrastructure enables scheme-consistent quark residuals at a common
 237scale μ* = 182 GeV, removing the mixed-scheme artifacts that inflate
 238the sub-leading mass formula's eta parameter (Item 8). -/
 239
 240/-- One-loop QCD mass anomalous dimension: γ₀ = 8 (universal for all quarks). -/
 241def mass_anomalous_dim : ℝ := 8
 242
 243/-- Mass evolution exponent γ₀/(2b₀) for `n_f` active flavors. -/
 244noncomputable def mass_evolution_exp (n_f : ℕ) : ℝ :=
 245  mass_anomalous_dim / (2 * b0_qcd n_f)
 246
 247theorem mass_anomalous_dim_pos : 0 < mass_anomalous_dim := by
 248  unfold mass_anomalous_dim; norm_num
 249
 250theorem mass_evolution_exp_pos (n_f : ℕ) (h : n_f ≤ 16) :
 251    0 < mass_evolution_exp n_f := by