pith. machine review for the scientific record. sign in
def

koideParameter

definition
show as:
view math explainer →
module
IndisputableMonolith.Physics.MassHierarchy
domain
Physics
line
121 · github
papers citing
none yet

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

A cached Ask Recognition explainer exists for this declaration.

open explainer

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  α : ℝ