module module high

`IndisputableMonolith.Physics.RGTransport`

RGTransport supplies an abstract interface for the running coupling at renormalization scale μ. It enables specialization to the SM couplings α_s, α, α_2 within the Recognition Science bridge to particle physics. Researchers comparing geometric mass ladders to perturbative flows cite it for the RG transport layer. The module consists of definitions for beta functions and anomalous dimensions that draw directly on the imported Anchor and Constants infrastructure.

claimThe running coupling $\alpha(\mu)$ at scale $\mu$, supplied as an abstract interface with specializations to the Standard Model values $\alpha_s(\mu)$, $\alpha(\mu)$, $\alpha_2(\mu)$.

background

The module imports the RS time quantum $\tau_0 = 1$ tick from Constants and the core bridge from RSBridge.Anchor. The latter defines the 12 Standard Model fermions, the charge index $Z_i = \tilde{q}^2 + \tilde{q}^4$ (+4 for quarks), the gap function $F(Z) = \ln(1 + Z/\phi)/\ln(\phi)$, and the mass at the anchor scale $\mu^\star$.

This supplies the local theoretical setting for RG transport in the physics domain, linking the recognition framework to particle physics. The abstract interface isolates the running-coupling object so that downstream modules can depend on a clean surface without committing to explicit beta-function forms.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the Single-Anchor RG Policy in AnchorPolicy and the Recognition Coupling analysis in RecognitionCoupling. It supplies the running-coupling interface required to quantify the discrepancy between the geometric mass formula (large residue $F(Z)$) and perturbative RG transport.

scope and limits

Does not implement explicit beta functions for QCD or QED.
Does not compute numerical running of couplings.
Does not derive the couplings from the recognition axioms.
Does not address multi-loop or non-perturbative corrections.

used by (2)

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

IndisputableMonolith.Physics.AnchorPolicy module_import
IndisputableMonolith.Physics.RecognitionCoupling 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