bottom_mass_pos

formal source

  90theorem strange_mass_pos : 0 < fermionMass .strange :=
  91  predict_mass_pos _ _ _
  92
  93theorem bottom_mass_pos : 0 < fermionMass .bottom :=
  94  predict_mass_pos _ _ _
  95
  96theorem all_fermion_masses_pos : ∀ f : Fermion, 0 < fermionMass f := by
  97  intro f; cases f <;> exact predict_mass_pos _ _ _
  98
  99/-! ## Generation Structure: φ-Scaling Between Generations -/
 100
 101theorem muon_rung_minus_electron_rung :
 102    r_lepton "mu" - r_lepton "e" = 11 := by
 103  simp only [r_lepton, tau, Anchor.E_passive, passive_field_edges,
 104             cube_edges, active_edges_per_tick, D, wallpaper_groups]
 105  norm_num
 106
 107theorem tauon_rung_minus_electron_rung :
 108    r_lepton "tau" - r_lepton "e" = 17 := by
 109  simp only [r_lepton, tau, Anchor.W, Anchor.E_passive, passive_field_edges,
 110             cube_edges, active_edges_per_tick, D, wallpaper_groups]
 111  norm_num
 112
 113/-! ## PDG Experimental Mass Values (MeV/c²)
 114
 115These are the PDG 2024 central values. RS predicts masses in units
 116of E_coh (≈ 0.0901 eV), so comparison requires the calibration:
 117
 118  m_predicted [eV] = fermionMass(f) × E_coh_eV
 119
 120where E_coh_eV ≈ φ⁻⁵ eV ≈ 0.0901 eV.
 121
 122| Particle | PDG Mass (MeV) | RS Rung | RS Sector |
 123|----------|---------------|---------|-----------|