runningCoupling
plain-language theorem explainer
The runningCoupling definition encodes the standard one-loop renormalization group evolution of a coupling constant between two energy scales. Researchers studying asymptotic freedom or UV regularization in QFT would cite it to link the continuous running formula to Recognition Science's discrete phi-ladder. The implementation is a direct algebraic expression matching the integrated beta-function result.
Claim. The running coupling at energy scale $E$ is given by $α(E) = α_0 / (1 - b α_0 ln(E/E_0))$ for $E > 0$ and $E_0 > 0$, where $α_0$ is the reference value at scale $E_0$ and $b$ is the one-loop beta-function coefficient.
background
The QFT.UVCutoff module targets derivation of a natural ultraviolet cutoff from Recognition Science discreteness at the τ₀ scale, with the fundamental energy E0 defined as ħ/τ₀. Energy scales follow the phi-ladder E_n = E0 × φ^n, and running between adjacent rungs is universal. Upstream, SpectralEmergence.E counts edges of the D-cube as D × 2^(D-1), while RunningCouplings.runningCoupling supplies the discrete-rung form α(n) = α₀ / (1 + b n ln φ).
proof idea
This is a definition realized by direct transcription of the closed-form one-loop running formula. No lemmas are applied; the body is the algebraic expression α0 / (1 - b * α0 * Real.log (E / E0)) with the positivity hypotheses on E and E0 ensuring the logarithm is defined.
why it matters
This definition supplies the continuous-energy version used by asymptotic_freedom_direction and running_at_zero in RunningCouplings. It advances the QFT-013 target of natural UV regularization by connecting the running formula to the phi-ladder. In the Recognition framework it links the T6 phi fixed point and T7 eight-tick octave to QFT renormalization group flow, supporting universal running between phi-spaced scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.