Proof bridge for classical well-posedness. The Galerkin limit and nested-horizon compatibility are already constructed in Infra.Classical; only joint smoothness of each closed integer-horizon limit remains an explicit input.

theorem AVenhance.Proofs.classical_wellposed_of_horizon_limit_regularity (φ : ℝ → 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 θ₀) (hLimitSmooth : ∀ (N : ℕ), 0 < N → ContDiffOn ℝ (↑⊤) (Function.uncurry (Infra.Classical.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

Classical well-posedness from the committed integer-horizon Galerkin limits, conditional only on the outstanding joint smoothness of those limits on their closed slabs.

The regularity hypothesis is stated on the actual family used by the existing limit construction. The horizon agreement needed to glue the family is proved by classicalGalerkinIntegerHorizonFamily_consistent, using the limit regularity bridge.

theorem AVenhance.Proofs.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 ℝ (↑⊤) θ₀) (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

Exact proof for classical well-posedness. The integer-horizon limits are jointly smooth by the all-order Galerkin word induction, including both time endpoints.