running_at_zero
plain-language theorem explainer
The declaration establishes that the running coupling function returns the reference value α₀ when evaluated at rung zero. Researchers modeling renormalization group flows in the Recognition Science framework would cite this as the normalization condition for the φ-ladder scaling. The proof is a one-line wrapper that unfolds the definition of runningCoupling and applies simplification.
Claim. For any real numbers $α_0$ and $b$, the running coupling at rung $0$ satisfies $α(0) = α_0$, where $α(n) = α_0 / (1 + b · n · ln φ)$.
background
In the QFT.RunningCouplings module the running coupling is defined from φ-ladder scaling, with different rungs corresponding to discrete energy scales. The function implements the one-loop form α(n) = α₀ / (1 + b n log φ). Upstream results supply multiple definitions of rung: as a fixed natural number in Compat.Constants, as an OreClass index in AsteroidOreSpectroscopy, and as sector-dependent integers in AnchorPolicy and RSBridge.Anchor. The module document states that in Recognition Science running couplings reflect how J-cost optimization varies with φ-rung.
proof idea
The proof unfolds the definition of runningCoupling and applies simp to reduce the expression at n=0 to the identity α₀ = α₀.
why it matters
This theorem supplies the base case for the running coupling formula in the QFT.RunningCouplings module, which derives running from φ-scaling per the module target. It anchors the renormalization group boundary condition in the Recognition Science framework, consistent with T5 J-uniqueness and the phi forced fixed point. No downstream uses are recorded, yet the result supports later derivations of asymptotic freedom for positive b.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.