IndisputableMonolith.Masses.RungConstructor.Motif

   1import Mathlib
   2import IndisputableMonolith.Masses.RungConstructor.Basic
   3
   4namespace IndisputableMonolith
   5namespace Masses
   6namespace RungConstructor
   7
   8/-! ## Generation Step Constants
   9
  10### Sector-Dependent Generation Torsion (SDGT)
  11
  12Each fermion sector uses different cube cell counts for its generation steps.
  13The four step values form a cyclic chain:
  14
  15  V+F-C=13 → E_pass=11 → F=6 → V=8
  16
  17Each sector takes two consecutive values:
  18- Up quarks:   {V+F-C=13, E_pass=11}, total = 2E = 24
  19- Leptons:     {E_pass=11, F=6},       total = W = 17
  20- Down quarks: {F=6, V=8},             total = V+F = 14
  21
  22The three spans partition N₃ = 2D^D + 1 = 55.
  23Lean proof: `IndisputableMonolith.Masses.SectorDependentTorsion`
  24
  25### Legacy (universal torsion, leptons only)
  26
  27The old convention used {0, 11, 17} for all charged fermions.
  28This is retained as `tau_charged` for backward compatibility but
  29is accurate only for leptons. Use `tau_sdgt` for quarks. -/
  30
  31def step_gen1 : ℤ := 11
  32def step_gen2_charged : ℤ := 6
  33def step_gen2_neutrino : ℤ := 8
  34
  35/-- Cumulative generation torsion for leptons (legacy name: tau_charged).
  36    CORRECT for leptons. For quarks, use tau_sdgt. -/
  37def tau_charged (gen : ℕ) : ℤ :=
  38  match gen with
  39  | 0 => 0
  40  | 1 => step_gen1
  41  | _ => step_gen1 + step_gen2_charged  -- gen ≥ 2
  42
  43/-- Cumulative generation torsion for neutrinos. -/
  44def tau_neutrino (gen : ℕ) : ℤ :=
  45  match gen with
  46  | 0 => 0
  47  | 1 => step_gen1
  48  | _ => step_gen1 + step_gen2_neutrino  -- gen ≥ 2
  49
  50/-! ### SDGT: Sector-specific generation torsion (HYPOTHESIS for quarks)
  51
  52These quark-sector torsion values were identified from PDG same-scale
  53mass ratios, then matched to Q₃ cell counts. The integers ARE cube-geometric
  54(Lean-proved), but the assignment of specific integers to specific sectors
  55is a HYPOTHESIS, not a first-principles derivation.
  56
  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).
  91    CORRECT for leptons and neutrinos. For quarks, use compute_rung_sdgt. -/
  92def compute_rung (s : Species) : ℤ :=
  93  match s with
  94  | .fermion f =>
  95      let sector := sectorOf (.fermion f)
  96      let gen := (RSBridge.genOf f).val
  97      match sector with
  98      | .Neutrino => ell_baseline sector + tau_neutrino gen
  99      | _         => ell_baseline sector + tau_charged gen
 100  | .W | .Z | .H =>
 101      ell_baseline .Electroweak
 102
 103/-- SDGT rung constructor (sector-dependent torsion).
 104    Lepton rungs: DERIVED. Quark rungs: HYPOTHESIS (from PDG data). -/
 105def compute_rung_sdgt (s : Species) : ℤ :=
 106  match s with
 107  | .fermion f =>
 108      let sector := sectorOf (.fermion f)
 109      let gen := (RSBridge.genOf f).val
 110      ell_baseline sector + tau_sdgt sector gen
 111  | .W | .Z | .H =>
 112      ell_baseline .Electroweak
 113
 114end RungConstructor
 115end Masses
 116end IndisputableMonolith
 117