betaFunction
plain-language theorem explainer
betaFunction supplies the string representation of the renormalization group beta function β(g) = μ dg/dμ. Researchers deriving scale dependence of couplings from φ-ladder transitions in Recognition Science cite it when connecting J-cost optimization across rungs to the observed increase of α_em and decrease of α_s. The implementation is a direct string literal with no computation or lemmas.
Claim. The renormalization group beta function is given by $β(g) = μ dg/dμ$.
background
The QFT module derives running couplings from φ-ladder scaling, where each rung corresponds to a distinct energy scale and J-cost optimization changes with rung number. This produces the observed behavior: α_em increases with energy while α_s decreases (asymptotic freedom). The module imports PhiForcing to supply the self-similar fixed point and forcing chain that set the rung spacing.
proof idea
Direct definition as a string literal assignment; no lemmas or tactics are applied.
why it matters
This definition anchors the QFT-011 target of obtaining running couplings from φ-ladder scaling. It supplies the mathematical object whose scale dependence is later tied to J-cost changes and the Recognition Composition Law. Sibling declarations such as beta0_SUN and qcd_asymptotic_free build on the same RG framework but remain unlinked in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.