LeftJacobian the left-Jacobian form: on an active refresh window the large-scale cutoff ξ̂_l is the indicator of that window (local re-proof of the private lemmas of Terms/R46FluxSupport, which are not exported).

theorem AVenhance.Infra.Section5.LeftJacobian.HatXiWindow.indIcc_nonneg_e53 (a b t : ℝ) : 0 ≤ indIcc a b t

theorem AVenhance.Infra.Section5.LeftJacobian.hatZetaML_mem_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.LeftJacobian.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

On an active refresh window the large cutoff equals one.

theorem AVenhance.Infra.Section5.LeftJacobian.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

On an active refresh window all other large cutoffs vanish.