module module moderate

`IndisputableMonolith.Physics.RGTransport`

Abstract RG-transport layer for Recognition Science: running couplings at scale μ, one-loop QCD/QED beta functions, and mass anomalous dimensions used to move masses and couplings between the anchor scale and lab scales. Phenomenologists matching the geometric mass ladder to SM evolution cite it. Mostly definitions plus elementary positivity and asymptotic-freedom facts for the QCD coefficient.

claimThe module packages a running coupling at renormalization scale $\mu$, an anomalous dimension, a positive QCD scale $\Lambda$, and the one-loop coefficients $\beta_0^{\mathrm{QCD}}$, $\beta^{\mathrm{QCD}}_{1\mathrm{L}}$, $\beta^{\mathrm{QED}}_{1\mathrm{L}}$, $\gamma_m^{\mathrm{QCD}}$, $\gamma_m^{\mathrm{QED}}$, including the $n_f=0$ specialization and asymptotic freedom of $\beta_0^{\mathrm{QCD}}$.

background

Recognition Science fixes particle masses at a single anchor scale $\mu_\star$ via the geometric ladder: yardstick times $\varphi$ to a power set by rung and the gap $F(Z)=\ln(1+Z/\varphi)/\ln\varphi$, with $Z$ the charge-indexed integer from the fermion species map. Laboratory values then require renormalization-group transport from $\mu_\star$ down (or up) to the measurement scale.

This module supplies that transport interface without committing to a full SM matching. A running coupling is an abstract map of scale; concrete $\alpha_s$, $\alpha$, $\alpha_2$ are meant as specializations. One-loop beta functions and mass anomalous dimensions for QCD and QED are the standard coefficients used in that transport. The QCD scale $\Lambda$ is required positive.

Upstream, Constants fixes RS-native units (including the tick) and RSBridge.Anchor defines fermions, $Z$, $F(Z)$, and mass-at-anchor. Downstream policy modules wire these coefficients into a single-anchor phenomenology and into certificates that $\mu_\star$ is not fixed by fermion mass inputs.

proof idea

Definition-heavy module, not a single theorem. It introduces the abstract running-coupling and anomalous-dimension interfaces, names the one-loop QCD/QED beta and mass-gamma coefficients (including real-valued and $n_f=0$ forms), and records elementary lemmas: positivity of $\Lambda$ and asymptotic freedom of $\beta_0^{\mathrm{QCD}}$. No deep derivation of the beta functions from a Lagrangian; the coefficients are taken as the standard one-loop inputs for later RG policy and coupling-discrepancy arguments.

why it matters in Recognition Science

Single-anchor mass phenomenology needs a clean Lean surface for RG evolution between $\mu_\star$ and lab scales. This module is that surface. Physics.AnchorPolicy imports it to isolate assumptions about the anchor and radiative stability while wiring $F(Z)$ and $\varphi$. Physics.RecognitionCoupling uses the same transport language to formalize the gap between perturbative RG running and the large geometric residue required by the mass formula (the "missing strength"). Verification.AnchorNonCircularityCert depends on the stack to certify that $\mu_\star\approx 182.201,\mathrm{GeV}$ is fixed by structural stationarity, not by feeding fermion masses into the RG fit. In the broader chain it sits under the mass ladder and the anchor bridge, not under T5–T8 forcing.

scope and limits

Does not derive one-loop beta or gamma coefficients from a Lagrangian or path integral.
Does not specialize the abstract running coupling to numerical $\alpha_s(\mu)$, $\alpha(\mu)$, or $\alpha_2(\mu)$.
Does not prove multi-loop, threshold-matched, or scheme-converted SM RG evolution.
Does not fix the numerical anchor scale $\mu_\star$ or prove non-circularity of that scale.
Does not resolve the geometric-versus-perturbative residue discrepancy; that lives downstream.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.AnchorPolicy module_import
IndisputableMonolith.Physics.RecognitionCoupling module_import
IndisputableMonolith.Verification.AnchorNonCircularityCert module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.RSBridge.Anchor module_import

declarations in this module (30)

structure RunningCoupling L70
structure AnomalousDimension L81
def lambda L92
theorem lambda_pos L95
def beta0QCD L102
def beta0QCDReal L105
def betaQCD1L L109
def betaQED1L L114
def gammaMassQCD1L L119
def gammaMassQED1L L123
theorem beta0QCD_nf0 L126
theorem beta0QCD_asymp_free L129
theorem betaQCD1L_vanishes_at_zero L139
theorem gammaMassQCD1L_zero L143
def rk4Increment L149
def rk4Step L153
theorem rk4Step_eq_self_of_zero L160
theorem abs_rk4Increment_le L167
theorem rk4Step_deviation_le L199
def integratedResidue L227
def runningMass L237
theorem mass_ratio_formula L243
def muStar L253
theorem muStar_pos L255
def lnMuStar L258
def residueAtAnchor L265
def anchorClaimHolds L274
def residueDerivative L284
theorem stationarity_iff_gamma_zero L287
theorem mass_ratio_phi_power L307