Disjointness of the small ζ window from all but its assigned large window.

theorem AVenhance.Infra.Ingredients.Overlap.zetaMK_mem_outer_interval {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) (t : ℝ) (hτ : 0 < tau β I.Λ m) (hne : I.zetaMK m k t ≠ 0) : t ∈ Set.Icc (↑k * tau β I.Λ m - 2 / 3 * tau β I.Λ m) (↑k * tau β I.Λ m + 2 / 3 * tau β I.Λ m)

theorem AVenhance.Infra.Ingredients.Overlap.hatZetaML_mem_core_interval {β : ℝ} (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.Ingredients.cutoff_overlaps {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k l : ℤ) (hl : l ≠ lIdx β I.Λ m k) (t : ℝ) : I.hatZetaML m l t * I.zetaMK m k t = 0

e.cutoff.overlaps (1363-1365), with the corrected floor index: for l ≠ l_k the translated large cutoff and small cutoff have zero product.