Iterates TSource Upgrade

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_T_source_upgrade_of_diffusivity_and_flow {β : ℝ} (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) (hm : 2 ≤ m) (hκm : 0 < κm) (hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) (hflowp : ∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t)) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) {c Ck K Cflow Cmean Rflow Cθ Rθ C₀ N : ℝ} (hN : 0 < N) (hc : 0 < c) (hCk : 0 ≤ Ck) (hK : 0 ≤ K) (hCf : 0 ≤ Cflow) (hCm : 0 ≤ Cmean) (hRf : 256 ≤ Rflow) (hRθ : 0 < Rθ) (hlower : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ κprev) (hupper : κprev ≤ Ck * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β))) (hC₀ : iterateSourceConstant (iterateBudgetUniversalConstant K Ck c (2 ^ (-25)) Cflow Cmean) Rflow Cθ ≤ C₀) (hradius : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ) (hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * C₀ ^ 3)⁻¹) (hKm : ∀ (t : ℝ) (j k : Fin 2), |I.Kmat κm m t j k| ≤ K * κprev) (hmean : ∀ (j k : Fin 2), |(timeAvgMat (I.Kmat κm m) - κprev • 1) j k| ≤ κprev * Cmean * epsilon β I.Λ (m - 1) ^ (2 * delta β)) (hzero : ∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (j k : Fin 2), |(I.flowGrad hΦ m l t x - 1) j k| ≤ Cflow * epsilon β I.Λ (m - 1) ^ (2 * delta β)) (hpositive : ∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (p : List (Fin 2)), 1 ≤ p.length → ∀ (j k : Fin 2), |iterateSpatialWord p (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) j k) x| ≤ Cflow * ↑p.length.factorial * (Rflow / epsilon β I.Λ (m - 1)) ^ p.length) (hκscale : |κm| ≤ κprev) (hbase : iterateCoordinateEnergyProfile θprev κprev N (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0) : √κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (T (Nstar β) t)) ≤ N * (1 + C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * ↑(Nstar β) * ↑(2 * Nstar β).factorial) ∧ ∀ (v w : List (Fin 2)), v.length = w.length → 1 ≤ v.length → ∀ (s : ℝ), 0 ≤ s → s ≤ 1 → √(l2NormSq (iterateSpatialWord v (T (Nstar β) s))) + √κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (T (Nstar β) t))) ≤ N * 4 ^ Nstar β * ↑(2 * Nstar β).factorial * ↑v.length.factorial * (4 * C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) ^ v.length

Corrected positive-order l.Tm.reg.upgrade under the printed radius and smallness conditions, with abstract amplitude and a gradient-only zero branch.