pith. machine review for the scientific record. sign in
def definition def or abbrev high

superpartners

show as:
view Lean formalization →

Definition enumerates four example superpartner pairs with mass splittings in GeV. Model builders studying J-cost asymmetries in the Standard Model cite it to anchor SUSY breaking discussions against LHC data. Construction is a direct list literal of SuperPair structures with no computation or lemmas.

claimDefine superpartners as the list of structures each holding a boson name, its fermionic partner name, and a real mass splitting: (selectron, electron, 1000), (squark, quark, 1500), (gluino, gluon, 2000), (photino, photon, 500) with values in GeV.

background

SuperPair is the structure that records a boson name, a fermion name, and the real-valued mass splitting between them. The module places this definition inside the Recognition Science account of supersymmetry breaking, where J-cost differs between bosonic and fermionic sectors because of the eight-tick phase structure. Upstream results include the unification theorem that supplies the three Aristotelian conditions on any recognizer and the PhiForcingDerived structures that calibrate J-cost.

proof idea

Direct list literal construction of four SuperPair values; no lemmas or tactics are invoked beyond the structure definition itself.

why it matters in Recognition Science

Supplies the concrete data consumed by the softBreaking definition and the susy_breaking_scale theorem. It instantiates the Recognition Science claim that J-cost asymmetry across the phi-ladder spontaneously breaks supersymmetry, consistent with the eight-tick octave and the requirement that D equals three spatial dimensions. It touches the open question of whether the listed splittings remain compatible with current LHC bounds.

scope and limits

formal statement (Lean)

  66def superpartners : List SuperPair := [

proof body

Definition body.

  67  ⟨"selectron", "electron", 1000⟩,  -- GeV
  68  ⟨"squark", "quark", 1500⟩,
  69  ⟨"gluino", "gluon", 2000⟩,
  70  ⟨"photino", "photon", 500⟩
  71]
  72
  73/-! ## Why SUSY is Attractive -/
  74
  75/-- Benefits of supersymmetry:
  76
  77    1. **Hierarchy problem**: Cancels quadratic divergences
  78    2. **Gauge coupling unification**: Couplings meet at ~10¹⁶ GeV
  79    3. **Dark matter candidate**: Lightest superpartner (LSP)
  80    4. **String theory**: Requires SUSY for consistency -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.