strange_down_equal_Z

formal source

  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
  89explicit row IDs so the scorecard can be read at a glance.
  90-/
  91
  92/-- P0-Q structural row: m_c / m_u = φ^11 (proved). -/
  93theorem row_charm_up_ratio :
  94    Verification.charm_quark_pred / Verification.up_quark_pred =
  95      Constants.phi ^ (11 : ℕ) :=
  96  Verification.charm_up_ratio