phi_ladder_verified

formal source

 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
 339For DownQuark: rs_mass_MeV(DownQuark, r) = 2^23 × φ^(-5) × φ^(-5) × φ^r / 10^6
 340                                          = 2^23 × φ^(r-10) / 10^6  MeV.
 341
 342The absolute mass scale requires the gap correction Z, which for quarks involves
 343large integer Z-charges (ZOf_up ≈ 276, ZOf_down ≈ 24 in the RS bridge).
 344The gap-corrected predictions are pending full RSBridge calibration.
 345
 346What IS proved without gap correction:
 347- All quark masses are positive
 348- Within-sector mass ratios follow the φ-ladder (generation spacing)
 349- The up-charm-top spacing φ^11 and φ^6 respectively reproduce correct orders of magnitude
 350-/
 351
 352/-- The up-quark structural mass (UpQuark sector, rung 4, Z=0 gap correction). -/
 353noncomputable def up_quark_pred : ℝ :=
 354  Constants.phi ^ (34 : ℕ) / 2000000
 355