The actual iterate gradient equation in primitive flux form.

theorem AVenhance.Infra.Section4.amnr_temperature_gradient_flux_equation {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {v u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ v₀ : Homogenization.Vec 2 → ℝ} {Fv : ℝ → Homogenization.Vec 2 → ℝ} (hv : IsClassicalSol (streamVel (Φ (m - 1))) κprev Fv v₀ v) (hu : IsClassicalSol (streamVel (Φ (m - 1))) κprev (I.TForcing hΦ m κm κprev v) u₀ u) (p : Fin 2) : Set.EqOn (amnrOp (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) none (amnrTGradient u p)) (fun (z : AmnrSpace) => κprev * ∑ q : Fin 2, amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) [some q, some q] (amnrTGradient u p) z + ∑ q : Fin 2, amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) [some p, some q] (amnrTemperatureFlux I hΦ m κm κprev v q) z - ∑ q : Fin 2, amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) q p z * amnrTGradient u q z) (Set.Ioi 0 ×ˢ Set.univ)

The source iterate equation has exactly two diffusion/flux spatial letters and the actual velocity-gradient contraction.

theorem AVenhance.Infra.Section4.amnr_temperature_material_step_budget (α : List (Fin 2)) {r N : ℕ} (hbudget : α.length + 2 * (r + 1) ≤ N) (p q : Fin 2) : amnrBudget (amnrMixedWord α r ++ [some p, some q]) ≤ N ∧ amnrMaterialCount (amnrMixedWord α r ++ [some p, some q]) ≤ r ∧ ∀ (η : List (Fin 2)) (s : ℕ), η.length + 2 * s ≤ amnrBudget (amnrMixedWord α r) → s ≤ r → η.length + 2 * s + 2 ≤ N

The canonical material step preserves the total budget by spending two units on diffusion or flux. Every lower canonical jet stays at material level at most r; this is checked before applying normal ordering.