Provider proof of existence of the recursively constructed stream sequence.

theorem AVenhance.Proofs.exists_isStreamSeq {β : ℝ} (I : Ingredients β) : ∃ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ

Stream-function estimates: recursively choose the zero stream and then apply the one-step recursion, using stream-function estimates to keep every predecessor admissible.