The flux coefficient input for the positive-time H_m source.

The estimates are assembled from the Section 3 flux - Jhat remainder, the zeroth-order bounds on Jhat - κ I and Kmat - κ I, and the diffusivity-recursion scale package.

theorem AVenhance.Infra.Section4.Kmat_sub_kappa_entry_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hratio : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m) (t : ℝ) (i j : Fin 2) : |(I.Kmat κ m t - κ • 1) i j| ≤ ↑(Nstar β) * (I.Czeta * a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ)

The oscillatory part of Kmat is bounded by the number of Taylor terms times the standard a_m² ε_m⁴/κ scale.

theorem AVenhance.Infra.Section4.flux_sub_Kmat_entry_abs_le_of_small_ratio {β : ℝ} (I : Ingredients β) {C₀ CJ : ℝ} (hCzeta : I.Czeta ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1) (hJbound : ∀ (t : ℝ) (i j : Fin 2), |(I.Jhat κ m t - κ • 1) i j| ≤ CJ * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ)) (t : ℝ) (i j : Fin 2) : |(I.flux κ m t - I.Kmat κ m t) i j| ≤ (4 * Real.pi ^ 2 * C₀ * ↑(Nstar β) * 2 ^ Nstar β + CJ + ↑(Nstar β) * C₀) * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ)

flux-Kmat is controlled by the sum of the two comparison errors and the Section 3 flux-Jhat remainder.

theorem AVenhance.Infra.Section4.hm_flux_coefficient_rate_onA7 (β C₀ : ℝ) (hC₀ : 1 ≤ C₀) : ∃ (C₁ : ℝ) (Cflux : ℝ), 0 ≤ Cflux ∧ Section5.Integration.OnA7Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (_θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (_T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => ∀ (t : ℝ) (i j : Fin 2), |(I.flux (I.kappaSeq κ M m) m t - I.Kmat (I.kappaSeq κ M m) m t) i j| ≤ Cflux * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / I.kappaSeq κ M m)

The scale hypotheses, together with the diffusivity-recursion chain, provide the small-ratio flux coefficient bound used by the positive-time H_m pairing.