theorem
proved
top_to_up_ratio
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.QuarkVerification on GitHub at line 141.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
138 rw [← zpow_natCast, ← zpow_add₀ hphi_ne]
139 congr 1
140
141theorem top_to_up_ratio :
142 rs_mass_MeV .UpQuark (r_up "t") / rs_mass_MeV .UpQuark (r_up "u") =
143 Constants.phi ^ (17 : ℕ) := by
144 simp only [r_up, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
145 cube_edges, active_edges_per_tick, D, wallpaper_groups]
146 unfold rs_mass_MeV
147 simp only [B_pow, r0, Anchor.E_passive, Anchor.W, passive_field_edges,
148 cube_edges, active_edges_per_tick, D, wallpaper_groups, A]
149 have hphi := Constants.phi_pos
150 have hphi_ne : Constants.phi ≠ 0 := ne_of_gt hphi
151 field_simp
152 rw [← zpow_natCast, ← zpow_add₀ hphi_ne]
153 congr 1
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