def
definition
m_s_exp
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.QuarkVerification on GitHub at line 49.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
46
47def m_u_exp : ℝ := 2.16
48def m_d_exp : ℝ := 4.70
49def m_s_exp : ℝ := 93.5
50def m_c_exp : ℝ := 1270
51def m_b_exp : ℝ := 4180
52def m_t_exp : ℝ := 172500
53
54/-! ## Rung Integer Verification -/
55
56theorem r_up_values : r_up "u" = 4 ∧ r_up "c" = 15 ∧ r_up "t" = 21 := by
57 simp only [r_up, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
58 cube_edges, active_edges_per_tick, D, wallpaper_groups]
59 omega
60
61theorem r_down_values : r_down "d" = 4 ∧ r_down "s" = 15 ∧ r_down "b" = 21 := by
62 simp only [r_down, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
63 cube_edges, active_edges_per_tick, D, wallpaper_groups]
64 omega
65
66/-! ## Sector Parameter Verification
67
68The up-quark sector has B_pow = -1, r0 = 35.
69Effective exponent: -5 + 35 + r = 30 + r.
70Scale: 2^(-1) / 10^6 = 1 / (2 × 10^6).
71
72The down-quark sector has B_pow = 23, r0 = -5.
73Effective exponent: -5 + (-5) + r = -10 + r.
74Scale: 2^23 / 10^6 = 8388608 / 10^6. -/
75
76theorem upquark_sector_params :
77 B_pow .UpQuark = -1 ∧ r0 .UpQuark = 35 := by
78 exact ⟨B_pow_UpQuark_eq, r0_UpQuark_eq⟩
79