`Species`

definition

show as: view math explainer →

module: IndisputableMonolith.Masses.RungConstructor.Basic
domain: Masses
line: 9 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.RungConstructor.Basic on GitHub at line 9.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

   6namespace RungConstructor
   7
   8/-- Canonical species for the mass framework. -/
   9inductive Species
  10  | fermion (f : RSBridge.Fermion)
  11  | W
  12  | Z
  13  | H
  14  deriving DecidableEq, Repr
  15
  16open RSBridge
  17
  18/-- Sector identifier (local copy to avoid circular import).
  19    Note: Neutrino is distinct from Lepton because it has a different baseline (0 vs 2). -/
  20inductive Sector | Lepton | Neutrino | UpQuark | DownQuark | Electroweak
  21  deriving DecidableEq, Repr
  22
  23/-- Sector mapping for the rung constructor. -/
  24def sectorOf : Species → Sector
  25  | .fermion f =>
  26      match RSBridge.sectorOf f with
  27      | .lepton   => .Lepton
  28      | .neutrino => .Neutrino
  29      | .up       => .UpQuark
  30      | .down     => .DownQuark
  31  | .W | .Z | .H => .Electroweak
  32
  33/-- Charge-index q̃ used as input to the constructor motifs. -/
  34def tildeQ : Species → ℤ
  35  | .fermion f => RSBridge.tildeQ f
  36  | .W => 0
  37  | .Z => 0
  38  | .H => 0
  39

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.