theorem
proved
term proof
tauon_rung_minus_electron_rung
show as:
view Lean formalization →
formal statement (Lean)
107theorem tauon_rung_minus_electron_rung :
108 r_lepton "tau" - r_lepton "e" = 17 := by
proof body
Term-mode proof.
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|----------|---------------|---------|-----------|
124| e | 0.511 | 2 | Lepton |
125| μ | 105.66 | 13 | Lepton |
126| τ | 1776.9 | 19 | Lepton |
127| u | 2.16 | 4 | UpQuark |
128| c | 1270 | 15 | UpQuark |
129| t | 172760 | 21 | UpQuark |
130| d | 4.67 | 4 | DownQuark |
131| s | 93.4 | 15 | DownQuark |
132| b | 4180 | 21 | DownQuark |
133
134## Mass Ratios (More Meaningful Than Absolute Masses)
135
136The φ-ladder predicts specific mass ratios between generations:
137- m_μ/m_e ≈ φ¹¹ ≈ 199.0 (experimental: 206.8)
138- m_τ/m_e ≈ φ¹⁷ ≈ 3571 (experimental: 3477)
139- m_c/m_u ≈ φ¹¹ ≈ 199.0 × gap_correction (experimental: ~588)
140- m_t/m_u ≈ φ¹⁷ ≈ 3571 × gap_correction (experimental: ~80000)
141
142The lepton ratios agree to ~4-5%. Quark ratios require gap corrections. -/
143