Public statement.

theorem AVenhance.indystepdown (β C₀ : ℝ) : ∃ (C : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (R : ℝ), 0 < R → ∀ (θ₀ : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) θ₀ → IsZ2Periodic θ₀ → Homogenization.MeanZeroOn unitCube θ₀ → IsThetaAnalytic R θ₀ → ∀ (m : ℕ), mTheta0 β I.Λ R ≤ m → m ≤ M → ∀ (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ m)) (I.kappaSeq κ M m) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θm → IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → (∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θm t x - θprev t x) + √(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θm s) x - spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s) x) ≤ C * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)) ∧ (6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → |(I.kappaSeq κ M m * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θm s) x) - I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x| ≤ C * epsilon β I.Λ (m - 1) ^ delta β * (I.kappaSeq κ M (m - 1) * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))

Step-down estimate: p.indystepdown (8026-8062). Binder order and constants as in bigbound. Conclusions: e.homogenization.m (for every t ∈ [0,1], the L^∞_tL²_x norm plus the κ_m^{1/2}‖∇·‖_{L²_{t,x}} term, ∇θ_m and ∇θTilde_m the classical gradients) and e.tildethetam.energy.diss in cross-multiplied form |κ_m D_m - κ_{m-1} D_{m-1}| ≤ Cε_{m-1}^δ κ_{m-1} D_{m-1}, D_j = ‖∇θ_j‖²_{L²((0,1)×𝕋²)} (equal to the printed ratio bound when D_{m-1} > 0, and true, rather than 0/0, for θ₀ = 0). Conjunct (ii) is asserted only for 6/5 ≤ β and at later levels ε_{m-1}^{1+γ/2-δ} ≤ R.