charm_up_equal_Z

formal source

  55
  56/-! ## Equal-Z within a sector implies pure φ-power ratios -/
  57
  58theorem charm_up_equal_Z : ZOf .u = ZOf .c := by
  59  obtain ⟨hu, hc, _⟩ := ZOf_up_quarks
  60  rw [hu, hc]
  61
  62theorem top_up_equal_Z : ZOf .u = ZOf .t := by
  63  obtain ⟨hu, _, ht⟩ := ZOf_up_quarks
  64  rw [hu, ht]
  65
  66theorem strange_down_equal_Z : ZOf .d = ZOf .s := by
  67  obtain ⟨hd, hs, _⟩ := ZOf_down_quarks
  68  rw [hd, hs]
  69
  70theorem bottom_down_equal_Z : ZOf .d = ZOf .b := by
  71  obtain ⟨hd, _, hb⟩ := ZOf_down_quarks
  72  rw [hd, hb]
  73
  74/-! ## Generation rung spacing (proved directly from Integers definitions) -/
  75
  76open Integers in
  77theorem up_generation_spacing :
  78    r_up "c" - r_up "u" = 11 ∧ r_up "t" - r_up "u" = 17 := by
  79  decide
  80
  81open Integers in
  82theorem down_generation_spacing :
  83    r_down "s" - r_down "d" = 11 ∧ r_down "b" - r_down "d" = 17 := by
  84  decide
  85
  86/-! ## Structural ratios that already match PDG order of magnitude
  87
  88These are theorems in `Masses.Verification`. We re-export them under