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