Stream-regularity coefficient bounds in the first-derivative drift estimate.

theorem AVenhance.Infra.Section4.IteratesStreamPhysical.iterate_A3_high_order_fraction_le_one {n : ℕ} (hn : 2 ≤ n) : (↑n + 2) ^ 2 / (↑n + 1) ^ 3 ≤ 1

theorem AVenhance.Infra.Section4.iterate_stream_word_factorial_bound_of_A3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (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))) (t : ℝ) (w : List (Fin 2)) (hw : 2 ≤ w.length) (x : Homogenization.Vec 2) : |iterateSpatialWord w (Φ (m - 1) t) x| ≤ 2 ^ 5 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2 * ↑w.length.factorial * (2 ^ 8 * (epsilon β I.Λ (m - 1))⁻¹) ^ w.length / (↑w.length + 1) ^ 2

All high spatial stream jets obey the source factorial profile under the stream-regularity premise. This is the coefficient profile used in the drift sum.

theorem AVenhance.Infra.Section4.iterate_stream_second_jet_bound_of_A3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (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))) (t : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2) : |spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (Φ (m - 1) t) y j) x i| ≤ 2 ^ 19 * a β I.Λ (m - 1)

The Hessian entries needed by the first-derivative drift error have a fixed numerical bound times the physical stream-amplitude scale.

theorem AVenhance.Infra.Section4.iterate_velocity_word_bound_of_A3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (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))) (t : ℝ) (w : List (Fin 2)) (hw : 1 ≤ w.length) (x : Homogenization.Vec 2) (i : Fin 2) : |iterateSpatialWord w (fun (y : Homogenization.Vec 2) => streamVel (Φ (m - 1)) t y i) x| ≤ 2 ^ 5 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ 2 * ↑(w.length + 1).factorial * (2 ^ 8 * (epsilon β I.Λ (m - 1))⁻¹) ^ (w.length + 1) / (↑w.length + 2) ^ 2

The stream-regularity estimates also control every positive-order velocity jet appearing in the material oscillatory errors. The component formula and derivative commutation are proved from the stream velocity.