The telescoped classical chain

chain_data: for a datum with mTheta0 R ≤ m₀ + 1, a chain topped at any κ ∈ permittedInterval M (m₀ < M), the classical iterates exist at levels m₀, …, M and ‖θ_M(t) − θ_{m₀}(t)‖ ≤ 2 C₈ ε_{m₀}^δ ‖θ₀‖.

theorem AVenhance.Infra.FullTheorem.NoSel.eps_succ_half {β : ℝ} (I : Ingredients β) {s : ℝ} (hs : 0 < s) {k : ℕ} (hk : 1 ≤ k) (hg : (1 + Ingredients.supergeoConstant β) ^ s * (↑I.Λ)⁻¹ ^ ((q β - 1) * s) ≤ 1 / 2) : epsilon β I.Λ (k + 1) ^ s ≤ epsilon β I.Λ k ^ s / 2

ε_{k+1}^δ ≤ ½ ε_k^δ for k ≥ 1 once Λ is large.

theorem AVenhance.Infra.FullTheorem.NoSel.chain_data (β C₀ : ℝ) : ∃ (C₈ : ℝ) (Λc : ℝ), 0 ≤ C₈ ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → Λc ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∀ (κ : ℝ) (M : ℕ), κ ∈ permittedInterval β I.Λ M → ∀ (m₀ : ℕ), 2 ≤ m₀ → m₀ < M → ∀ (R : ℝ), 0 < R → ∀ (θ₀ : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) θ₀ → IsZ2Periodic θ₀ → Homogenization.MeanZeroOn unitCube θ₀ → IsThetaAnalytic R θ₀ → mTheta0 β I.Λ R ≤ m₀ + 1 → (∀ (j : ℕ), m₀ ≤ j → j ≤ M → 0 < I.kappaSeq κ M j) ∧ ∃ (θs : ℕ → ℝ → Homogenization.Vec 2 → ℝ), (∀ (j : ℕ), m₀ ≤ j → j ≤ M → IsClassicalSol (streamVel (Φ j)) (I.kappaSeq κ M j) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ (θs j)) ∧ ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θs M t x - θs m₀ t x) ≤ 2 * C₈ * epsilon β I.Λ m₀ ^ delta β * √(l2NormSq θ₀)