cascade_decreases
plain-language theorem explainer
The cascade mass function decreases strictly with generation index n for positive base mass m0 and scaling α. Researchers modeling fermion hierarchies via Recognition Science's φ-cascade would cite it to justify geometric mass suppression across generations. The proof unfolds the definition and applies strict monotonicity of the real exponential with base phi > 1.
Claim. Let φ > 1 be the golden ratio. For m₀ > 0 and α > 0, the cascade mass m(n) = m₀ φ^{-α n} satisfies m(n+1) < m(n) for every natural number n.
background
In the SM-006 module the fermion mass hierarchy is derived from a φ-cascade in which each generation is suppressed geometrically: m_n ~ m₀ × φ^{-α n}. The cascadeMass function implements exactly this form, with φ fixed by the self-similar fixed point of the forcing chain (T5–T6). Upstream results supply the key inequality 1 < φ (one_lt_phi) together with the electron mass placed on the φ-ladder (m_e = mass_on_rung 2). The module notes that powers φ², φ⁴, φ⁸, φ¹⁶, φ²⁴ already span the observed top-to-electron ratio of order 340 000.
proof idea
The tactic proof introduces n, unfolds cascadeMass, obtains phi > 0 and phi > 1 from Constants, proves the exponent inequality -(α(n+1)) < -(α n) by linarith after Nat.cast, invokes Real.rpow_lt_rpow_of_exponent_lt to obtain the power inequality, and finishes with mul_lt_mul_of_pos_left using positivity of m0.
why it matters
The theorem supplies the monotonicity required for the geometric progression that generates the observed mass hierarchy inside the φ-cascade construction. It anchors the SM-006 derivation that converts the eight-tick octave and D = 3 into large ratios via successive powers of φ. Sibling declarations (koide_is_two_thirds, phi_cascade_from_higgs) rely on this decrease to reach concrete lepton and quark spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.