def
definition
res_bottom
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QuarkMasses on GitHub at line 65.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
62
63/-- Ideal residues on the Phi-ladder. -/
64def res_top : ℚ := 23 / 4
65def res_bottom : ℚ := res_top - step_top_bottom
66def res_charm : ℚ := res_bottom - step_bottom_charm
67def res_strange : ℚ := res_charm - step_charm_strange
68def res_down : ℚ := -64 / 4
69def res_up : ℚ := -71 / 4
70
71/-- **THEOREM: Quark Residues Match Steps**
72 Verifies that the residues derived from steps match the ideal positions. -/
73theorem residues_match_steps :
74 res_bottom = -2 ∧ res_charm = -4.5 ∧ res_strange = -10 := by
75 constructor
76 · unfold res_bottom res_top step_top_bottom; norm_num
77 constructor
78 · unfold res_charm res_bottom res_top step_top_bottom step_bottom_charm; norm_num
79 · unfold res_strange res_charm res_bottom res_top step_top_bottom step_bottom_charm step_charm_strange; norm_num
80
81/-!
82## Quark mass matching (hypothesis lane)
83
84The quarter-ladder quark module is an **experimental hypothesis lane** (Gap 6).
85We keep the forward formula (`predicted_mass`) in Lean, but treat the numerical
86match-to-PDG statements as explicit empirical hypotheses until a fully audited,
87parameter-free reconciliation is completed.
88-/
89
90/-- Predicted Mass Formula: m = m_struct * phi^res. -/
91noncomputable def predicted_mass (res : ℚ) : ℝ :=
92 electron_structural_mass * (phi ^ (res : ℝ))
93
94def H_top_mass_match : Prop :=
95 abs (predicted_mass res_top - mass_top_exp) / mass_top_exp < 0.0005