koide_is_two_thirds
plain-language theorem explainer
The Koide parameter for the three observed charged lepton masses lies within 0.0001 of exactly 2/3. Particle physicists comparing Recognition Science mass predictions to experiment would cite the result when checking consistency with the φ-cascade. The proof is a one-line wrapper that reduces the numerical claim directly to the trivial proposition.
Claim. Let $K$ be the Koide parameter formed from the observed electron, muon and tau masses. Then $|K - 2/3| < 0.0001$.
background
The MassHierarchy module derives the Standard-Model fermion mass hierarchy from Recognition Science’s φ-cascade. Each generation occupies a successive rung on the φ-ladder; the Higgs coupling to successive generations differs by a factor of φ, and mass scales with the square of that coupling, producing geometric ratios φ², φ⁴, … that span the observed range from the electron to the top quark. The module imports the fundamental tick (one RS time quantum) and the rung function that indexes discrete tiers. Upstream lemmas supply the rung definition as a natural-number index and the tick constant as the base time unit.
proof idea
The proof is a one-line wrapper that applies the trivial tactic, treating the numerical closeness of the Koide parameter to 2/3 as an established observational fact.
why it matters
The declaration records the experimental datum that the Koide parameter for charged leptons is within 0.0001 of 2/3, the value the φ-cascade is constructed to reproduce. It anchors the mass-hierarchy claims of the SM-006 section and connects to the eight-tick octave (T7) that fixes the three-generation structure. The result leaves open the derivation of the exact 2/3 value from the Recognition Composition Law or J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.