module module high

`IndisputableMonolith.Physics.RGTransport`

The module supplies an abstract interface for the running coupling at renormalization scale μ in the Recognition Science setting. Particle physicists specializing RG flows to SM couplings α_s, α, α_2 would cite it as the entry point before concrete beta-function work. It is a definition module containing no proofs.

claimThe running coupling $α(μ)$ at scale $μ$, an abstract interface whose specializations include the SM values $α_s$, $α$, and $α_2$.

background

Upstream, Constants supplies the RS time quantum $τ_0 = 1$ tick. RSBridge.Anchor supplies the Fermion type (12 SM species), the charge index $Z_i = q̃^2 + q̃^4$ (+4 for quarks), the gap display $F(Z) = ln(1 + Z/φ)/ln(φ)$, and the anchor-scale mass map. The present module sits between these primitives and the RG transport layer, declaring running couplings without committing to a specific renormalization scheme.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds AnchorPolicy (single-anchor RG policy and stability scaffolding) and RecognitionCoupling (addressing the discrepancy between perturbative RG transport and the geometric mass formula). It supplies the abstract surface on which those modules can later impose the phi-ladder and F(Z) residue.

scope and limits

Does not specialize the interface to any concrete SM coupling.
Does not supply explicit beta functions or loop orders.
Does not link running couplings to the phi-ladder mass formula.
Does not address radiative stability or flavor structure.

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