Statement file: l_recurse (Section3). This file contains exactly one declaration of the formalization's public statement surface.

theorem AVenhance.l_recurse (β C₀ : ℝ) : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ c < C ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → (∀ (m : ℕ), 1 ≤ m → m < M → c * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β)) ≤ I.kappaAt κ m (M - m) ∧ I.kappaAt κ m (M - m) ≤ C * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β))) ∧ ∀ (m : ℕ), 2 ≤ m → m < M → c * epsilon β I.Λ (m - 1) ^ (4 * delta β) ≤ epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) ∧ epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) ≤ C * epsilon β I.Λ (m - 1) ^ (4 * delta β)

l.recurse. Constants c < C depend only on β (and the three cutoff-constant bounds C₀), placed before I, Λ = I.Λ, κ, M, m. Ranges: see the errata (e.kappam.bound for m ∈ {1,…,M-1}; e.exprat.bound for m ∈ {2,…,M-1}). Corrected form: the exponent in e.exprat.bound is 4δ, not the printed 2δ (the identity at source line 3715 gives 8δ, not 4δ).