theorem
proved
proton_relative_error
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Masses.Verification on GitHub at line 308.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
305Note: the integer rung 48 is the closest to the proton mass. The ~3.3%
306overshoot reflects the non-perturbative QCD binding that sits between
307rungs 47 and 48 on the phi-ladder. -/
308theorem proton_relative_error :
309 |proton_binding_pred - m_p_exp| / m_p_exp < 0.035 := by
310 have hb := proton_mass_bounds
311 have hexp_pos : (0 : ℝ) < m_p_exp := by unfold m_p_exp; norm_num
312 rw [div_lt_iff₀ hexp_pos, abs_lt]
313 unfold m_p_exp
314 constructor <;> nlinarith [hb.1, hb.2]
315
316/-! ## Verification Supersedes mass_ladder_assumption
317
318The concrete interval-arithmetic bounds above replace the placeholder
319`mass_ladder_assumption` from `Assumptions.lean`. The following theorem
320provides the direct replacement: the phi-ladder model with geometry-derived
321parameters matches PDG masses without any external assumption. -/
322
323/-- Direct verification that the phi-ladder model matches PDG to stated tolerances.
324 This supersedes `Masses.mass_ladder_assumption`. -/
325theorem phi_ladder_verified :
326 (|electron_pred - m_e_exp| / m_e_exp < 0.003) ∧
327 (|muon_pred - m_mu_exp| / m_mu_exp < 0.04) ∧
328 (|tau_pred - m_tau_exp| / m_tau_exp < 0.03) := by
329 rw [show electron_pred = rs_mass_MeV .Lepton 2 from electron_pred_eq.symm,
330 show muon_pred = rs_mass_MeV .Lepton 13 from muon_pred_eq.symm,
331 show tau_pred = rs_mass_MeV .Lepton 19 from tau_pred_eq.symm]
332 exact ⟨electron_relative_error, muon_relative_error, tau_relative_error⟩
333
334/-! ## Quark Sector — φ-Ladder Structural Predictions
335
336Quark masses use: rs_mass_MeV(UpQuark, r) = 2^(-1) × φ^(-5) × φ^35 × φ^r / 10^6
337 = φ^(30+r) / 2000000 MeV.
338