integratedResidue
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not supply explicit QCD or QED kernels for gamma.
- Does not evaluate the integral for concrete fermion species or scales.
- Does not address non-perturbative regimes outside the boundedness hypothesis.
- Does not derive or fix the value of lambda or phi.
Lean usage
def residueAtAnchor (γ : AnomalousDimension) (f : Fermion) (lnμ_ref : ℝ) : ℝ := integratedResidue γ f lnMuStar lnμ_refformal statement (Lean)
227def integratedResidue (γ : AnomalousDimension) (f : Fermion) (lnμ₀ lnμ₁ : ℝ) : ℝ :=
proof body
Definition body.
228 (1 / lambda) * ∫ t in Set.Icc lnμ₀ lnμ₁, γ.gamma f (Real.exp t)
229
230/-! ## Connection to Mass Formula -/
231
232/-- The running mass at scale μ, given the mass at scale μ₀ and an anomalous dimension.
233
234 `m(μ) = m(μ₀) · exp(-∫_{ln μ₀}^{ln μ} γ(μ') d(ln μ'))`
235
236 This is the solution to `d(ln m)/d(ln μ) = -γ_m(μ)`. -/