cascade_exponential_growth
The theorem asserts that the n-fold iterated defect under the recognition composition law satisfies d_n(t) ≥ 4^n d_0(t). Researchers pursuing the composition-divergence certificate for the Riemann hypothesis cite it as the exponential amplification step in the cascade. The proof is a one-line wrapper that invokes the exponential lower bound already established for the iterated defect.
claimLet $d_n(t) := cosh(2^n t) - 1$. Then for all real $t$ and natural $n$, $4^n (cosh(t) - 1) ≤ d_n(t)$.
background
The CompositionDivergence module develops an alternate conditional route to the Riemann hypothesis by showing that iterated defects under the zero composition law diverge and violate a finite carrier budget. The defect functional equals J(x) for positive x, where J satisfies the recognition composition law. The iterated defect is defined as defectIterate t n := cosh(2^n t) - 1; for a zeta zero with deviation η = Re(ρ) - 1/2 one sets t = 2η so that d_0 = cosh(2η) - 1 is the base defect and d_n tracks the n-th self-composition.
proof idea
The proof is a one-line wrapper that applies the upstream theorem defectIterate_exponential_lower from ZeroCompositionLaw.
why it matters in Recognition Science
This supplies the exponential growth step in the module's forcing chain: RCL self-composition amplifies defect so that d_n ≥ 4^n d_0, which under the composition closure hypothesis exceeds any finite carrier budget. It sits between the zero composition law and the divergence claims, consistent with J-uniqueness (T5) and the recognition composition law. The module doc notes that the cascade is theoretically stronger than a single defect yet does not reduce the EBBA bridge.
scope and limits
- Does not establish the composition closure hypothesis needed to link divergence to budget violation.
- Does not derive the Riemann hypothesis itself.
- Does not apply when t = 0, where all defects remain zero.
- Does not compare cascade strength to the EBBA bridge.
formal statement (Lean)
132theorem cascade_exponential_growth (t : ℝ) (n : ℕ) :
133 (4 : ℝ) ^ n * defectIterate t 0 ≤ defectIterate t n :=
proof body
Term-mode proof.
134 defectIterate_exponential_lower t n
135
136/-- Doubly-exponential growth: the defect at level n involves
137 cosh(2ⁿ · t), which for t ≠ 0 grows as exp(2ⁿ · |t|)/2. -/