 250
 251/-! ## Summary Certificate -/
 252
 253structure MassVerificationCert where
 254  electron_in_range : (0.5098 : ℝ) < electron_pred ∧ electron_pred < 0.5102
 255  muon_in_range : (101.49 : ℝ) < muon_pred ∧ muon_pred < 101.57
 256  tau_in_range : (1821 : ℝ) < tau_pred ∧ tau_pred < 1823
 257  electron_pct : |rs_mass_MeV .Lepton 2 - m_e_exp| / m_e_exp < 0.003
 258  muon_pct : |rs_mass_MeV .Lepton 13 - m_mu_exp| / m_mu_exp < 0.04
 259  tau_pct : |rs_mass_MeV .Lepton 19 - m_tau_exp| / m_tau_exp < 0.03
 260  mu_e_ratio_pct : |Constants.phi ^ (11 : ℕ) - ratio_mu_e_exp| / ratio_mu_e_exp < 0.04
 261  tau_e_ratio_pct : |Constants.phi ^ (17 : ℕ) - ratio_tau_e_exp| / ratio_tau_e_exp < 0.03
 262
 263theorem mass_verification_cert_exists : Nonempty MassVerificationCert :=
 264  ⟨{ electron_in_range := electron_mass_bounds
 265     muon_in_range := muon_mass_bounds
 266     tau_in_range := tau_mass_bounds
 267     electron_pct := electron_relative_error
 268     muon_pct := muon_relative_error
 269     tau_pct := tau_relative_error
 270     mu_e_ratio_pct := muon_electron_ratio_error
 271     tau_e_ratio_pct := tau_electron_ratio_error }⟩
 272
 273/-! ## Proton Mass Verification
 274
 275The proton mass is dominated by QCD binding energy (~99%). In the
 276phi-ladder framework, the binding energy sits at `E_coh × φ^r_binding`
 277where `r_binding = 48` is the nearest integer rung (binding exponent 43).
 278
 279The total proton mass ≈ `φ^43 / 10^6` MeV (valence quarks contribute <0.001%). -/
 280
 281def m_p_exp : ℝ := 938.272
 282
 283noncomputable def proton_binding_pred : ℝ := Constants.phi ^ (43 : ℕ) / 1000000

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.