module module moderate

`IndisputableMonolith.QFT.RunningCouplings`

This module defines running gauge couplings and beta functions for QFT inside the Recognition Science framework, starting from the low-energy fine structure constant. Workers deriving SM parameters from the phi-ladder or the alpha band would cite these objects. The module is a collection of definitions and elementary lemmas that import the phi-forcing and constant machinery.

claimDefinitions of $\alpha_{em}$(low), $\alpha_{em}(Z)$, $\alpha_s(Z)$, $\alpha_W$, the beta function $\beta(g)$, and the leading coefficients $\beta_0(SU(N))$, $\beta_0(SU(2))$ together with the phi-ladder scale factor.

background

The module sits in the QFT domain and imports the RS time quantum $\tau_0=1$ tick together with the PhiForcing module. PhiForcing establishes that $\phi$ is forced by self-similarity in a discrete ledger equipped with J-cost. The sibling declarations then instantiate the running couplings and one-loop beta coefficients that appear in the standard renormalization-group flow.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the concrete coupling definitions required by any downstream QFT calculation that aims to reproduce the observed alpha band (137.030, 137.039). No used_by edges are recorded yet, so the module currently serves as an interface layer between PhiForcing and later QFT results.

scope and limits

Does not compute numerical values of the couplings from the phi-ladder.
Does not contain higher-loop or non-perturbative corrections.
Does not prove asymptotic freedom or confinement.
Does not link the beta functions to the eight-tick octave or D=3.

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