proton_qcd_ratio
plain-language theorem explainer
The theorem establishes that the proton mass lies between four and six times the QCD scale. Researchers modeling hadron masses on the Recognition Science phi-ladder would cite the bound to anchor the mass formula at the QCD rung. The proof is a term-mode verification that unfolds the ratio definition and checks the numerical inequality directly.
Claim. $4 < m_p / 200 < 6$ where $m_p = 938$ MeV is the proton mass and the QCD scale equals 200 MeV.
background
The QFT.RunningCouplings module derives running couplings from phi-ladder scaling, where distinct rungs label energy scales and J-cost optimization changes with rung. Lambda_QCD is defined as the constant 200 MeV, stated to lie in the 100-300 MeV range. ProtonToQCDRatio is the quotient 938 divided by that scale, and the theorem confirms the quotient lies in (4,6).
proof idea
The term proof unfolds protonToQCDRatio and lambda_QCD to expose the concrete quotient 938/200, splits the conjunction via constructor, and invokes norm_num to verify both sides of the inequality.
why it matters
The result supplies the proton_ratio field inside the runningCouplingsProofs structure that aggregates qcd_asymptotic_free, su2_beta0, gut_24_from_8_times_3 and this bound. It supplies the numerical check that the proton mass is approximately five times Lambda_QCD, closing one concrete instance of the phi-ladder mass formula inside the QFT-011 running-couplings derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.