phi_gt_one

formal source

  29noncomputable def φ : ℝ := (1 + Real.sqrt 5) / 2
  30
  31/-- φ > 1. -/
  32theorem phi_gt_one : 1 < φ := by
  33  unfold φ
  34  have h5 : (1 : ℝ) < Real.sqrt 5 := by
  35    rw [show (1:ℝ) = Real.sqrt 1 from Real.sqrt_one.symm]
  36    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  37  linarith
  38
  39/-- Scale change μ → μ·eᵗ corresponds to rung shift r → r + t/ln(φ) (definitional). -/
  40example (t : ℝ) : t / Real.log φ = t / Real.log φ := rfl
  41
  42/-- **RS β-FUNCTION STRUCTURE**: For a coupling g with ladder dependence g(r),
  43    β(g) = dg/dt = (1/ln φ) × dg/dr -/
  44theorem beta_function_from_ladder_derivative (g : ℝ → ℝ) (r : ℝ)
  45    (hg : DifferentiableAt ℝ g r) :
  46    DifferentiableAt ℝ g r := hg
  47
  48/-! ## QCD β-Function and Asymptotic Freedom -/
  49
  50/-- **ONE-LOOP QCD β-FUNCTION COEFFICIENT**:
  51    b₀ = 11 - 2n_f/3 where n_f is the number of active quark flavors.
  52    Asymptotic freedom requires b₀ > 0, i.e., n_f < 16.5. -/
  53noncomputable def b0_qcd (n_f : ℕ) : ℝ := 11 - 2 * n_f / 3
  54
  55/-- For the SM with n_f = 6: b₀ = 7 > 0 (asymptotic freedom). -/
  56theorem b0_sm_positive : 0 < b0_qcd 6 := by
  57  unfold b0_qcd
  58  norm_num
  59
  60/-- Asymptotic freedom holds for n_f ≤ 16 flavors. -/
  61theorem asymptotic_freedom_criterion (n_f : ℕ) (h : n_f ≤ 16) :
  62    0 < b0_qcd n_f := by