SuperPair
plain-language theorem explainer
SuperPair introduces a record type holding a boson identifier, its fermionic partner identifier, and the real-valued mass splitting between them. Researchers modeling supersymmetry breaking via J-cost asymmetry in Recognition Science cite this when enumerating concrete candidate pairs. The declaration is a direct structure definition with three fields and no computational content or lemmas.
Claim. A superpartner pair consists of a boson string identifier, a fermion string identifier, and a real number $m$ that records the mass difference between the pair.
background
The StandardModel.SupersymmetryBreaking module targets SM-010: deriving supersymmetry breaking from J-cost differences. In Recognition Science the J-cost satisfies the Recognition Composition Law and receives distinct averages for bosons versus fermions because of the eight-tick phase structure (T7). Upstream anchors Z and W from Masses.Anchor map electric charges to integer rungs on the phi-ladder, while OptionAEmpiricalProgram.is and EdgeLengthFromPsi.is supply collision-free and algebraic checks that keep the ledger consistent.
proof idea
The declaration is a plain structure definition that introduces the three fields boson, fermion, and mass_splitting with no lemmas or tactics applied.
why it matters
SuperPair supplies the data carrier used by the downstream superpartners definition to list explicit pairs such as selectron-electron at 1000 GeV. It supports the module goal of showing that J-cost asymmetry arising from the eight-tick octave forces spontaneous breaking above the TeV scale, consistent with the T7 and D=3 landmarks of the forcing chain. The parent result is the superpartners list that feeds viability and LHC-limit checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.