observedLeptons
plain-language theorem explainer
The definition records the measured masses of the electron, muon, and tau lepton in GeV units for use in Recognition Science calculations. Particle physicists working on mass hierarchies would cite these values when testing φ-cascade predictions. It consists of a direct assignment of the experimental numbers with no derivation steps.
Claim. The observed charged lepton masses satisfy $m_e = 0.000511$ GeV, $m_μ = 0.1057$ GeV, $m_τ = 1.777$ GeV.
background
The module develops the claim that the fermion mass hierarchy arises from a φ-cascade, where each generation differs by factors of φ² or φ³ and three generations follow from the eight-tick structure. The charged lepton mass structure packages the three charged lepton masses in GeV to enable direct comparison with cascade predictions. Upstream, the generation torsion definition encodes τ(0) = 0, τ(1) = 11, τ(2) = 17 as the representation-independent foundation.
proof idea
This is a definition that directly assigns the experimentally measured values to the fields of the charged lepton mass structure.
why it matters
This supplies the concrete data for the downstream theorem verifying that the Koide parameter for these masses is close to 2/3. It implements the input for the φ-cascade analysis in the mass hierarchy module, linking to the eight-tick octave. The definition closes the gap between abstract φ-ladder predictions and observed lepton masses, supporting the proposition on fermion masses from first principles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.