Support and fixed-time algebra for the transition-window flux.

The cutoff inequalities in the ingredient package imply genuine support statements because their lower bounds are nonnegative indicators.

theorem AVenhance.Infra.Section5.R46FluxSupport.indIcc_nonneg_r46 (a b t : ℝ) : 0 ≤ indIcc a b t

theorem AVenhance.Infra.Section5.R46FluxSupport.hatZetaML_mem_refresh_window {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (hne : I.hatZetaML m l t ≠ 0) : t ∈ Set.Icc ((↑l - 1 / 2) * tauPP β I.Λ m + tauP β I.Λ m) ((↑l + 1 / 2) * tauPP β I.Λ m - tauP β I.Λ m)

theorem AVenhance.Infra.Section5.R46FluxSupport.xiMK_ne_zero_near_center {β : ℝ} (I : Ingredients β) (m : ℕ) {k : ℤ} {t : ℝ} (hne : I.xiMK m k t ≠ 0) : |t - ↑k * tau β I.Λ m| ≤ 5 / 4 * tau β I.Λ m

theorem AVenhance.Infra.Section5.R46FluxSupport.tauP_ge_five_tau {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) : 5 * tau β I.Λ m ≤ tauP β I.Λ m

theorem AVenhance.Infra.Section5.lIdx_eq_of_hatZeta_xiMK_ne_zero {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (l k : ℤ) (t : ℝ) (hz : I.hatZetaML m l t ≠ 0) (hξ : I.xiMK m k t ≠ 0) : lIdx β I.Λ m k = l

If a large refresh cutoff and a small xi cutoff are both active, the small cutoff's refresh index is the large cutoff's index.

theorem AVenhance.Infra.Section5.R46FluxSupport.hatXiML_eq_one_of_hatZeta_ne_zero {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (hz : I.hatZetaML m l t ≠ 0) : I.hatXiML m l t = 1

theorem AVenhance.Infra.Section5.R46FluxSupport.hatXiML_eq_zero_of_ne_refresh {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (l j : ℤ) (t : ℝ) (hz : I.hatZetaML m l t ≠ 0) (hjl : j ≠ l) : I.hatXiML m j t = 0

theorem AVenhance.Infra.Section5.Gbar_eq_G_of_hatZeta_ne_zero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (T : ℝ → Homogenization.Vec 2 → ℝ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hz : I.hatZetaML m l t ≠ 0) : Gbar I hΦ m T t x = G I hΦ m T l t x

On any active refresh window, the large-scale average of the pulled-back gradients is exactly the gradient with that window's index.

theorem AVenhance.Infra.Section5.flux_eq_kappa_of_hatZeta_zero {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (κ t : ℝ) (hzero : ∀ (l : ℤ), I.hatZetaML m l t = 0) : I.flux κ m t = κ • 1

If all refresh coefficients vanish, the exact Section 3 flux formula reduces to the molecular matrix. This uses the zetaProd coefficient and does not require the unmasked small cutoff zetaMK itself to vanish.

theorem AVenhance.Infra.Section5.r46Flux_eq_zero_of_hatZeta_ne_zero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (l : ℤ) (t : ℝ) (hz : I.hatZetaML m l t ≠ 0) : r46Flux I hΦ m κm T t = 0

The flux vanishes wherever one of the refresh cutoffs is active.

theorem AVenhance.Infra.Section5.r46Flux_eq_kappa_smul_defect_of_hatZeta_zero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hzero : ∀ (l : ℤ), I.hatZetaML m l t = 0) : r46Flux I hΦ m κm T t = κm • ∑' (k : { k : ℤ // Odd k }), I.xiMK m (↑k) t • (Gbar I hΦ m T t - G I hΦ m T (lIdx β I.Λ m ↑k) t)

On the complement of the refresh windows the actual flux factor of the transition-window term is exactly κm I.