Public statement.

theorem AVenhance.lebron_step (β C₀ : ℝ) : ∃ (μ : ℝ) (C : ℝ), 0 < μ ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), 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 → ℝ), 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 → HolderTimeL2Le μ (C * epsilon β I.Λ (m - 1) ^ (delta β / 2) * √(l2NormSq θ₀ + gradNormSq (spaceGrad θ₀))) fun (t : ℝ) (x : Homogenization.Vec 2) => θm t x - θprev t x

Remark 5.3 of the paper (r.LeBron) (e.continuous.indeed, 9041-9051), in the context of p.indystepdown (premises exactly those of step-down minus the iterate witness T): ‖θ_m − θ_{m−1}‖_{C^{0,μ}([0,1];L²)} ≤ C ε_{m−1}^{δ/2} ‖θ₀‖_{H¹} with μ, C depending only on β (and the cutoff bound C₀).