Conditional assembly of the integer-horizon Galerkin limits into the classical solution operator.

theorem AVenhance.Infra.Classical.classicalGalerkinIntegerHorizonFamily_classical_wellposed (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (hsmooth : ∀ (N : ℕ), 0 < N → ContDiffOn ℝ (↑⊤) (Function.uncurry (classicalGalerkinIntegerHorizonFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per N)) (Set.Icc 0 ↑N ×ˢ Set.univ)) : ∃ (θ : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel φ) κ F θ₀ θ ∧ ∀ (θ' : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel φ) κ F θ₀ θ' → ∀ (t : ℝ), 0 ≤ t → ∀ (x : Homogenization.Vec 2), θ' t x = θ t x

Once each integer-horizon limit is jointly smooth on its closed slab, the compatible Galerkin family gives the exact classical existence-and-uniqueness conclusion. The smoothness premise is a separate regularity obligation discharged by the limit-regularity modules.