Actual drift-gradient transfer on the full time cell.

theorem AVenhance.Infra.Section4.iterate_terminal_material_error_gradient_transfer {s : ℝ} (hs1 : s ≤ 1) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {u v : ℝ → Homogenization.Vec 2 → ℝ} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hQc : ContinuousOn Q (Set.Ici 0)) (hbp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (b t)) (hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t)) (hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t)) (w : List (Fin 2)) : ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (fun (y : Homogenization.Vec 2) => iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (z.1, y)) z.2) ((Q z.1).mulVec (spaceGrad (v z.1) z.2)) = -∫ (z : AmnrSpace) in iterateTruncatedCell s, iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) z * ∑ j : Fin 2, ∑ k : Fin 2, Q z.1 j k * spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (v z.1) y k) z.2 j

The differentiated material error transfers to the preceding Hessian over timeCube. Natural integrability follows from its explicit velocity sum.