composition_cascade_stronger_than_single_defect
The iterated defect under repeated RCL self-composition is monotonically nondecreasing for any nonzero deviation parameter t. Researchers constructing alternate RH certificates via composition divergence would cite this to show the cascade produces strictly more cost values than a single-defect argument. The proof is a direct one-line application of the defectIterate monotonicity lemma.
claimLet $d_n(t) := 2^n t$ and define the iterated defect by $d_n(t) = 2^n t - 1$. For every real $t$ with $t ≠ 0$ and every natural number $n$, the base defect satisfies $d_0(t) ≤ d_n(t)$.
background
The defect iteration function is defined as defectIterate t n := cosh(2^n · t) - 1, with the base case d_0(t) = cosh(t) - 1 recovered when n = 0. This arises directly from the Recognition Composition Law applied to an off-critical zero whose deviation parameter is t = 2η, where η = Re(ρ) - 1/2. The module develops an alternate conditional route to the Riemann Hypothesis by showing that iterated defects diverge and must eventually violate any finite carrier budget under the Composition Closure Hypothesis.
proof idea
The proof is a one-line wrapper that applies the upstream defectIterate_mono theorem to the supplied hypotheses ht and n.
why it matters in Recognition Science
This monotonicity result underpins the module's claim that the composition route is strictly stronger than any single-defect argument, because the RCL generates infinitely many successively larger cost values from one off-critical zero. It fills the step in the forcing chain that converts the recurrence d_{n+1} = 2 d_n (d_n + 2) into the exponential lower bound d_n ≥ 4^n d_0, which is then used to reach the carrier-budget violation. No downstream theorems are recorded yet, but the result directly supports the Composition Closure Hypothesis stated in the module documentation.
scope and limits
- Does not prove the Composition Closure Hypothesis.
- Does not link iterated defects to the annular carrier budget.
- Does not establish the Riemann Hypothesis.
- Does not supply the exponential growth rate; that is handled by a separate lemma.
formal statement (Lean)
126theorem composition_cascade_stronger_than_single_defect
127 {t : ℝ} (ht : t ≠ 0) (n : ℕ) :
128 defectIterate t 0 ≤ defectIterate t n :=
proof body
Term-mode proof.
129 defectIterate_mono ht n
130
131/-- The cascade grows at least as fast as 4ⁿ · d₀. -/