IndisputableMonolith.Masses.RungConstructor.Proofs

   1import Mathlib
   2import IndisputableMonolith.Masses.Anchor
   3import IndisputableMonolith.RSBridge.Anchor
   4import IndisputableMonolith.Masses.RungConstructor.Motif
   5
   6namespace IndisputableMonolith
   7namespace Masses
   8namespace RungConstructor
   9
  10open RSBridge
  11
  12/-- Proof that the rung constructor reproduces the charged lepton table. -/
  13theorem match_lepton_e : compute_rung (.fermion .e) = 2 := by rfl
  14
  15theorem match_lepton_mu : compute_rung (.fermion .mu) = 13 := by rfl
  16
  17theorem match_lepton_tau : compute_rung (.fermion .tau) = 19 := by rfl
  18
  19/-- Proof that the rung constructor reproduces the up-quark table. -/
  20theorem match_up_u : compute_rung (.fermion .u) = 4 := by rfl
  21
  22theorem match_up_c : compute_rung (.fermion .c) = 15 := by rfl
  23
  24theorem match_up_t : compute_rung (.fermion .t) = 21 := by rfl
  25
  26/-- Proof that the rung constructor reproduces the down-quark table. -/
  27theorem match_down_d : compute_rung (.fermion .d) = 4 := by rfl
  28
  29theorem match_down_s : compute_rung (.fermion .s) = 15 := by rfl
  30
  31theorem match_down_b : compute_rung (.fermion .b) = 21 := by rfl
  32
  33/-- Proof that the rung constructor reproduces the boson table. -/
  34theorem match_boson_W : compute_rung .W = 1 := by rfl
  35
  36theorem match_boson_Z : compute_rung .Z = 1 := by rfl
  37
  38theorem match_boson_H : compute_rung .H = 1 := by rfl
  39
  40/-- Proof that the constructor matches the legacy `RSBridge.rung` mapping for charged leptons. -/
  41theorem match_rsbridge_rung_charged_leptons :
  42    compute_rung (.fermion .e) = RSBridge.rung .e ∧
  43    compute_rung (.fermion .mu) = RSBridge.rung .mu ∧
  44    compute_rung (.fermion .tau) = RSBridge.rung .tau :=
  45  ⟨rfl, rfl, rfl⟩
  46
  47/-- Proof that the constructor matches the legacy `RSBridge.rung` mapping for up-type quarks. -/
  48theorem match_rsbridge_rung_up_quarks :
  49    compute_rung (.fermion .u) = RSBridge.rung .u ∧
  50    compute_rung (.fermion .c) = RSBridge.rung .c ∧
  51    compute_rung (.fermion .t) = RSBridge.rung .t :=
  52  ⟨rfl, rfl, rfl⟩
  53
  54/-- Proof that the constructor matches the legacy `RSBridge.rung` mapping for down-type quarks. -/
  55theorem match_rsbridge_rung_down_quarks :
  56    compute_rung (.fermion .d) = RSBridge.rung .d ∧
  57    compute_rung (.fermion .s) = RSBridge.rung .s ∧
  58    compute_rung (.fermion .b) = RSBridge.rung .b :=
  59  ⟨rfl, rfl, rfl⟩
  60
  61/-- Proof that the constructor matches the legacy `RSBridge.rung` mapping for neutrinos.
  62    Neutrinos have baseline 0 (due to Z=0) and a different gen-2 step (+8 vs +6). -/
  63theorem match_rsbridge_rung_neutrinos :
  64    compute_rung (.fermion .nu1) = RSBridge.rung .nu1 ∧
  65    compute_rung (.fermion .nu2) = RSBridge.rung .nu2 ∧
  66    compute_rung (.fermion .nu3) = RSBridge.rung .nu3 :=
  67  ⟨rfl, rfl, rfl⟩
  68
  69/-- The master matching theorem: constructor reproduces all legacy rung values. -/
  70theorem match_rsbridge_rung (f : Fermion) : compute_rung (.fermion f) = RSBridge.rung f := by
  71  cases f <;> rfl
  72
  73/-! ## SDGT Rung Proofs (Sector-Dependent Generation Torsion)
  74
  75These are the CANONICAL rungs derived from the cyclic chain 13→11→6→8.
  76Leptons are unchanged. Quarks use sector-specific generation steps. -/
  77
  78/-- SDGT: Leptons unchanged from legacy. -/
  79theorem sdgt_lepton_e : compute_rung_sdgt (.fermion .e) = 2 := by rfl
  80theorem sdgt_lepton_mu : compute_rung_sdgt (.fermion .mu) = 13 := by rfl
  81theorem sdgt_lepton_tau : compute_rung_sdgt (.fermion .tau) = 19 := by rfl
  82
  83/-- SDGT: Up-quark rungs {4, 17, 28} from steps {V+F-C=13, E_pass=11}. -/
  84theorem sdgt_up_u : compute_rung_sdgt (.fermion .u) = 4 := by rfl
  85theorem sdgt_up_c : compute_rung_sdgt (.fermion .c) = 17 := by rfl
  86theorem sdgt_up_t : compute_rung_sdgt (.fermion .t) = 28 := by rfl
  87
  88/-- SDGT: Down-quark rungs {4, 10, 18} from steps {F=6, V=8}. -/
  89theorem sdgt_down_d : compute_rung_sdgt (.fermion .d) = 4 := by rfl
  90theorem sdgt_down_s : compute_rung_sdgt (.fermion .s) = 10 := by rfl
  91theorem sdgt_down_b : compute_rung_sdgt (.fermion .b) = 18 := by rfl
  92
  93/-- SDGT: Neutrinos unchanged. -/
  94theorem sdgt_nu1 : compute_rung_sdgt (.fermion .nu1) = 0 := by rfl
  95theorem sdgt_nu2 : compute_rung_sdgt (.fermion .nu2) = 11 := by rfl
  96theorem sdgt_nu3 : compute_rung_sdgt (.fermion .nu3) = 19 := by rfl
  97
  98/-- SDGT: Bosons unchanged. -/
  99theorem sdgt_boson_W : compute_rung_sdgt .W = 1 := by rfl
 100theorem sdgt_boson_Z : compute_rung_sdgt .Z = 1 := by rfl
 101theorem sdgt_boson_H : compute_rung_sdgt .H = 1 := by rfl
 102
 103/-- SDGT agrees with legacy for leptons, neutrinos, and bosons. -/
 104theorem sdgt_agrees_leptons :
 105    compute_rung_sdgt (.fermion .e) = compute_rung (.fermion .e) ∧
 106    compute_rung_sdgt (.fermion .mu) = compute_rung (.fermion .mu) ∧
 107    compute_rung_sdgt (.fermion .tau) = compute_rung (.fermion .tau) :=
 108  ⟨rfl, rfl, rfl⟩
 109
 110/-- SDGT DIFFERS from legacy for quarks (the whole point!). -/
 111theorem sdgt_differs_up_c : compute_rung_sdgt (.fermion .c) ≠ compute_rung (.fermion .c) := by
 112  decide
 113theorem sdgt_differs_up_t : compute_rung_sdgt (.fermion .t) ≠ compute_rung (.fermion .t) := by
 114  decide
 115theorem sdgt_differs_down_s : compute_rung_sdgt (.fermion .s) ≠ compute_rung (.fermion .s) := by
 116  decide
 117theorem sdgt_differs_down_b : compute_rung_sdgt (.fermion .b) ≠ compute_rung (.fermion .b) := by
 118  decide
 119
 120/-- SDGT generation step verification: the steps match the cyclic chain. -/
 121theorem sdgt_up_step_12 : compute_rung_sdgt (.fermion .c) - compute_rung_sdgt (.fermion .u) = 13 := by
 122  native_decide
 123theorem sdgt_up_step_23 : compute_rung_sdgt (.fermion .t) - compute_rung_sdgt (.fermion .c) = 11 := by
 124  native_decide
 125theorem sdgt_down_step_12 : compute_rung_sdgt (.fermion .s) - compute_rung_sdgt (.fermion .d) = 6 := by
 126  native_decide
 127theorem sdgt_down_step_23 : compute_rung_sdgt (.fermion .b) - compute_rung_sdgt (.fermion .s) = 8 := by
 128  native_decide
 129theorem sdgt_lepton_step_12 : compute_rung_sdgt (.fermion .mu) - compute_rung_sdgt (.fermion .e) = 11 := by
 130  native_decide
 131theorem sdgt_lepton_step_23 : compute_rung_sdgt (.fermion .tau) - compute_rung_sdgt (.fermion .mu) = 6 := by
 132  native_decide
 133
 134end RungConstructor
 135end Masses
 136end IndisputableMonolith
 137