residueAtAnchor
plain-language theorem explainer
residueAtAnchor computes the integrated mass anomalous dimension residue for fermion f from the fixed anchor scale lnMuStar to a supplied reference lnμ_ref. Researchers deriving physical masses from the phi-ladder in Recognition Science cite it to connect Standard Model running to the structural mass formula. It is realized as a direct one-line specialization of the integratedResidue integral.
Claim. Define the residue at the anchor for anomalous dimension structure γ, fermion f and reference scale ln μ_ref by the integrated residue from ln μ⋆ to ln μ_ref: f_i(μ⋆, μ_ref) := (1/λ) ∫_{ln μ⋆}^{ln μ_ref} γ_i(exp(t)) dt.
background
The module supplies the mathematical framework for RG transport of fermion masses. In the Standard Model the running obeys d(ln m)/d(ln μ) = -γ_m(μ); the integrated residue between scales is f(μ₀, μ₁) = (1/λ) ∫_{ln μ₀}^{ln μ₁} γ_m(μ') d(ln μ') with λ = ln φ. AnomalousDimension is the structure carrying gamma : Fermion → ℝ → ℝ together with smoothness and perturbative boundedness. This definition fixes the lower limit at the anchor lnMuStar, yielding the transport expression that the axiom f_residue in AnchorPolicy.lean is meant to represent.
proof idea
One-line wrapper that applies integratedResidue γ f lnMuStar lnμ_ref, thereby evaluating the definite integral of the anomalous dimension component for the chosen fermion between the anchor and the reference scale.
why it matters
It supplies the RG side of the residue used by anchorClaimHolds to assert |residueAtAnchor γ f lnμ_ref - gap(ZOf f)| < tolerance and by mass_ratio_phi_power to obtain the φ-power mass ratio. The definition therefore closes the transport step in Single Anchor Phenomenology, linking the running couplings of the Standard Model to the Recognition Science mass formula m_phys = m_struct · φ^{-f} and the phi-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.