Part I: joint C^∞ regularity of Amnr and HTilde_m on the open half space

The Amnr recursion differentiates in time with the two-sided deriv, so at t = 0 it sees values of T for t < 0. On the open half space (0,∞) × ℝ² everything is unconditional: the seed multiplier, the velocity, its gradient and ∇T_{N*} are all jointly C^∞ there, and the recursion preserves this.

theorem AVenhance.Infra.Section5.Integration.amnrSeedMultiplier_contDiff_top {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (n : ℕ) (j k i p : Fin 2) : ContDiff ℝ (↑⊤) (Section4.amnrSeedMultiplier I hΦ m κ n j k i p)

The primitive seed multiplier is C^∞, with no source-budget restriction.

theorem AVenhance.Infra.Section5.Integration.amnr_contDiffOn_Ioi_top {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (n r : ℕ) (i j k : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => I.Amnr hΦ m κm n (T (Nstar β)) r z.1 z.2 i j k) (Set.Ioi 0 ×ˢ Set.univ)

Joint C^∞ regularity of the actual Amnr tensors on the open half space.