Exact first and high stream order split at each terminal time.

theorem AVenhance.Infra.Section4.iterate_truncated_stream_pairing_order_split {φ u : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => φ z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.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) (iterateWordFlux (fun (y : Homogenization.Vec 2) => φ z.1 y • sigmaMat) (u z.1) w z.2) = (∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) (iterateSplitFlux (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => p.1.length == 1) (iterateSpatialSplits w)) (fun (y : Homogenization.Vec 2) => φ z.1 y • sigmaMat) (u z.1) z.2)) + ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) (iterateSplitFlux (List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (2 ≤ p.1.length)) (iterateSpatialSplits w)) (fun (y : Homogenization.Vec 2) => φ z.1 y • sigmaMat) (u z.1) z.2)

The actual stream energy flux has no principal contribution; its first and high parts retain all multiplicities exactly.