Full nonnegative energies control each actual terminal stream pairing.

theorem AVenhance.Infra.Section4.iterate_truncated_stream_pairing_bound_full {ψ u v : ℝ → Homogenization.Vec 2 → ℝ} {H : ℝ} (hH : 0 < H) (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)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) {s : ℝ} (hs : 0 ≤ s) (hs1 : s ≤ 1) (hψp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (ψ t)) (hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t)) (hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t)) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2), |spaceGrad (ψ t) x j| ≤ H) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (u z.1) z.2) ((ψ z.1 z.2 • sigmaMat).mulVec (spaceGrad (v z.1) z.2))| ≤ H * ((∫ (z : ℝ × Homogenization.Vec 2) in timeCube, u z.1 z.2 ^ 2) + spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (v t))

The terminal signed stream integral is bounded using full nonnegative energies, after the actual spatial skew transfer on that terminal cell.