structure
definition
QuarkVerificationCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Masses.QuarkVerification on GitHub at line 157.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
154
155/-! ## Certificate -/
156
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
164theorem quark_verification_cert_exists : Nonempty QuarkVerificationCert :=
165 ⟨{ rung_spacing_up := up_generation_spacing
166 rung_spacing_down := down_generation_spacing
167 sector_params_up := upquark_sector_params
168 sector_params_down := downquark_sector_params
169 all_masses_positive := quark_mass_positive }⟩
170
171end
172
173end IndisputableMonolith.Masses.QuarkVerification