runningCoupling
plain-language theorem explainer
The definition supplies the one-loop running coupling α(n) = α₀ / (1 + b n ln φ) on the φ-ladder. QFT researchers modeling discrete renormalization in Recognition Science cite it for scale dependence of couplings. The implementation is a direct algebraic expression with no lemmas or tactics.
Claim. The running coupling at integer rung $n$ is $α(n) = α_0 / (1 + b n ln φ)$, where $α_0$ is the reference coupling, $b$ the beta coefficient, and $φ$ the golden ratio.
background
The QFT module derives running couplings from φ-ladder scaling, where rungs label discrete energy scales and J-cost optimization produces scale dependence. The module contrasts this with standard RG flow α(E) = α(E₀) / (1 - b α₀ ln(E/E₀)). Upstream results include multiple rung definitions (Fermion sectors, OreClass, AnchorPolicy) that supply the integer index n, plus the continuous runningCoupling in UVCutoff that replaces the discrete log φ factor with a general energy ratio.
proof idea
This is a direct definition that unfolds to the algebraic formula α0 / (1 + b * n * log phi). No lemmas are applied.
why it matters
The definition is invoked by asymptotic_freedom_direction and running_at_zero in the same module, and by the UVCutoff counterpart. It supplies the discrete φ-ladder step required by QFT-011 for running couplings. It sits downstream of the phi forcing chain and supplies the scale variable used in later RG arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.