RunningCouplingsProofs
plain-language theorem explainer
RunningCouplingsProofs bundles four statements on beta-function coefficients and the proton-to-QCD ratio inside the Recognition Science QFT module. A physicist modeling φ-scaled renormalization-group flow would cite it to record asymptotic freedom for SU(3) and the factor-of-five mass ratio. The structure is assembled by direct field assignments that invoke the upstream beta0_SUN evaluations and the proton ratio bound.
Claim. The structure asserts β₀(SU(3), N_f=6) > 0, β₀(SU(2), N_f=6) = 10/3, the integer identity 24 = 8 × 3, and 4 < proton-mass / Λ_QCD < 6.
background
The module treats running couplings as the variation of J-cost with φ-ladder rung, where each rung labels a distinct energy scale. The one-loop coefficient is supplied by the definition β₀(N, N_f) = (11N − 2N_f)/3. Upstream results record that this expression equals 7 for QCD (N=3, N_f=6) and that the proton mass is approximately five times Λ_QCD.
proof idea
The structure is populated by direct field assignments that reference the lemmas qcd_asymptotic_free, su2_beta0, gut_24_from_8_times_3 and proton_qcd_ratio.
why it matters
The structure supplies the verified facts that are assembled into runningCouplingsProofs, thereby closing the QFT-011 target on φ-scaled running couplings. It records the positivity of the QCD beta coefficient and the proton-to-QCD ratio near five, both required for the Recognition Science account of asymptotic freedom and mass generation on the φ-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.