cascade_doubly_exponential_lower
plain-language theorem explainer
Analysts pursuing the composition-law certificate for the Riemann Hypothesis cite this bound to quantify how iterated defects diverge doubly exponentially. For positive initial parameter t and natural number n the n-fold defect satisfies exp(2^n t)/2 minus one as a lower bound. The short tactic proof unfolds the iterated defect definition then verifies the elementary comparison of the exponential against the hyperbolic cosine via its explicit formula and linear arithmetic.
Claim. For all real numbers $t > 0$ and natural numbers $n$, let $x = 2^n t$. Then $e^x/2 - 1$ is a lower bound for the defect obtained after $n$ iterations of the Recognition Composition Law applied to initial parameter $t$.
background
The module develops an alternate conditional route to the Riemann Hypothesis by showing that repeated self-composition under the Recognition Composition Law produces defects that outrun any finite carrier budget. The iterated defect is realized by the map whose n-fold application yields cosh(2^n t) - 1; this expression satisfies the recurrence d_{n+1} = 2 d_n (d_n + 2) and therefore grows as exp(2^n |t|)/2 for large n. The local theoretical setting is the four-step chain: RCL forces J, J-symmetry encodes the functional equation, self-composition amplifies defect, and divergent defect violates the annular carrier cost bound once the Composition Closure Hypothesis is assumed.
proof idea
The tactic proof first simplifies the definition of the iterated defect to expose the cosh expression. It then proves the auxiliary inequality exp(x)/2 ≤ cosh(x) for x = 2^n t by rewriting cosh via its exponential definition, invoking non-negativity of the negative exponential, and applying linear arithmetic. A final linear arithmetic step subtracts one from both sides.
why it matters
The lemma supplies the explicit doubly-exponential lower bound required for the divergence step inside the composition route to the Riemann Hypothesis. It shows that any positive initial parameter produces defects that exceed every fixed carrier budget for sufficiently large n, thereby supporting the claim that off-critical zeros are incompatible with finite annular cost once the Composition Closure Hypothesis is granted. The result sits inside the alternate RH certificate of this module and complements the zero composition law; the remaining open question is a proof of the Composition Closure Hypothesis itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.