Linearity of the forcing, with an explicit regularity premise on its actual coefficient. No quantitative V or T estimate is assumed.

theorem AVenhance.Infra.Section4.IteratesForcing.gradient_contDiff_one {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 2 f) : ContDiff ℝ 1 (spaceGrad f)

theorem AVenhance.Infra.Section4.IteratesForcing.matrix_gradient_differentiable {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {f : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ 1 A) (hf : ContDiff ℝ 2 f) : Differentiable ℝ fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad f y)

theorem AVenhance.Infra.Section4.matrix_div_gradient_sub {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {f g : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ 1 A) (hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 2 g) (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad (fun (z : Homogenization.Vec 2) => f z - g z) y)) x = vecDiv (fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad f y)) x - vecDiv (fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad g y)) x

The divergence-form diffusion forcing is linear in its scalar argument.

theorem AVenhance.Infra.Section4.TForcing_sub {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) {f g : ℝ → Homogenization.Vec 2 → ℝ} (t : ℝ) (hA : ContDiff ℝ 1 fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y) (hf : ContDiff ℝ 2 (f t)) (hg : ContDiff ℝ 2 (g t)) (x : Homogenization.Vec 2) : I.TForcing hΦ m κm κprev (fun (s : ℝ) (y : Homogenization.Vec 2) => f s y - g s y) t x = I.TForcing hΦ m κm κprev f t x - I.TForcing hΦ m κm κprev g t x

Linearity for the actual TForcing. The coefficient regularity is stated explicitly for subsequent discharge from the flow regularity data.

theorem AVenhance.Infra.Section4.increment_classical_forcing {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hA : ∀ (t : ℝ), 0 < t → ContDiff ℝ 1 fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y) (i : ℕ) (hi : i + 1 ≤ Nstar β) : IsClassicalSol (streamVel (Φ (m - 1))) κprev (I.TForcing hΦ m κm κprev (iterateIncrement T i)) (fun (x : Homogenization.Vec 2) => 0) (iterateIncrement T (i + 1))

e.Vm-1.i for the actual iterates, including the first step. The only extra structural input is C¹ regularity of the actual coefficient.