cascade_exponential_growth

formal source

 129  defectIterate_mono ht n
 130
 131/-- The cascade grows at least as fast as 4ⁿ · d₀. -/
 132theorem cascade_exponential_growth (t : ℝ) (n : ℕ) :
 133    (4 : ℝ) ^ n * defectIterate t 0 ≤ defectIterate t n :=
 134  defectIterate_exponential_lower t n
 135
 136/-- Doubly-exponential growth: the defect at level n involves
 137    cosh(2ⁿ · t), which for t ≠ 0 grows as exp(2ⁿ · |t|)/2. -/
 138theorem cascade_doubly_exponential_lower {t : ℝ} (_ht : 0 < t) (n : ℕ) :
 139    Real.exp ((2 : ℝ) ^ n * t) / 2 - 1 ≤ defectIterate t n := by
 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 -/