residueDerivative
plain-language theorem explainer
The residue derivative definition supplies the derivative of the integrated residue with respect to the upper scale limit in renormalization group transport. It is cited by proofs establishing stationarity of the mass residue at the fixed scale. The definition is a direct algebraic reduction that invokes the fundamental theorem of calculus on the integral form of the residue.
Claim. For an anomalous dimension structure and fermion species, the residue derivative at logarithmic renormalization scale equals (1/λ) times the anomalous dimension evaluated at the exponential of that scale, where λ equals the natural logarithm of the golden ratio.
background
The RGTransport module formalizes renormalization group transport for mass residues. Fermion masses run with renormalization scale μ according to d(ln m)/d(ln μ) = -γ_m(μ), and the integrated residue from μ₀ to μ₁ is (1/λ) times the integral of γ_m over the logarithmic interval, with λ = ln φ. This connects the structural mass at the anchor scale to the physical mass via m_phys = m_struct · φ^{-f}.
proof idea
The definition is a one-line wrapper that applies the reciprocal of lambda to the gamma component of the AnomalousDimension structure evaluated at the exponential of the input logarithmic scale.
why it matters
This definition supports the stationarity_iff_gamma_zero theorem that equates a vanishing residue derivative to zero anomalous dimension at the stationary scale. It implements the RG transport framework linking the mass formula to the phi-ladder normalization, where lambda serves as the constant in the Recognition Science mass formula and eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.