Public statement.

theorem AVenhance.classical_wellposed (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hper : IsZ2Periodic θ₀) : ∃ (θ : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel φ) κ F θ₀ θ ∧ ∀ (θ' : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel φ) κ F θ₀ θ' → ∀ (t : ℝ), 0 ≤ t → ∀ (x : Homogenization.Vec 2), θ' t x = θ t x

Smooth periodic solvability for smooth forcing (external input of PLAN §0: "parabolic smoothness of θ_m for smooth b_m"): existence, and uniqueness on t ≥ 0 (the class does not constrain t < 0). Makes the hypotheses IsClassicalSol of FILES 34, 35 non-vacuous.