HadronMass
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.