Exact derivative of the actual lower material error.

theorem AVenhance.Infra.Section4.iterate_transport_smooth {b : Homogenization.Vec 2 → Homogenization.Vec 2} {u : Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => Homogenization.vecDot (b x) (spaceGrad u x)

The actual scalar transport field is smooth.

theorem AVenhance.Infra.Section4.iterate_transport_gradient_formula {b : Homogenization.Vec 2 → Homogenization.Vec 2} {u : Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) (x : Homogenization.Vec 2) (j : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => Homogenization.vecDot (b y) (spaceGrad u y)) x j = ∑ k : Fin 2, spaceGrad (fun (y : Homogenization.Vec 2) => b y k) x j * spaceGrad u x k + Homogenization.vecDot (b x) (spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad u y j) x)

One spatial derivative of actual transport separates the velocity jet from transport of the differentiated scalar.

theorem AVenhance.Infra.Section4.iterate_material_error_gradient_formula {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {u : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) (w : List (Fin 2)) (x : Homogenization.Vec 2) (j : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, y)) x j = iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) (j :: w) (fun (z : AmnrSpace) => u z.1 z.2) (t, x) - ∑ k : Fin 2, spaceGrad (fun (y : Homogenization.Vec 2) => b t y k) x j * spaceGrad (iterateSpatialWord w (u t)) x k

Differentiating Err_w gives Err_(j::w) minus the one-jet velocity term. This formula contains only derivatives of actual fields and no PDE premise.