The corrector equation pushed through its smooth inverse flow.

theorem AVenhance.Infra.Section5.frozen_corrector_flux_contDiff_one {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) (j : Fin 2) (t : ℝ) : ContDiff ℝ 1 (frozenCorrectorFlux I κ m k j t)