f_residue
plain-language theorem explainer
Existence of a residue function attaining any prescribed real value at a given fermion and renormalization scale is asserted, independent of the anomalous dimension. Single-anchor RG model builders cite it to interface external transport integrals with the geometric display. The proof is a term-mode construction that defines the function to return the target value at the exact point and zero elsewhere, then applies simp to confirm the equality.
Claim. For any anomalous dimension, fermion species, renormalization scale, and real number val, there exists a residue function such that the function returns val at the given fermion and scale.
background
The module supplies a Lean interface for single-anchor RG phenomenology, wiring the integrated residue of the mass anomalous dimension to the geometric display function at the anchor scale. The residue arises from the RG flow equation d ln m / d ln μ = -γ_m(μ) and is expressed as the integral (1 / ln φ) ∫ γ_i(μ') d(ln μ') from the anchor to the physical mass; external QCD 4L and QED 2L calculations supply the numerical content while the module isolates the existence claim.
proof idea
The proof is a term-mode construction. It introduces a function that returns the target value when the fermion and scale arguments match exactly and zero otherwise. The use tactic supplies this function as the existential witness; simp then reduces the equality via and_self and conditional simplification.
why it matters
This supplies the residue-function interface required by the display identity theorem (which equates the residue to the gap function of Z under the exact RS mapping hypothesis) and by the stationarity and stability theorems in the same module. It formalizes the empirical calibration step linking RG transport to the phi-ladder mass formula at the universal anchor; the open question it leaves is whether the integrated anomalous dimensions reproduce the geometric gap exactly for every fermion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.