alpha_W

formal source

  45noncomputable def alpha_s_Z : ℝ := 0.118
  46
  47/-- The weak coupling (related to Fermi constant). -/
  48noncomputable def alpha_W : ℝ := 1/30
  49
  50/-! ## The Beta Function -/
  51
  52/-- The beta function describes how a coupling changes with scale:
  53    β(g) = μ dg/dμ. For QED β > 0; for QCD β < 0 (asymptotic freedom). -/
  54def betaFunction : String := "β(g) = μ dg/dμ"
  55
  56/-- The 1-loop beta function coefficient for SU(N) with Nf flavors:
  57    β₀ = (11N - 2Nf) / 3 -/
  58def beta0_SUN (N Nf : ℕ) : ℚ := (11 * N - 2 * Nf) / 3
  59
  60/-- **THEOREM**: QCD (SU(3)) with 6 flavors has β₀ = 7 > 0. -/
  61theorem qcd_beta0_positive : beta0_SUN 3 6 = 7 := by native_decide
  62
  63/-- **THEOREM**: QCD is asymptotically free (positive β₀ means coupling decreases at high energy). -/
  64theorem qcd_asymptotic_free : beta0_SUN 3 6 > 0 := by
  65  rw [qcd_beta0_positive]; norm_num
  66
  67/-- **THEOREM**: SU(2) with 6 flavors has β₀ = 10/3 > 0. -/
  68theorem su2_beta0 : beta0_SUN 2 6 = 10/3 := by native_decide
  69
  70/-! ## φ-Ladder Connection -/
  71
  72/-- Energy scale at φ-ladder rung n, in units of reference scale E₀. -/
  73noncomputable def phiLadderScale (n : ℤ) : ℝ := phi ^ n
  74
  75/-- φ is nonzero. -/
  76lemma phi_ne_zero' : phi ≠ 0 := ne_of_gt Constants.phi_pos
  77
  78/-- φ > 1. -/