CascadeParameters
plain-language theorem explainer
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.
Claim. A 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
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 α.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.