experimentalStatus
plain-language theorem explainer
Recognition Science's J-cost model for QCD confinement receives direct empirical backing from four listed observations: no free quarks, lattice string tension near 0.18 GeV², linear Regge trajectories, and quark-gluon plasma at high temperature. A lattice QCD or hadron spectroscopy researcher would cite the list when comparing RS predictions against data. The definition simply enumerates four ConfinementFalsifier records pairing each test type with its observed status.
Claim. The experimental status is the finite list of pairs $(f_i, s_i)$ where each $f_i$ names a potential falsifier of the J-cost confinement derivation and $s_i$ records its current experimental status: (``Free quark search'', ``No free quarks ever observed''), (``String tension'', ``Matches lattice QCD: σ ≈ 0.18 GeV²''), (``Regge trajectories'', ``Observed in hadron spectroscopy''), (``Quark-gluon plasma'', ``Observed at RHIC and LHC'').
background
The module derives quark confinement from Recognition Science's J-cost distance scaling. At short distances the J-cost behaves as 1/r (Coulomb-like, asymptotic freedom); at long distances it grows linearly as σr, producing a constant force whose tension σ ≈ 0.18 GeV² matches lattice QCD. The ConfinementFalsifier structure pairs a string naming a potential falsifier with a string describing its observed status. Upstream, the Quark inductive type supplies the color-charged objects whose J-cost is computed, while the Matches definition encodes the universal dimensionless bridge that the confinement mechanism must satisfy.
proof idea
The definition is a direct list construction that applies the ConfinementFalsifier structure constructor four times, once for each experimental check. No lemmas or tactics are invoked beyond the inductive definition of the list type.
why it matters
This definition supplies the empirical anchor for SM-007, the Recognition Science derivation of confinement from J-cost scaling. It closes the loop from the T5 J-uniqueness and T6 phi fixed-point steps to observable hadron data, feeding the parent confinement_at_long_distance and potential_confining declarations. The list directly supports the paper claim that the linear term in J(r) ≈ -α/r + σr accounts for the absence of free quarks and the measured string tension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.