The cutoff separation that reduces the spatial flux to one active shear.

theorem AVenhance.Infra.Section3.FluxStructure.zetaMK_coord_bound {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) (t : ℝ) (hzk : I.zetaMK m k t ≠ 0) : (t - ↑k * tau β I.Λ m) / tau β I.Λ m ∈ Set.Icc (-(2 / 3)) (2 / 3)

theorem AVenhance.Infra.Section3.FluxStructure.xi_eq_one_of_zetaMK_ne_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) (k : ℤ) (t : ℝ) (hzk : I.zetaMK m k t ≠ 0) : I.xiMK m k t = 1

theorem AVenhance.Infra.Section3.FluxStructure.xi_eq_zero_outside {β : ℝ} (I : Ingredients β) {u : ℝ} (hu : u ∉ Set.Icc (-(5 / 4)) (5 / 4)) : I.xi u = 0

theorem AVenhance.Infra.Section3.xiMK_eq_zero_outside {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) (t : ℝ) (hu : (t - ↑k * tau β I.Λ m) / tau β I.Λ m ∉ Set.Icc (-(5 / 4)) (5 / 4)) : I.xiMK m k t = 0

The scaled corrector cutoff vanishes outside its support interval.

theorem AVenhance.Infra.Section3.FluxStructure.odd_indices_separated {k l : ℤ} (hk : Odd k) (hl : Odd l) (hne : k ≠ l) : l ≤ k - 2 ∨ k + 2 ≤ l

theorem AVenhance.Infra.Section3.xiMK_eq_one_of_zetaMK_ne_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) (k : ℤ) (t : ℝ) (hzk : I.zetaMK m k t ≠ 0) : I.xiMK m k t = 1

On the support of an odd small cutoff, its own transition cutoff is one.

theorem AVenhance.Infra.Section3.xiMK_eq_zero_of_zetaMK_ne_zero_of_odd_ne {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) {k l : ℤ} (hk : Odd k) (hl : Odd l) (hne : l ≠ k) (t : ℝ) (hzk : I.zetaMK m k t ≠ 0) : I.xiMK m l t = 0

At a time in one odd shear's active cutoff, all other odd transition cutoffs vanish.

theorem AVenhance.Infra.Section3.chiM_eq_chiMK_of_zetaMK_ne_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) {k : ℤ} (hk : Odd k) (t : ℝ) (x : Homogenization.Vec 2) (hzk : I.zetaMK m k t ≠ 0) : I.chiM κ m t x = I.chiMK κ m k t x

On the support of one odd stream cutoff, the summed corrector is exactly the matching single-mode corrector.

theorem AVenhance.Infra.Section3.psiM_eq_single_of_zetaMK_ne_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ m) {k : ℤ} (hk : Odd k) (t : ℝ) (x : Homogenization.Vec 2) (hzk : I.zetaMK m k t ≠ 0) : I.psiM m t x = I.zetaProd m k t * psi β I.Λ m k x

When an odd mode is active, the stream field sum has only that mode.