IndisputableMonolith.Masses.RungConstructor.Basic

   1import Mathlib
   2import IndisputableMonolith.Masses.RSBridge.Anchor
   3
   4namespace IndisputableMonolith
   5namespace Masses
   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
  40end RungConstructor
  41end Masses
  42end IndisputableMonolith
  43