betaQED1L
plain-language theorem explainer
The definition supplies the explicit one-loop beta function for the QED coupling scaled by an effective charge-weight factor. Physicists constructing the integrated mass residue f^exp from RG transport would cite this kernel when assembling the running of alpha. The body is a direct algebraic expression that multiplies alpha squared by the charge weight divided by three pi.
Claim. $β_{QED}(w,α)=(w/(3π))α²$, where $w$ is the effective charge-weight factor and $α$ is the fine-structure constant.
background
The module formalizes RG transport that defines the empirical mass residue f^exp. Fermion masses run with scale μ via d(ln m)/d(ln μ)=-γ_m(μ), and the integrated residue is f(μ0,μ1)=(1/λ)∫_{ln μ0}^{ln μ1} γ_m(μ') d(ln μ') with λ=ln φ. The structural mass at the anchor μ⋆ then relates to the physical mass by m_phys=m_struct·φ^{-f}.
proof idea
Direct definition returning the product of the supplied charge-weight factor divided by three times pi and the square of the fine-structure constant. No lemmas or tactics are invoked; the expression is the explicit one-loop kernel.
why it matters
This kernel supplies the one-loop QED running term inside the RG transport framework for mass residues. It supports the mass formula on the phi-ladder by providing the explicit contribution to the anomalous dimension through charge sums. The module doc states that exact higher-loop expressions are left to Level-B extensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.