leptonParams
plain-language theorem explainer
Fitted parameters for charged leptons supply the heaviest mass and cascade exponent in the Recognition Science mass hierarchy model. Researchers deriving fermion masses from the φ-cascade would cite these values to compute generation ratios. The definition constructs the record directly from the tau mass and an approximate fit for the exponent.
Claim. The cascade parameters for charged leptons are defined by the heaviest generation mass $m_0 = 1.777$, the exponent $α = 4.5$, and the particle type string ``charged leptons''.
background
The module derives the Standard Model fermion mass hierarchy from the φ-cascade. Each generation differs by a factor governed by powers of φ, with three generations arising from the eight-tick octave (period 2³). The structure CascadeParameters holds three fields: m0 as the mass of the heaviest generation, α as the cascade exponent (particle-type dependent), and particle as a descriptive string. Upstream results include the fundamental tick as the RS time quantum and the tau anchor supplying the generation torsion values 0, 11, and 17.
proof idea
The definition is a direct record literal that assigns the tau mass to m0 and an approximate numerical fit to α.
why it matters
This definition supplies the lepton-specific inputs for the φ-cascade mass formula, supporting the overall derivation of the fermion hierarchy from the eight-tick structure. It fills the SM-006 section by providing concrete values that span observed mass ratios via geometric progression in φ powers. The parent construction appears in sibling cascade functions that apply these parameters to generate the full lepton spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.