runningMass
plain-language theorem explainer
The running mass definition computes the fermion mass at a new renormalization scale from its reference value by exponentiating the negative integral of the anomalous dimension over the logarithmic interval. Researchers modeling scale dependence of masses in the Standard Model or Recognition Science phi-ladder constructions cite it when deriving residues between anchor and physical scales. The definition directly implements the integrated solution to the differential equation for mass running.
Claim. The mass of fermion $f$ at scale $μ$ is given by $m(μ) = m(μ_0) · exp(-∫_{ln μ_0}^{ln μ} γ(f, e^t) dt)$, where $γ$ is the anomalous dimension function.
background
The module formalizes renormalization group transport that defines the empirical mass residue in the Standard Model. The anomalous dimension structure supplies a function from each fermion species to a real-valued map of the scale $μ$, equipped with differentiability and a perturbative bound on its magnitude. This encodes the flow equation d(ln m)/d(ln μ) = -γ_m(μ) whose solution produces the integrated factor relating structural and physical masses on the phi-ladder.
proof idea
The definition is a direct one-line encoding of the exponential integral formula that solves the RG differential equation, multiplying the reference mass by exp of the negated integral of the gamma component over the closed interval.
why it matters
This definition supplies the transport operator invoked by the mass ratio theorem to relate masses at distinct scales. It supplies the mathematical framework for the residue that converts the structural mass at the anchor scale into the physical mass via the phi-ladder formula, as described in the module documentation. Explicit higher-order kernels for QCD and QED remain outside the present scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.