Exact integration of the actual finite Leibniz flux.

theorem AVenhance.Infra.Section4.iterate_truncated_split_flux_pairing_integral (P : List (List (Fin 2) × List (Fin 2))) {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (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)) (hA : ∀ p ∈ P, ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (A z.1) p.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) {s : ℝ} (hs1 : s ≤ 1) (w : List (Fin 2)) : ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) (iterateSplitFlux P (A z.1) (v z.1) z.2) = (List.map (fun (p : List (Fin 2) × List (Fin 2)) => ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) ((iterateMatrixWord (A z.1) p.1 z.2).mulVec (spaceGrad (iterateSpatialWord p.2 (v z.1)) z.2))) P).sum

Integrating the actual selected flux preserves every ordered split.