Source spatial primitive estimates for the stream velocity.

theorem AVenhance.Infra.Section4.amnr_clm_norm_le_two_basis {L : Homogenization.Vec 2 →L[ℝ] ℝ} {B : ℝ} (hB : 0 ≤ B) (h0 : ‖L (Homogenization.basisVec 0)‖ ≤ B) (h1 : ‖L (Homogenization.basisVec 1)‖ ≤ B) : ‖L‖ ≤ 2 * B

Coordinate bounds control the operator norm in the fixed two-dimensional sup norm, with the explicit dimension factor.

theorem AVenhance.Infra.Section4.amnr_gradient_lipschitz_of_hessian {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) {B : ℝ} (hB : 0 ≤ B) (hH : ∀ (x : Homogenization.Vec 2) (J : Fin 2 → Fin 2), ‖(iteratedFDeriv ℝ 2 f x) fun (j : Fin 2) => Homogenization.basisVec (J j)‖ ≤ B) (i : Fin 2) : LipschitzWith (2 * B).toNNReal fun (x : Homogenization.Vec 2) => spaceGrad f x i

A smooth scalar's gradient coordinates inherit a Lipschitz bound from its actual Hessian coordinate bounds.

theorem AVenhance.Infra.Section4.amnr_streamVel_lipschitz_of_hessian {φ : ℝ → Homogenization.Vec 2 → ℝ} (t : ℝ) (hf : ContDiff ℝ (↑⊤) (φ t)) {B : ℝ} (hB : 0 ≤ B) (hH : ∀ (x : Homogenization.Vec 2) (J : Fin 2 → Fin 2), ‖(iteratedFDeriv ℝ 2 (φ t) x) fun (j : Fin 2) => Homogenization.basisVec (J j)‖ ≤ B) (x y : Homogenization.Vec 2) : ‖streamVel φ t x - streamVel φ t y‖ ≤ 2 * B * ‖x - y‖

Rotation of the gradient preserves its coordinate Lipschitz bound.

theorem AVenhance.Infra.Section4.amnr_streamVel_lipschitz_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x y : Homogenization.Vec 2) : ‖streamVel (Φ m) t x - streamVel (Φ m) t y‖ ≤ 2 ^ 20 * a β I.Λ m * ‖x - y‖

The source stream-regularity seminorm gives the velocity's spatial Lipschitz estimate. No derivative estimate for the velocity is assumed.

theorem AVenhance.Infra.Section4.amnr_flowGrad_abs_le_two_of_A3_ge_two {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 2 ≤ m) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (ht : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) (k p : Fin 2) : |I.flowGrad hΦ m l t x k p| ≤ 2

The actual pulled-back flow gradient is bounded by two on the cutoff window, from the source stream-regularity estimates, uniformly in the level and cutoff index.

theorem AVenhance.Infra.Section4.amnr_flowGrad_one_abs_le_one {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (k p : Fin 2) : |I.flowGrad hΦ 1 l t x k p| ≤ 1

The base stream has zero velocity, so its actual flow-gradient entries are bounded by one by the same characterized-flow estimate.

theorem AVenhance.Infra.Section4.amnr_flowGrad_abs_le_two_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (ht : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) (k p : Fin 2) : |I.flowGrad hΦ m l t x k p| ≤ 2

Uniform primitive flow size on every actual cutoff window, including the zero-stream base scale.