cascade_doubly_exponential_lower
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove the Composition Closure Hypothesis.
- Does not yield an unconditional proof of the Riemann Hypothesis.
- Does not supply an upper bound on defect growth.
- Does not apply when the initial parameter t is non-positive.
- Does not reference the phi-ladder or eight-tick octave.
formal statement (Lean)
138theorem cascade_doubly_exponential_lower {t : ℝ} (_ht : 0 < t) (n : ℕ) :
139 Real.exp ((2 : ℝ) ^ n * t) / 2 - 1 ≤ defectIterate t n := by
proof body
Tactic-mode proof.
140 simp only [defectIterate]
141 have h : Real.exp ((2 : ℝ) ^ n * t) / 2 ≤ Real.cosh ((2 : ℝ) ^ n * t) := by
142 rw [Real.cosh_eq]
143 have hexp : 0 ≤ Real.exp (-((2 : ℝ) ^ n * t)) := Real.exp_nonneg _
144 linarith
145 linarith
146
147/-! ## §5. What remains
148
149The gap between the composition route and unconditional RH is precisely
150the Composition Closure Hypothesis (CCH).
151
152CCH asserts that each iterate of the RCL self-composition corresponds
153to an actual constraint on the carrier budget. This is the RS-native
154version of the `EulerBoundaryBridgeAssumption`.
155
156Potential approaches to proving CCH:
1571. **Explicit formula**: the Guinand-Weil formula connects zeros to primes;
158 the iterated defect should map to prime correlations at scale 2ⁿ
1592. **Hadamard product**: the convergence ∑ 1/|ρ|² < ∞ constrains the
160 collective defect budget; the cascade from one zero may violate it
1613. **Spectral**: the Hilbert-Pólya approach places zeros as eigenvalues;
162 the RCL cascade maps to an operator norm constraint -/
163
164end
165
166end NumberTheory
167end IndisputableMonolith