koideParameter
plain-language theorem explainer
The Koide parameter is defined as the ratio of summed charged lepton masses to the square of the summed square roots of those masses. Particle physicists examining lepton mass patterns cite this when testing the empirical near-2/3 relation against data. The definition is a direct algebraic expression with no lemmas or reductions required.
Claim. For a triple of charged lepton masses $(m_e, m_μ, m_τ)$, the Koide parameter is $(m_e + m_μ + m_τ) / (√m_e + √m_μ + √m_τ)^2$.
background
The module derives fermion mass hierarchy from the φ-cascade in Recognition Science, where each generation differs by factors of φ² or φ³ and three generations arise from the eight-tick structure. ChargedLeptonMasses is the structure holding the three charged lepton masses in GeV units. The local theoretical setting is SM-006, which targets derivation of the observed hierarchy (top quark ~173 GeV versus electron ~0.5 MeV) from geometric progressions in φ powers.
proof idea
This is a one-line wrapper that directly implements the algebraic definition of the Koide parameter using the three mass components from the ChargedLeptonMasses structure.
why it matters
This definition supplies the Koide parameter to the downstream theorem koide_is_two_thirds, which asserts the parameter lies close to 2/3 for observed masses. It fills the empirical relation slot inside the φ-cascade account of mass hierarchy, where φ powers span the observed range. It touches the open question of why the relation holds to 0.01% precision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.