runningCouplingsProofs
plain-language theorem explainer
This definition assembles a record bundling four theorems on the leading beta coefficients for SU(3) and SU(2), the 24-equals-8-times-3 unification relation, and the proton-to-QCD mass ratio. A physicist examining renormalization-group flow in the Recognition Science framework would cite it as the compact summary of all QFT-011 claims. The construction is a direct record literal that references the four component theorems without further reasoning.
Claim. The record of running-coupling proofs is instantiated by the theorems establishing that the one-loop coefficient for SU(3) with six flavors is positive, that the corresponding coefficient for SU(2) with six flavors equals 10/3, that the unification integer satisfies 24 = 8 × 3, and that the proton mass lies strictly between four and six times the QCD scale.
background
Module QFT-011 derives the scale dependence of coupling constants from φ-ladder scaling. In this setting the one-loop beta-function coefficient for an SU(N) gauge theory with f flavors determines whether the coupling decreases at high energy. The structure collects the four central claims: positivity of the coefficient for QCD, its explicit value for SU(2), the numerical relation 24 = 8 × 3 that encodes the eight-tick octave and three spatial dimensions, and the proton-to-QCD ratio lying between 4 and 6.
proof idea
The definition is a one-line record construction that populates each field by direct reference to the corresponding theorem: the QCD asymptotic-freedom result, the SU(2) beta-value theorem, the 24-equals-8-times-3 equality, and the proton-ratio bounds.
why it matters
This record supplies the complete set of proven statements required by the QFT-011 target of deriving running couplings from φ-ladder scaling. It directly supports the Recognition Science unification picture by linking the eight-tick octave and three dimensions through the 24 = 8 × 3 relation while confirming asymptotic freedom and the proton mass scale. No open questions are addressed; the record simply packages the four component theorems for downstream use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.