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

QuarkVerificationCert

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)

 157structure QuarkVerificationCert where
 158  rung_spacing_up : r_up "c" - r_up "u" = 11 ∧ r_up "t" - r_up "u" = 17
 159  rung_spacing_down : r_down "s" - r_down "d" = 11 ∧ r_down "b" - r_down "d" = 17
 160  sector_params_up : B_pow .UpQuark = -1 ∧ r0 .UpQuark = 35
 161  sector_params_down : B_pow .DownQuark = 23 ∧ r0 .DownQuark = -5
 162  all_masses_positive : ∀ s r, 0 < rs_mass_MeV s r
 163

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.