Physics Running Couplings

Running couplings in RS

In particle physics, a coupling constant measures the strength of a force, and it is not actually constant. The strong force's coupling, written α_s, grows weaker at higher energies, a behavior called asymptotic freedom. The standard one-loop formula describes this running: α_s(μ) = α_s(anchor) / (1 + b₀/(2π) · α_s(anchor) · ln(μ/μ*)), where μ is the energy scale and b₀ depends on the number of quark flavors. The coefficient b₀ for QCD is 11 - 2n_f/3, and asymptotic freedom holds when this is positive, which occurs for 16 or fewer flavors.

Recognition Science (RS) builds its account of running couplings on a specific structure: the golden ratio φ = (1 + √5)/2, about 1.618. The framework's library of machine-checked theorems defines the ledger, a discrete record of recognition events, and derives a φ-ladder of energy scales. Within this framework, the β-function, which governs how the coupling changes with energy, is expressed as a derivative along this ladder: β(g) = (1/ln φ) dg/dr. The framework identifies a special anchor scale μ* = 182.201 GeV, a stationarity point where the flow pauses. From this anchor, the framework's running formula yields α_s(M_Z) ≈ 0.1185 at the Z boson mass, consistent with the measured world average of about 0.1181.

In Recognition Science, the QCD coefficient b₀ is not a free parameter but a derived quantity. The library proves b₀ = 11/(2π), which it shows equals the number of passive field edges in a cube, 3, divided by 2π. This connects the running of the strong force to the spatial structure forced by the framework's earlier theorems. The framework also handles quark mass running: the anomalous dimension is 8, and the mass evolution exponent for six flavors is 8/14. A key theorem proves that mass ratios are invariant under this running, meaning the ratio of two running masses equals the ratio of their reference values.

The framework's library proves the standard asymptotic freedom criterion: for n_f ≤ 16 flavors, b₀ is positive, and for 17 flavors it is not. It defines flavor thresholds at the charm, bottom, and top quark masses, where the number of active flavors steps up. It also defines a GUTUnification structure, a scale μ_GUT above the anchor where the couplings might unify, expressed as a φ-ladder rung. The framework's Weinberg angle squared is (3 - φ)/6, a value between 0 and 1. The central claim is that the running of couplings, including its sign and its special scales, follows from the same φ-ladder structure that forces the golden ratio and three spatial dimensions.

/-- **RS α_s(M_Z)**: Running from μ* = 182.201 GeV to M_Z = 91.2 GeV. -/
noncomputable def rs_alpha_s_MZ : ℝ :=
  alpha_s_running rs_alpha_s_anchor (b0_qcd 6) 91.2 rs_anchor_scale

/-- Asymptotic freedom holds for n_f ≤ 16 flavors. -/
theorem asymptotic_freedom_criterion (n_f : ℕ) (h : n_f ≤ 16) :
    0 < b0_qcd n_f := by
  unfold b0_qcd
  have : (n_f : ℝ) ≤ 16 := by exact_mod_cast h
  linarith

/-- b₀ comes from the passive-edge count: passive_field_edges(3) = 12 − 1 = 11. -/
theorem b0_from_passive_edges :
    b0_qcd_rs =
      (Constants.AlphaDerivation.passive_field_edges 3 : ℝ) / (2 * Real.pi) := by
  simp only [b0_qcd_rs, Constants.AlphaDerivation.passive_field_edges,
             Constants.AlphaDerivation.cube_edges,
             Constants.AlphaDerivation.active_edges_per_tick]
  norm_num

/-- **Mass ratios within a sector are RG-invariant at LO** when both masses
    are evolved from the same reference scale with the same α_s values. -/
theorem mass_ratio_rg_invariant (m1 m2 α_s_ref α_s_target : ℝ) (n_f : ℕ)
    (hr : (α_s_target / α_s_ref) ^ (mass_evolution_exp n_f) ≠ 0) :
    running_mass m1 α_s_ref α_s_target n_f / running_mass m2 α_s_ref α_s_target n_f =
    m1 / m2 := by
  unfold running_mass
  rw [mul_div_mul_right _ _ hr]

/-- **RS ANCHOR SCALE**: μ* = 182.201 GeV (stationarity point of RG). -/
def rs_anchor_scale : ℝ := 182.201  -- GeV

What this page does not claim

This answer does not claim the framework derives the fine-structure constant α. This answer does not claim the framework's α_s(M_Z) value is a theorem; it is a definitional model anchored at a chosen scale. This answer does not claim the framework proves the standard model's full renormalization group equations.

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/Physics/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: