Actual zero-stream base cases for the higher material induction.

theorem AVenhance.Infra.Section4.amnr_streamVelocity_zero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) : (fun (y : AmnrSpace) => streamVel (Φ 0) y.1 y.2) = 0

theorem AVenhance.Infra.Section4.amnr_streamVelocity_zero_word {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (w : List (Option (Fin 2))) (i : Fin 2) : (amnrWord (fun (y : AmnrSpace) => streamVel (Φ 0) y.1 y.2) w fun (y : AmnrSpace) => streamVel (Φ 0) y.1 y.2 i) = 0

theorem AVenhance.Infra.Section4.amnr_streamGradient_zero_word {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (w : List (Option (Fin 2))) (i p : Fin 2) : amnrWord (fun (y : AmnrSpace) => streamVel (Φ 0) y.1 y.2) w (amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ 0) y.1 y.2) i p) = 0