HadronMass
HadronMass records a hadron's mass as the sum of a small quark-mass term and a dominant string-energy term generated by linear J-cost growth at long distance. QCD modelers and Recognition Science workers cite the structure to quantify how confinement supplies nearly all the mass of light hadrons. The definition simply packages the four numeric fields together with the additive equality that enforces the decomposition.
claimA structure consisting of a name, a real mass $m$, a real quark-mass contribution $q$, a real string contribution $s$, and the equality $m = q + s$.
background
The module derives quark confinement from J-cost distance scaling: short-distance J-cost falls as $1/r$ while long-distance J-cost grows linearly, $J(r) = -α/r + σ r$. This linear term supplies the constant force (string tension) that prevents isolated quarks. Upstream, PhiForcingDerived.of supplies the explicit J-cost expression obtained from the Recognition Composition Law, while LedgerFactorization.of calibrates the underlying distance measure on the positive reals. PrimitiveDistinction.from reduces the seven-axiom foundation to the four structural conditions used here. Quark enumerates the six flavors; RSNativeUnits.Mass is simply the reals in native units.
proof idea
The declaration is a plain structure definition. It introduces the five fields name, mass, quark_mass_contribution, string_contribution and the equality total_eq that forces the mass to equal the sum of the two contributions. No lemmas or tactics are applied; the structure itself encodes the required additive decomposition.
why it matters in Recognition Science
HadronMass supplies the data carrier for protonMassBreakdown, which exhibits the numerical split showing that the proton mass is 99 percent string energy. It therefore realizes the central claim of SM-007 that light-hadron masses arise from the linear J-cost term rather than current-quark masses. The construction sits inside the phi-forcing chain (T5 J-uniqueness through T8 D=3) and closes the loop from the Recognition Composition Law to observable hadron spectroscopy.
scope and limits
- Does not derive the numerical value of string tension from the phi-ladder.
- Does not compute masses for excited states or glueballs.
- Does not incorporate electromagnetic or weak corrections.
- Does not address the running of the strong coupling at short distances.
formal statement (Lean)
175structure HadronMass where
176 /-- Hadron name. -/
177 name : String
178 /-- Mass in GeV. -/
179 mass : ℝ
180 /-- Quark content contribution. -/
181 quark_mass_contribution : ℝ
182 /-- String/binding contribution. -/
183 string_contribution : ℝ
184 /-- Total = quark + string. -/
185 total_eq : mass = quark_mass_contribution + string_contribution
186
187/-- The proton gets most of its mass from QCD dynamics, not quark masses. -/