The literal time-only K coefficient and the spatial flow correction remain separate in every differentiated forcing.

theorem AVenhance.Infra.Section4.iterateSpatialWord_const (c : ℝ) (w : List (Fin 2)) : (iterateSpatialWord w fun (x : Homogenization.Vec 2) => c) = fun (x : Homogenization.Vec 2) => if w = [] then c else 0

Positive-order spatial words annihilate a spatial constant.

theorem AVenhance.Infra.Section4.iterateLowerWordFlux_constant (B : Matrix (Fin 2) (Fin 2) ℝ) (v : Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) : iterateLowerWordFlux (fun (x : Homogenization.Vec 2) => B) v w = 0

A spatial constant matrix has no lower-order Leibniz flux.

theorem AVenhance.Infra.Section4.iterateWordFlux_constant (B : Matrix (Fin 2) (Fin 2) ℝ) (v : Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateWordFlux (fun (x : Homogenization.Vec 2) => B) v w x = B.mulVec (spaceGrad (iterateSpatialWord w v) x)

Only the principal flux survives for the time-only coefficient.

theorem AVenhance.Infra.Section4.iterateWordFlux_add {A B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (v : Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateWordFlux (fun (y : Homogenization.Vec 2) => A y + B y) v w x = iterateWordFlux A v w x + iterateWordFlux B v w x

The expanded flux is linear in its smooth matrix coefficient.

theorem AVenhance.Infra.Section4.iterateWordFlux_TForcing_coefficient {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev t : ℝ) (hs : ContDiff ℝ (↑⊤) (I.sMat hΦ m κm t)) (v : Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateWordFlux (fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y) v w x = (I.Kmat κm m t - κprev • 1).mulVec (spaceGrad (iterateSpatialWord w v) x) + iterateWordFlux (I.sMat hΦ m κm t) v w x

Exact forcing-flux decomposition for the literal iterate equation.