The actual spatial velocity base case, without a drift amplitude bound.

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