module module high

`IndisputableMonolith.Physics.RGTransport`

The module supplies an abstract interface for running couplings at renormalization scale μ within the Recognition Science framework. Researchers modeling RG flow between the anchor scale and physical masses on the phi-ladder would cite it when bridging geometric mass formulas to perturbative transport. The module declares RunningCoupling, AnomalousDimension, and one-loop beta functions for QCD and QED as placeholders for later SM specializations.

claimLet $α(μ)$ be the running coupling at scale $μ$. The beta function satisfies $β(α) = μ dα/dμ$, with one-loop coefficients $β_0^{QCD}$ and $β_0^{QED}$ together with anomalous dimensions $γ_m^{QCD}$ and $γ_m^{QED}$.

background

The module imports Constants (where $τ_0 = 1$ tick is the fundamental RS time quantum) and RSBridge.Anchor. The latter defines the 12 Standard Model fermions, the charge-indexed integer $Z_i = q̃² + q̃⁴$ (+4 for quarks), the gap display function $F(Z) = ln(1 + Z/φ)/ln(φ)$, and the mass at the anchor scale $μ_⋆$. These objects supply the geometric input that RG transport must carry to low-energy scales.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds AnchorPolicy, which isolates assumptions about the single anchor scale and radiative stability for the mass framework, and RecognitionCoupling, which quantifies the discrepancy between perturbative RG transport and the geometric mass formula requiring a large residue $F(Z)$. It therefore supplies the RG layer needed to compare the phi-ladder predictions with observed couplings.

scope and limits

Does not specialize the abstract interface to concrete SM values for $α_s$, $α$, or $α_2$.
Does not implement higher-loop or non-perturbative corrections.
Does not compute explicit numerical running from $μ_⋆$ to the electroweak scale.
Does not derive the beta functions from the underlying J-cost or RCL axioms.

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