lhcLimits
plain-language theorem explainer
LHC limits on superpartners are recorded as a list of lower mass bounds in GeV for squarks, gluinos, sleptons and charginos. A physicist embedding collider data into a Recognition Science model of supersymmetry breaking would cite this list to fix the breaking scale above 1 TeV. The definition is a direct enumeration with no derivation or lemma application.
Claim. The LHC lower bounds on supersymmetric particle masses are given by the list $[(``squarks'', 1500), (``gluinos'', 2000), (``sleptons'', 500), (``charginos'', 500)]$ in GeV.
background
Recognition Science treats supersymmetry as a possible boson-fermion symmetry that is broken by an asymmetry in J-cost. The J-cost functional satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ and acquires different values for bosons and fermions because of the eight-tick octave structure. The module therefore requires an empirical anchor for the breaking scale.
proof idea
The declaration is a direct definition that constructs the four-element list of string-real pairs. No lemmas or tactics are invoked; the body is a literal enumeration of the reported LHC bounds.
why it matters
The definition supplies the experimental floor that any J-cost-derived breaking mechanism must satisfy. It supports sibling declarations on SUSY viability and LSP candidates inside the same module. The surrounding text links the bounds to the eight-tick phase difference between boson and fermion sectors, consistent with the T7 octave and T8 dimension steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.