QCDString
plain-language theorem explainer
QCDString encodes a flux tube between quark and antiquark whose length is positive and whose stored energy equals string tension times length. Researchers modeling hadronization in QCD would cite this structure when applying the energy threshold for string breaking. It is introduced as a direct structure definition with four fields that enforce the linear relation without further lemmas.
Claim. A QCD string is a pair of real numbers $l > 0$ and $E$ satisfying $E = σ l$, where $σ$ is the string tension.
background
The module treats confinement as a consequence of J-cost distance scaling in Recognition Science. At long distances the J-cost grows linearly with separation, yielding a constant force and therefore a string tension; the short-distance term remains Coulomb-like. Energy and Length are imported as aliases for the reals from RSNativeUnits, while upstream ledger factorization supplies the calibration of J itself.
proof idea
The declaration is a direct structure definition. It introduces four fields: length as a real, a positivity witness, energy as a real, and the equality energy = stringTension * length. No lemmas or tactics are invoked beyond the structure constructor.
why it matters
QCDString supplies the object type for the downstream string_breaking theorem that encodes hadronization once energy exceeds twice the quark mass. It realizes the long-distance linear term in the module's J(r) ≈ -α/r + σ r potential, linking to the Recognition Science forcing chain through the constants and phi-ladder machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.