def
definition
def or abbrev
lhcLimits
show as:
view Lean formalization →
formal statement (Lean)
162def lhcLimits : List (String × ℝ) := [
proof body
Definition body.
163 ("squarks", 1500), -- GeV
164 ("gluinos", 2000),
165 ("sleptons", 500),
166 ("charginos", 500)
167]
168
169/-- Is SUSY still viable?
170
171 Yes, but:
172 - "Natural" SUSY (solving hierarchy without fine-tuning) is strained
173 - Split SUSY (very heavy scalars) is still possible
174 - "Stealth" SUSY (compressed spectra) is hard to detect
175
176 RS doesn't require SUSY, but explains why it would be broken if present. -/