AnomalousDimension
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.