`quark_verification_cert_exists`

proved

show as: view math explainer →

module: IndisputableMonolith.Masses.QuarkVerification
domain: Masses
line: 164 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.QuarkVerification on GitHub at line 164.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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

papers checked against this theorem

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