integratedResidue
plain-language theorem explainer
integratedResidue encodes the cumulative mass anomalous dimension effect between two logarithmic renormalization scales as a scaled integral. Physicists deriving fermion mass ratios from the Recognition Science phi-ladder would cite it to link RG flow to the structural mass at the anchor scale. The definition is a direct one-line encoding of the integral formula supplied in the module documentation.
Claim. The integrated residue is defined by $f = (1/λ) ∫_{ln μ₀}^{ln μ₁} γ_f(e^t) dt$, where γ is an AnomalousDimension structure supplying the mass anomalous dimension function for fermion f, and λ = ln φ is the RS normalization constant.
background
The RGTransport module formalizes renormalization group transport of fermion masses in the Standard Model setting. Fermion masses obey d(ln m)/d(ln μ) = -γ_m(μ), where γ_m is the mass anomalous dimension. The AnomalousDimension structure packages a function gamma : Fermion → ℝ → ℝ together with smoothness and perturbative boundedness conditions. Lambda is the constant ln φ drawn from the RS-native units and the mass formula yardstick.
proof idea
This is a direct definition that applies the real integral operator over the closed interval Set.Icc lnμ₀ lnμ₁ to the gamma component of the supplied AnomalousDimension structure, then scales the result by 1/lambda. No auxiliary lemmas are required.
why it matters
The definition supplies the core object consumed by the anchor residue theorem f_residue and the mass ratio phi power theorem in AnchorPolicy and the same module. It implements the RG transport step that converts the structural mass at μ⋆ into the physical mass via φ^{-f}, closing the link between the phi-ladder mass formula and empirical residues. The module documentation flags the open task of inserting explicit QCD 4L/QED 2L kernels to obtain numerical values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.