protonMassBreakdown
plain-language theorem explainer
protonMassBreakdown records the proton mass as 0.938 GeV with a 1% quark-mass share and 99% string contribution. QCD model builders cite this breakdown when testing whether J-cost scaling reproduces the observed hadron spectrum. The definition constructs the HadronMass record directly and verifies the arithmetic sum by norm_num.
Claim. The proton mass $M_p = 0.938$ GeV decomposes as quark-mass contribution $0.010$ GeV plus string contribution $0.928$ GeV, satisfying $M_p = 0.010 + 0.928$.
background
In the Recognition Science treatment of QCD, the HadronMass structure encodes that a hadron's total mass equals the sum of its quark-mass contribution and its string (binding) contribution. For light hadrons the string term dominates. The module SM-007 derives confinement from J-cost distance scaling, where the potential takes the form $J(r) ≈ -α/r + σr$ with the linear term producing a constant force at long distance.
proof idea
The definition directly populates the HadronMass record with the proton name, total mass 0.938, quark share 0.010, and string share 0.928. The equality total_eq is discharged by a single norm_num tactic that confirms the arithmetic identity.
why it matters
This definition supplies the concrete numerical content for the 'Mass Without Mass' statement that the proton mass is mostly QCD binding energy. It illustrates the long-distance linear term in the J-cost potential derived in the parent confinement module. The construction closes the gap between the abstract HadronMass structure and the empirical 938 MeV value, supporting the claim that confinement arises from J-cost scaling rather than from explicit quark masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.