The residual field adapter for BigBoundInputs.

theorem AVenhance.Infra.Section5.Integration.frozenResidualBigBoundResidual {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm κprev : ℝ) (hκm : 0 < κm) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (t : ℝ) : t ∈ Set.Ioo 0 1 → ∀ (x : Homogenization.Vec 2), sourceResidualIdentity I hΦ m κm κprev T t x

The BigBoundInputs.residual field follows from the iterate recursion and the exact classical-solution predicate for the previous iterate. At each positive time, choose any positive localization radius.