pith. machine review for the scientific record. sign in
def

step_up_gen1

definition
show as:
view math explainer →
module
IndisputableMonolith.Masses.RungConstructor.Motif
domain
Masses
line
60 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.RungConstructor.Motif on GitHub at line 60.

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

  57The lepton torsion {0, 11, 17} remains DERIVED (from edge/face geometry). -/
  58
  59/-- Up-quark generation steps: {V+F-C=13, E_pass=11}. HYPOTHESIS. -/
  60def step_up_gen1 : ℤ := 13   -- V + F - C = 8 + 6 - 1
  61def step_up_gen2 : ℤ := 11   -- E_pass = E - A = 12 - 1
  62
  63/-- Down-quark generation steps: {F=6, V=8}. HYPOTHESIS. -/
  64def step_down_gen1 : ℤ := 6   -- F = 2D = 6
  65def step_down_gen2 : ℤ := 8   -- V = 2^D = 8
  66
  67/-- Sector-dependent cumulative generation torsion.
  68    CANONICAL for all fermion sectors. -/
  69def tau_sdgt (sector : Sector) (gen : ℕ) : ℤ :=
  70  match sector, gen with
  71  | _, 0           => 0
  72  | .Lepton, 1     => step_gen1                         -- 11 = E_pass
  73  | .Lepton, _     => step_gen1 + step_gen2_charged     -- 17 = W
  74  | .UpQuark, 1    => step_up_gen1                      -- 13 = V+F-C
  75  | .UpQuark, _    => step_up_gen1 + step_up_gen2       -- 24 = 2E
  76  | .DownQuark, 1  => step_down_gen1                    -- 6  = F
  77  | .DownQuark, _  => step_down_gen1 + step_down_gen2   -- 14 = V+F
  78  | .Neutrino, 1   => step_gen1                         -- 11
  79  | .Neutrino, _   => step_gen1 + step_gen2_neutrino    -- 19
  80  | .Electroweak, _ => 0
  81
  82/-- Sector-global length baseline. -/
  83def ell_baseline : Sector → ℤ
  84  | .Lepton      => 2
  85  | .Neutrino    => 0
  86  | .UpQuark     => 4
  87  | .DownQuark   => 4
  88  | .Electroweak => 1
  89
  90/-- Legacy rung constructor (universal torsion {0,11,17} for all charged).