pith. machine review for the scientific record. sign in
structure definition def or abbrev

QuarkScoreCardCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.