r_up_values

formal source

  53
  54/-! ## Rung Integer Verification -/
  55
  56theorem r_up_values : r_up "u" = 4 ∧ r_up "c" = 15 ∧ r_up "t" = 21 := by
  57  simp only [r_up, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
  58             cube_edges, active_edges_per_tick, D, wallpaper_groups]
  59  omega
  60
  61theorem r_down_values : r_down "d" = 4 ∧ r_down "s" = 15 ∧ r_down "b" = 21 := by
  62  simp only [r_down, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
  63             cube_edges, active_edges_per_tick, D, wallpaper_groups]
  64  omega
  65
  66/-! ## Sector Parameter Verification
  67
  68The up-quark sector has B_pow = -1, r0 = 35.
  69Effective exponent: -5 + 35 + r = 30 + r.
  70Scale: 2^(-1) / 10^6 = 1 / (2 × 10^6).
  71
  72The down-quark sector has B_pow = 23, r0 = -5.
  73Effective exponent: -5 + (-5) + r = -10 + r.
  74Scale: 2^23 / 10^6 = 8388608 / 10^6. -/
  75
  76theorem upquark_sector_params :
  77    B_pow .UpQuark = -1 ∧ r0 .UpQuark = 35 := by
  78  exact ⟨B_pow_UpQuark_eq, r0_UpQuark_eq⟩
  79
  80theorem downquark_sector_params :
  81    B_pow .DownQuark = 23 ∧ r0 .DownQuark = -5 := by
  82  exact ⟨B_pow_DownQuark_eq, r0_DownQuark_eq⟩
  83
  84/-! ## Quark Mass Formula Structural Properties
  85
  86Each quark mass is a specific phi-power divided by a sector-dependent scale.