Qft Running Couplings

Running couplings and the phi ladder

In quantum field theory, a coupling constant measures the strength of an interaction, and it is not actually constant. The fine-structure constant α, which governs electromagnetism, is about 1/137 at low energies but grows to about 1/127.9 at the mass of the Z boson, roughly 91 GeV. The strong coupling α_s behaves oppositely: it is large at low energies, around 0.118 at the Z mass, and shrinks at higher energies, a property called asymptotic freedom. The weak coupling α_W is about 1/30. This energy dependence is described by the renormalization group, whose central object is the beta function, written β(g) = μ dg/dμ, which tells how a coupling g changes as the energy scale μ changes.

The standard model's one-loop beta function for a non-abelian gauge group SU(N) with N_f fermion flavors is β₀ = (11N - 2N_f)/3. For quantum chromodynamics, with N=3 colors and N_f=6 quarks, this gives β₀ = 7, a positive number that proves asymptotic freedom: the coupling decreases at high energy. For the electroweak SU(2) with N_f=6, β₀ = 10/3. These are textbook results, and the framework's machine-checked library of formal theorems reproduces them as proved statements, along with the observation that the strong coupling at the Z mass, α_s(Z) = 0.118, lies between the low-energy electromagnetic value 1/137.036 and the grand unified theory value 1/24.

In Recognition Science, the framework models each energy scale as a rung on a ladder built from the golden ratio φ ≈ 1.618. The scale at rung n is φ^n, so rung 0 is 1, rung 1 is φ, and rung 2 is φ². The framework proves that higher rungs give larger scales, and it defines a running coupling formula α(α₀, b, n) = α₀ / (1 + b·n·log φ), where α₀ is the coupling at rung 0 and b is a beta-function-like coefficient. The framework proves this formula decreases when b is positive and n is positive, matching the direction of asymptotic freedom. The GUT value 1/24 is identified with 1/(8×3), a factorization the framework derives from its eight-tick cycle and three spatial dimensions.

The framework also fixes the QCD scale Λ_QCD at 200 MeV, proves it lies between 100 and 300 MeV, and derives that the proton mass to Λ_QCD ratio is between 4 and 6, close to the measured value of about 4.7. It records the dimensional transmutation relation m_proton ~ Λ_QCD ~ M_Planck × exp(-const/α_s) and notes that the QED Landau pole, where the electromagnetic coupling would become infinite, sits at roughly 10^286 GeV, a scale the framework says is cut off by Planck-scale discreteness. The practical consequence: the framework's ladder of scales reproduces the standard running-coupling picture and adds a structural reason, the golden ratio, for why the scales are what they are.

/-- **THEOREM**: QCD is asymptotically free (positive β₀ means coupling decreases at high energy). -/
theorem qcd_asymptotic_free : beta0_SUN 3 6 > 0 := by
  rw [qcd_beta0_positive]; norm_num

/-- **THEOREM**: φ-ladder gives exponential hierarchy (φ^n > 1 for n > 0). -/
theorem phi_ladder_hierarchy (n : ℕ) (hn : n > 0) :
    phiLadderScale n > 1 := by
  unfold phiLadderScale
  rw [zpow_natCast]
  exact one_lt_pow₀ phi_gt_one' (Nat.pos_iff_ne_zero.mp hn)

/-- **THEOREM**: For positive b, coupling decreases with rung (asymptotic freedom). -/
theorem asymptotic_freedom_direction (alpha0 b : ℝ) (n : ℤ)
    (ha : alpha0 > 0) (hb : b > 0) (hn : n > 0) :
    runningCoupling alpha0 b n < alpha0 := by
  unfold runningCoupling
  have hlog : log phi > 0 := Real.log_pos (by linarith [phi_gt_onePointFive])
  have hbn_pos : b * n * log phi > 0 := by
    apply mul_pos
    apply mul_pos hb
    exact Int.cast_pos.mpr hn
    exact hlog
  have hdenom_gt_one : 1 + b * n * log phi > 1 := by linarith
  -- α / d < α when d > 1 and α > 0
  have h : alpha0 / (1 + b * ↑n * log phi) < alpha0 / 1 := by
    apply div_lt_div_of_pos_left ha (by linarith) hdenom_gt_one
  simp at h
  exact h

/-- **THEOREM**: Λ_QCD is of order 100-300 MeV. -/
theorem lambda_qcd_scale : 100 < lambda_QCD ∧ lambda_QCD < 300 := by
  unfold lambda_QCD
  constructor <;> norm_num

/-- **THEOREM**: Proton mass is ~ 5 × Λ_QCD. -/
theorem proton_qcd_ratio : 4 < protonToQCDRatio ∧ protonToQCDRatio < 6 := by
  unfold protonToQCDRatio lambda_QCD
  constructor <;> norm_num

What this page does not claim

This module does not derive the numerical values of the standard model couplings from first principles. The framework's running coupling formula is a model, not a derivation of the full renormalization group equations. The identification of the GUT scale with 1/(8×3) is a structural observation, not a proof of grand unification.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/QFT/RunningCouplings.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: