The actual forcing in the ordered flux calculus.

theorem AVenhance.Infra.Section4.amnr_temperatureFlux_contDiffOn {β : ℝ} (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) (j : Fin 2) : ContDiffOn ℝ (↑(Nstar β)) (amnrTemperatureFlux I hΦ m κm κprev u j) (Set.Ioi 0 ×ˢ Set.univ)

Flux regularity uses only the proved finite Kmat order and actual classical temperature regularity on the positive-time domain.

theorem AVenhance.Infra.Section4.amnr_temperatureForcing_eq_flux_divergence {β : ℝ} (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) : Set.EqOn (fun (z : AmnrSpace) => I.TForcing hΦ m κm κprev u z.1 z.2) (fun (z : AmnrSpace) => ∑ j : Fin 2, amnrOp B (some j) (amnrTemperatureFlux I hΦ m κm κprev u j) z) (Set.Ioi 0 ×ˢ Set.univ)

The matrix divergence equals the ordered coordinate divergence of its actual flux, with no forcing estimate or evolution equation assumed.