Exact current material pairing with its retained drift commutator.

theorem AVenhance.Infra.Section4.iterate_terminal_commuted_current_pairing_split {s : ℝ} (hs1 : s ≤ 1) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u v : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (hsol : IsClassicalSol b κ F u₀ u) (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (hFc : ContinuousOn (fun (z : AmnrSpace) => spaceGrad (iterateSpatialWord w (F z.1)) z.2) (Set.Ici 0 ×ˢ Set.univ)) (hQc : ContinuousOn Q (Set.Ici 0)) : ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (amnrMaterial b (fun (s : ℝ) => iterateSpatialWord w (u s)) z.1) z.2) ((Q z.1).mulVec (spaceGrad (v z.1) z.2)) = (∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (amnrMaterial b u z.1)) z.2) ((Q z.1).mulVec (spaceGrad (v z.1) z.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))

The commuted current material pairing is the original PDE pairing minus the actual drift error. Its natural integrability is derived from the PDE.