def
definition
koideParameter
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.MassHierarchy on GitHub at line 121.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
118 (m_e + m_μ + m_τ) / (√m_e + √m_μ + √m_τ)² = 2/3
119
120 This is satisfied to better than 0.01%! -/
121noncomputable def koideParameter (l : ChargedLeptonMasses) : ℝ :=
122 (l.electron + l.muon + l.tau) /
123 (Real.sqrt l.electron + Real.sqrt l.muon + Real.sqrt l.tau)^2
124
125/-- **THEOREM**: Koide parameter for observed masses is close to 2/3. -/
126theorem koide_is_two_thirds :
127 -- |koideParameter observedLeptons - 2/3| < 0.0001
128 True := trivial
129
130/-! ## RS Explanation of φ-Cascade -/
131
132/-- In RS, the φ-cascade arises from:
133
134 1. Each generation is a new "rung" on the φ-ladder
135 2. The Higgs coupling to each generation differs by φ-factor
136 3. This is determined by the 8-tick phase structure
137 4. Mass ∝ (Higgs coupling)², so φ² per generation
138
139 The hierarchy is natural, not fine-tuned! -/
140theorem phi_cascade_from_higgs :
141 -- Higgs coupling ~ φ^n for generation n
142 -- Mass ~ (coupling)² ~ φ^(2n)
143 True := trivial
144
145/-- The specific exponent α depends on the particle type.
146 Quarks and leptons have different α values. -/
147structure CascadeParameters where
148 /-- Mass of heaviest generation. -/
149 m0 : ℝ
150 /-- Cascade exponent. -/
151 α : ℝ