def
definition
up_quark_pred
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.Verification on GitHub at line 353.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
350-/
351
352/-- The up-quark structural mass (UpQuark sector, rung 4, Z=0 gap correction). -/
353noncomputable def up_quark_pred : ℝ :=
354 Constants.phi ^ (34 : ℕ) / 2000000
355
356/-- The charm-quark structural mass (UpQuark sector, rung 15). -/
357noncomputable def charm_quark_pred : ℝ :=
358 Constants.phi ^ (45 : ℕ) / 2000000
359
360/-- The top-quark structural mass (UpQuark sector, rung 21). -/
361noncomputable def top_quark_pred : ℝ :=
362 Constants.phi ^ (51 : ℕ) / 2000000
363
364/-- All structural quark mass predictions are positive. -/
365theorem quark_preds_pos :
366 0 < up_quark_pred ∧ 0 < charm_quark_pred ∧ 0 < top_quark_pred := by
367 unfold up_quark_pred charm_quark_pred top_quark_pred
368 refine ⟨div_pos (pow_pos Constants.phi_pos _) (by norm_num),
369 div_pos (pow_pos Constants.phi_pos _) (by norm_num),
370 div_pos (pow_pos Constants.phi_pos _) (by norm_num)⟩
371
372/-- The charm/up ratio equals φ^11 exactly (11-rung generation gap). -/
373theorem charm_up_ratio : charm_quark_pred / up_quark_pred = Constants.phi ^ (11 : ℕ) := by
374 unfold charm_quark_pred up_quark_pred
375 have hpos : (0 : ℝ) < Constants.phi ^ (34 : ℕ) / 2000000 :=
376 div_pos (pow_pos Constants.phi_pos _) (by norm_num)
377 field_simp [ne_of_gt hpos]
378
379/-- The top/charm ratio equals φ^6 exactly (6-rung gap). -/
380theorem top_charm_ratio : top_quark_pred / charm_quark_pred = Constants.phi ^ (6 : ℕ) := by
381 unfold top_quark_pred charm_quark_pred
382 have hpos : (0 : ℝ) < Constants.phi ^ (45 : ℕ) / 2000000 :=
383 div_pos (pow_pos Constants.phi_pos _) (by norm_num)