Positive-time transport estimates ignore the arbitrary extension at nonpositive times, including its value at zero.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_backward_transport_of_positive_data {F source : ℝ → Homogenization.Vec 2 → ℝ} (X : ℝ → Ergodic.PeriodicVolumePreservingDiffeomorphism 2) (hFper : ∀ (t : ℝ), 0 < t → IsZ2Periodic (F t)) (hSourcePer : ∀ (t : ℝ), 0 < t → IsZ2Periodic (source t)) (hComp : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 ((X p.1).toFun p.2)) (Set.Ioi 0 ×ˢ Set.univ)) (hSourceComp : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => source p.1 ((X p.1).toFun p.2)) (Set.Ioi 0 ×ˢ Set.univ)) (hMaterial : ∀ (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), HasDerivAt (fun (s : ℝ) => F s ((X s).toFun x)) (source t ((X t).toFun x)) t) {b D : ℝ} (hb : 0 < b) (hD : 0 ≤ D) (hzero : F b = 0) (hSourceIntegral : ∀ t ∈ Set.Ioc 0 b, ∫ (s : ℝ) in t..b, √(l2NormSq (source s)) ≤ D) (t : ℝ) : t ∈ Set.Ioc 0 b → √(l2NormSq (F t)) ≤ 2 * D

All periodicity premises are positive-time premises. Zeroing the unused nonpositive slices lets the existing transport FTC apply without constraining the original extension.