 181A single record bundling every theorem-grade row of this Phase 0
 182deliverable. -/
 183
 184structure QuarkScoreCardCert where
 185  ZOf_up : ZOf .u = 276 ∧ ZOf .c = 276 ∧ ZOf .t = 276
 186  ZOf_down : ZOf .d = 24 ∧ ZOf .s = 24 ∧ ZOf .b = 24
 187  ZOf_lep : ZOf .e = 1332 ∧ ZOf .mu = 1332 ∧ ZOf .tau = 1332
 188  charm_up_ratio_eq :
 189    Verification.charm_quark_pred / Verification.up_quark_pred =
 190      Constants.phi ^ (11 : ℕ)
 191  top_charm_ratio_eq :
 192    Verification.top_quark_pred / Verification.charm_quark_pred =
 193      Constants.phi ^ (6 : ℕ)
 194  top_in_band : (10000 : ℝ) < Verification.top_quark_pred ∧
 195      Verification.top_quark_pred < 1000000
 196  quark_preds_pos : 0 < Verification.up_quark_pred ∧
 197      0 < Verification.charm_quark_pred ∧ 0 < Verification.top_quark_pred
 198  electron_pct :
 199    |Verification.rs_mass_MeV .Lepton 2 - Verification.m_e_exp| /
 200        Verification.m_e_exp < 0.003
 201  muon_pct :
 202    |Verification.rs_mass_MeV .Lepton 13 - Verification.m_mu_exp| /
 203        Verification.m_mu_exp < 0.04
 204  tau_pct :
 205    |Verification.rs_mass_MeV .Lepton 19 - Verification.m_tau_exp| /
 206        Verification.m_tau_exp < 0.03
 207
 208theorem quarkScoreCardCert_holds : Nonempty QuarkScoreCardCert :=
 209  ⟨{ ZOf_up := ZOf_up_quarks
 210     ZOf_down := ZOf_down_quarks
 211     ZOf_lep := ZOf_charged_leptons
 212     charm_up_ratio_eq := row_charm_up_ratio
 213     top_charm_ratio_eq := row_top_charm_ratio
 214     top_in_band := row_top_quark_in_band

papers checked against this theorem

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