Joint smoothness and spatial periodicity for the actual T iterates.

The IsClassicalSol predicate already packages joint smoothness up to the initial time and spatial periodicity. This module exposes those facts as an iteration-indexed API, including the base iterate T 0 = θprev.

theorem AVenhance.Infra.Section4.tIterate_contDiffOn_nonneg {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) {i : ℕ} (hi : i ≤ Nstar β) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T i p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)

Every actual iterate through the budget is jointly smooth on the closed nonnegative-time domain. For positive iterates this is the smoothness field of IsClassicalSol; the base iterate uses the classical previous-scale solution.

theorem AVenhance.Infra.Section4.tIterate_space_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) {i : ℕ} (hi : i ≤ Nstar β) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ (↑⊤) (T i t)

Every nonnegative-time slice of an actual T iterate is spatially smooth.

theorem AVenhance.Infra.Section4.tIterate_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) {i : ℕ} (hi : i ≤ Nstar β) {t : ℝ} (ht : 0 ≤ t) : IsZ2Periodic (T i t)

Spatial periodicity of every actual iterate through the finite iteration budget.

theorem AVenhance.Infra.Section4.terminalT_contDiffOn_nonneg_and_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T (Nstar β) p.1 p.2) (Set.Ici 0 ×ˢ Set.univ) ∧ ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (T (Nstar β) t)

Joint regularity and periodicity of the terminal iterate used as T_{m-1} in the Section 5 residuals.