Differentiating the actual forcing flux within its finite source order.

theorem AVenhance.Infra.Section4.amnr_temperatureForcing_gradient_eq_flux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κprev F u₀ u) (B : AmnrSpace → Homogenization.Vec 2) (hB : ContDiff ℝ (↑⊤) B) (p : Fin 2) {z : AmnrSpace} (hz : 0 < z.1) : spaceGrad (I.TForcing hΦ m κm κprev u z.1) z.2 p = ∑ q : Fin 2, amnrWord B [some p, some q] (amnrTemperatureFlux I hΦ m κm κprev u q) z

Two ordinary derivatives suffice to identify the forcing gradient. No infinite regularity of the time-dependent Kmat is used.