pith. machine review for the scientific record. sign in
structure definition def or abbrev high

RunningCouplingsProofs

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 199structure RunningCouplingsProofs where
 200  qcd_af : beta0_SUN 3 6 > 0
 201  su2_beta : beta0_SUN 2 6 = 10/3
 202  gut_structure : (24 : ℕ) = 8 * 3
 203  proton_ratio : 4 < protonToQCDRatio ∧ protonToQCDRatio < 6
 204
 205/-- We can construct this proof summary. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.