Exact recursion identities for the selected stream increments.

theorem AVenhance.Infra.Section5.StreamIncrement.psi_zero_of_not_odd {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (x : Homogenization.Vec 2) (hk : ¬Odd k) : psi β I.Λ m k x = 0

theorem AVenhance.Infra.Section5.StreamIncrement.tsum_eq_odd_subtype_of_even_zero (f : ℤ → ℝ) (hzero : ∀ (k : ℤ), ¬Odd k → f k = 0) : ∑' (k : ℤ), f k = ∑' (k : { k : ℤ // Odd k }), f ↑k

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

The recursive increment of Φ_m is exactly the odd-mode corrector coefficient ψTilde_m.