proton_relative_error

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