module module moderate

`IndisputableMonolith.QFT.RunningCouplings`

The QFT.RunningCouplings module supplies definitions for gauge coupling evolution in the Recognition Science framework, centered on the low-energy fine structure constant and beta functions for QCD and SU(2). Physicists deriving unification scales or particle masses from the phi-ladder would cite these objects. The module consists of direct definitions and basic lemmas that import the RS time quantum and the self-similarity argument for phi.

claimThe electromagnetic fine structure constant at low energy, denoted $alpha_{em}(0)$, together with the one-loop beta function $beta_0$ for SU(N) groups and the associated QCD asymptotic freedom statements.

background

The module sits in the QFT domain and imports the RS time quantum $tau_0 = 1$ tick from Constants together with the PhiForcing module. The latter establishes that phi is forced by self-similarity in a discrete ledger with J-cost structure. It introduces sibling definitions such as alpha_em_low, betaFunction, qcd_beta0_positive, su2_beta0, and phiLadderScale that place the running couplings on the phi-ladder.

proof idea

This is a definition module, no proofs. Content is supplied by direct definitions and elementary lemmas that reference the imported PhiForcing and Constants modules.

why it matters in Recognition Science

The module supplies the coupling evolution required for the QFT sector of Recognition Science, supporting mass formulas on the phi-ladder and the alpha band (137.030, 137.039). It connects the eight-tick octave to asymptotic freedom statements and feeds the overall derivation of constants from the T0-T8 forcing chain.

scope and limits

Does not derive beta functions from the J-cost equation.
Does not include higher-loop or non-perturbative corrections.
Does not compute explicit numerical values for running couplings.
Does not address gravitational or other non-gauge interactions.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (31)

def alpha_em_low L39
def alpha_em_Z L42
def alpha_s_Z L45
def alpha_W L48
def betaFunction L54
def beta0_SUN L58
theorem qcd_beta0_positive L61
theorem qcd_asymptotic_free L64
theorem su2_beta0 L68
def phiLadderScale L73
lemma phi_ne_zero' L76
lemma phi_gt_one' L79
theorem scale_at_zero L82
theorem scale_at_one L86
theorem scale_at_two L90
theorem phi_ladder_hierarchy L95
def runningCoupling L105
theorem running_at_zero L109
theorem asymptotic_freedom_direction L115
def alpha_GUT L135
theorem gut_24_from_8_times_3 L138
theorem alpha_gut_intermediate L141
def lambda_QCD L151
theorem lambda_qcd_scale L154
def dimensionalTransmutationDescription L163
def protonToQCDRatio L167
theorem proton_qcd_ratio L170
def landauPoleDescription L178
def summary L188
structure RunningCouplingsProofs L199
def runningCouplingsProofs L206