The stream recursion gives the exact perpendicular-gradient velocity increment used in the Section 5 operator split.

theorem AVenhance.Infra.Section5.StreamVelocityIncrement.admissibleStream_spatialSlice_contDiff {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) (t : ℝ) : ContDiff ℝ (↑⊤) (φ t)

theorem AVenhance.Infra.Section5.streamSeq_psiTilde_differentiableAt {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (t : ℝ) (x : Homogenization.Vec 2) : DifferentiableAt ℝ (psiTilde I hΦ m t) x

The scalar recursion coefficient is differentiable in space because it is the difference of the two admissible stream slices.

theorem AVenhance.Infra.Section5.streamSeq_velocity_increment_eq_psiTilde {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (t : ℝ) (x : Homogenization.Vec 2) : streamVel (Φ m) t x - streamVel (Φ (m - 1)) t x = sigmaMat.mulVec (spaceGrad (psiTilde I hΦ m t) x)

For every m ≥ 1, differentiating the stream recursion in space gives b_m - b_{m-1} = σ ∇ψTilde_m. The current stream's smoothness is read from the next recursive witness in IsStreamSeq, while the previous stream is the one supplied by the m-th step.