Proof of stream-function estimates. The exponent-specific construction below uses one admissible exponent to choose the limit field; uniqueness of pointwise limits identifies every other exponent's witness with that field.

theorem AVenhance.Proofs.limit_field_regular (β : ℝ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∃ (φ : ℝ → Homogenization.Vec 2 → ℝ), (∀ (t : ℝ) (x : Homogenization.Vec 2), Filter.Tendsto (fun (M : ℕ) => Φ M t x) Filter.atTop (nhds (φ t x))) ∧ (∀ (M : ℕ) (t : ℝ) (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ C * epsilon β I.Λ (M + 1) ^ β) ∧ (∀ (t : ℝ), Differentiable ℝ (φ t)) ∧ TendstoUniformlyOn (fun (M : ℕ) (p : ℝ × Homogenization.Vec 2) => streamVel (Φ M) p.1 p.2) (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) Filter.atTop (Set.Icc 0 1 ×ˢ Set.univ) ∧ ∀ (α : ℝ), 0 < α → α < β - 1 → IsHolderClass α (streamVel φ) ∧ IsDivFree (streamVel φ)

Stream-function estimates proof. Its statement is identical to AVenhance.limit_field_regular; the statement file is not imported.