AnomalousDimension
The declaration defines a structure bundling a function gamma from fermions and renormalization scales to reals, together with differentiability for each fermion and a uniform bound on its absolute value for mu greater than 1. Researchers formalizing RG flow between structural and physical masses in the Recognition Science framework cite this carrier when deriving residues from the phi-ladder mass formula. The definition is a direct structure packaging the function with its analytic requirements.
claimA structure consisting of a map $gamma : F to mathbb{R} to mathbb{R}$ (with $F$ the set of fermion species) that gives the mass anomalous dimension $gamma_m(mu)$, together with the statements that $gamma(f)$ is differentiable for each $f$ and that there exists $B>0$ such that $|gamma(f,mu)|<B$ whenever $mu>1$.
background
The RGTransport module formalizes renormalization-group transport of mass residues. Fermion masses run according to $d(ln m)/d(ln mu) = -gamma_m(mu)$, and the integrated residue between scales is $f(mu_0,mu_1)=(1/lambda)int_{ln mu_0}^{ln mu_1} gamma_m(exp t) dt$ with normalization $lambda=ln phi$. The structure supplies the mathematical object that carries this gamma_m into the mass relation $m_phys = m_struct cdot phi^{-f}$.
proof idea
This is a structure definition that directly packages the gamma function field with the two required properties (differentiability and perturbative boundedness). No lemmas are invoked and no tactics are executed; the declaration itself is the carrier type used by downstream integral and identity statements.
why it matters in Recognition Science
AnomalousDimension is the input type to integratedResidue, residueAtAnchor, and the theorems display_identity_at_anchor, stationary_at_anchor, and anchorClaimHolds. It supplies the anomalous-dimension slot in the RG-transport step that connects the phi-ladder mass formula to the Single Anchor Phenomenology claim residueAtAnchor gamma f (ln m_phys) approx gap(ZOf f). The structure therefore closes the formal link between the T5 J-uniqueness and T6 phi fixed-point machinery and observable mass ratios.
scope and limits
- Does not supply explicit QCD or QED beta-function kernels for gamma_m.
- Does not evaluate the integrated residue for any concrete fermion.
- Does not prove existence of a gamma satisfying the smoothness and bound axioms.
- Does not incorporate higher-order running or threshold effects.
formal statement (Lean)
81structure AnomalousDimension where
82 /-- The anomalous dimension value for fermion f at scale μ. -/
83 gamma : Fermion → ℝ → ℝ
84 /-- The anomalous dimension is smooth (differentiable). -/
85 smooth : ∀ f, Differentiable ℝ (gamma f)
86 /-- Perturbative bound: |γ| is bounded in the perturbative regime. -/
87 pert_bounded : ∃ B > 0, ∀ f μ, μ > 1 → |gamma f μ| < B
88
89/-! ## RG Transport Integral -/
90
91/-- The λ-normalization constant: `λ = ln(φ)`. -/