Auxiliary finite-order stream-regularity bounds, without restricting the paper budget. The stream-regularity estimates control every spatial order. Auxiliary constants may use a larger finite order while each paper derivative retains its separately checked budget.

theorem AVenhance.Infra.Section4.amnr_velocityGradient_spatial_le_of_A3_auxiliary_budget {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (α : List (Fin 2)) (N : ℕ) (hbudget : α.length ≤ N) (i p : Fin 2) (z : AmnrSpace) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2) (List.map some α) (amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2) i p) z| ≤ amnrSpatialVelocityConstant N * a β I.Λ m * (epsilon β I.Λ m)⁻¹ ^ α.length

theorem AVenhance.Infra.Section4.amnr_previous_velocityGradient_spatial_raw_le_of_A3_auxiliary_budget {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (α : List (Fin 2)) (N : ℕ) (hbudget : α.length ≤ N) (i p : Fin 2) (z : AmnrSpace) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) i p) z| ≤ amnrSpatialVelocityConstant N * a β I.Λ (m - 1) * (epsilon β I.Λ (m - 1))⁻¹ ^ α.length

The previous-scale spatial primitive bound retains the actual amplitude, including the zero-stream base case.

theorem AVenhance.Infra.Section4.amnr_previous_velocityGradient_iteratedFDeriv_norm_le_of_A3_auxiliary_budget {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (n N : ℕ) (hbudget : n ≤ N) (i p : Fin 2) (t : ℝ) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => amnrVelocityGradient (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) i p (t, y)) x‖ ≤ 2 ^ n * (amnrSpatialVelocityConstant N * a β I.Λ (m - 1) * (epsilon β I.Λ (m - 1))⁻¹ ^ n)

theorem AVenhance.Infra.Section4.amnr_previous_velocityJacobian_iteratedFDeriv_norm_le_of_A3_auxiliary_budget {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (n N : ℕ) (hbudget : n ≤ N) (t : ℝ) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => Flow.jointSpatialFDeriv (streamVel (Φ (m - 1))) t y) x‖ ≤ 2 ^ (n + 1) * (amnrSpatialVelocityConstant N * a β I.Λ (m - 1) * (epsilon β I.Λ (m - 1))⁻¹ ^ n)