Public statement.

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

Well-definedness (existence) of the construction: the recursion can be carried out at every step. Together with IsStreamSeq.unique this makes φ_m a well-defined sequence. Provable from the closure theorem FILE 9 by recursion (same Paper proof lemma).