CascadeParameters
CascadeParameters bundles the heaviest-generation mass m0, the cascade exponent α, and a particle-type string to parameterize the geometric φ-cascade that produces the observed fermion mass ratios. Modelers fitting lepton or quark spectra within Recognition Science would cite this structure when constructing explicit generation ladders. It is introduced as a plain structure definition whose three fields carry no proof obligations.
claimA structure whose fields are a real number $m_0$ (mass of the heaviest generation), a real number $α$ (cascade exponent that depends on particle type), and a string (particle type).
background
The module SM-006 derives the Standard Model fermion mass hierarchy from Recognition Science's φ-cascade, where each generation differs by factors of φ² or φ³ and the overall span reaches 10^5 from geometric progression. Upstream, SpectralEmergence.of supplies the structural origin of exactly three generations (from Q₃ face-pair count) together with 24 chiral fermion flavors, while PhiForcingDerived.of and LedgerFactorization.of calibrate the J-cost and ledger factors that underlie the mass scaling; Constants.RSNativeUnits.Mass simply aliases ℝ for mass values. The local setting is the eight-tick octave (T7) that forces D = 3 and the discrete φ-tiers already present in NucleosynthesisTiers.of.
proof idea
The declaration is a direct structure definition; no lemmas are applied and no tactics are used.
why it matters in Recognition Science
CascadeParameters supplies the parameter record consumed by leptonParams (and analogous quark definitions) that realize the module's core claim of a φ-cascade mass hierarchy. It therefore sits inside the T7 eight-tick octave and the three-generation count from SpectralEmergence.of, directly supporting the paper proposition on fermion masses from first principles. The structure remains open to later insertion of explicit φ-dependence for α.
scope and limits
- Does not assign numerical values to m0 or α.
- Does not enforce that α must be a multiple of log φ.
- Does not derive the mass formula m_n ~ m0 × φ^(-α n).
- Does not connect the parameters to the Berry creation threshold or Z_cf.
formal statement (Lean)
147structure CascadeParameters where
148 /-- Mass of heaviest generation. -/
149 m0 : ℝ
150 /-- Cascade exponent. -/
151 α : ℝ
152 /-- Particle type. -/
153 particle : String
154
155/-- Fitted parameters for charged leptons. -/