lightQuarkMass
plain-language theorem explainer
The declaration supplies the numerical value for the average up and down quark mass used in Recognition Science modeling of QCD confinement. Researchers computing string breaking lengths or Cornell potentials from J-cost scaling would reference this constant when estimating hadronization thresholds. It is introduced as a direct numerical assignment of 0.003 in GeV units.
Claim. The typical light quark mass (up/down average) is defined as $m_q = 0.003$ GeV.
background
The QFT.Confinement module derives quark confinement from J-cost distance scaling, where the potential takes the form J(r) ≈ -α/r + σ r. The linear term produces a constant force whose string tension sets the scale for confinement, while the short-distance term recovers asymptotic freedom. This definition provides the light quark mass input needed for estimates of breaking lengths via σ r = 2 m_quark.
proof idea
The definition is a direct numerical assignment with no lemmas or tactics applied.
why it matters
This constant supplies the mass scale required for string-breaking calculations in the confinement model, where the module targets derivation of linear potentials from J-cost structure. It supports the SM-007 paper proposition on confinement emerging from Recognition Science's forcing chain and RCL. No downstream uses are recorded, leaving its integration with the phi-ladder mass formula open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.