Source transport identities for fields pulled back by the flow.

theorem AVenhance.Infra.Section5.TransportIdentities.frozen_inverse_flow_left {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (r : ℝ) (y : Homogenization.Vec 2) : I.xFlowInv hΦ m l r (I.xFlow hΦ m l r y) = y

theorem AVenhance.Infra.Section5.TransportIdentities.frozen_inverse_flow_right {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (r : ℝ) (y : Homogenization.Vec 2) : I.xFlow hΦ m l r (I.xFlowInv hΦ m l r y) = y

theorem AVenhance.Infra.Section5.TransportIdentities.chiMK_joint_contDiff_one {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) : ContDiff ℝ 1 (Function.uncurry fun (r : ℝ) (y : Homogenization.Vec 2) => I.chiMK κ m k r y)

theorem AVenhance.Infra.Section5.chiTilde_material_transport_component {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (i : Fin 2) : deriv (fun (r : ℝ) => I.chiTilde hΦ m κ k r x i) t + (fderiv ℝ (I.chiTilde hΦ m κ k t) x) (streamVel (Φ (m - 1)) t x) i = deriv (fun (r : ℝ) => I.chiMK κ m k r (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x) i) t

With the inverse slice regularity derived from the flow, transport of the single-mode corrector is exactly the source identity e.tbm1.one (at a fixed spatial point and coordinate).