The actual Hm material source along any flow of the previous velocity. Only positive-time joint regularity is used.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_Hm_material_derivative_along_flow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {g : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev) (hT : I.IsTIterates hΦ m κm κprev g θprev T) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow (streamVel (Φ (m - 1))) X) {t s : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : HasDerivAt (fun (r : ℝ) => I.Hm hΦ m κm (T (Nstar β)) r (X r x s)) (hmEndpoint I hΦ m κm (T (Nstar β)) (Jcut β) t (X t x s) - hmEndpoint I hΦ m κm (T (Nstar β)) 0 t (X t x s)) t

Pulling actual Hm along the previous velocity differentiates to the actual endpoint difference, with no negative-time or initial-time calculus premise.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_xFlow_joint_continuous {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) : Continuous fun (z : ST) => I.xFlow hΦ m l z.1 z.2

The actual fixed-start flow is jointly continuous in time and position.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_Hm_derivative_along_xFlow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {g : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev) (hT : I.IsTIterates hΦ m κm κprev g θprev T) (l : ℤ) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : HasDerivAt (fun (r : ℝ) => I.Hm hΦ m κm (T (Nstar β)) r (I.xFlow hΦ m l r x)) (hmEndpoint I hΦ m κm (T (Nstar β)) (Jcut β) t (I.xFlow hΦ m l t x) - hmEndpoint I hΦ m κm (T (Nstar β)) 0 t (I.xFlow hΦ m l t x)) t

The previous-scale fixed-start flow has the exact positive-time material derivative.