gammaMassQED1L
plain-language theorem explainer
This definition supplies the one-loop QED mass anomalous dimension as γ_m^QED(Q², α) = (3 Q² α)/(4π). A physicist assembling the full RG flow for Standard Model fermion masses would cite it to isolate the electromagnetic running piece. The implementation is a direct algebraic expression with no lemmas or reductions applied.
Claim. The one-loop QED contribution to the mass anomalous dimension is given by $γ_m^{QED}(Q^2, α) = (3 Q^2 α)/(4π)$, where $Q^2$ is the squared electric charge in elementary units and $α$ is the fine-structure constant.
background
Renormalization group transport encodes how fermion masses evolve with scale μ via d(ln m)/d(ln μ) = -γ_m(μ). The integrated residue is defined as f(μ₀, μ₁) = (1/λ) ∫ γ_m d(ln μ) with λ = ln φ; this residue converts between the structural mass at the anchor scale and the physical mass through m_phys = m_struct ⋅ φ^{-f}.
proof idea
The definition is a direct one-line algebraic expression implementing the standard perturbative one-loop QED result for the mass anomalous dimension.
why it matters
This definition populates the RG transport scaffolding that connects the Recognition Science mass formula to Standard Model running. It supplies the electromagnetic term required to evaluate the residue f that relates structural and observed masses on the phi-ladder. The module prepares the ground for inserting complete QCD and higher-order kernels while remaining consistent with the overall forcing chain and phi-based constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.