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