def
definition
step_up_gen1
show as:
view math explainer →
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
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).