Actual large-cutoff support, local finiteness, and mixed derivative bounds.

theorem AVenhance.Infra.Section4.amnr_hatXi_support {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) {t : ℝ} (ht : I.hatXiML 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)

The actual support lies in the closed source window.

theorem AVenhance.Infra.Section4.amnr_hatXi_support_radius {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) {t : ℝ} (ht : I.hatXiML m l t ≠ 0) : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m

Distance form of the source support window.

theorem AVenhance.Infra.Section4.amnr_hatXi_local_finite {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : ∃ (s : Finset ℤ), s.card ≤ 3 ∧ ∀ (u : ℝ), |u - t| < tauPP β I.Λ m / 8 → ∀ l ∉ s, I.hatXiML m l u = 0

At most three lattice indices occur in a fixed small neighborhood of a specified time. This is a local support statement, not just pointwise finiteness.

theorem AVenhance.Infra.Section4.amnr_hatXi_derivative_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) {j : ℕ} (hj : j ≤ Nstar β) (t : ℝ) : |iteratedDeriv j (I.hatXiML m l) t| ≤ I.Chat * (tauP β I.Λ m)⁻¹ ^ j

The source derivative bound, expressed without weighted denominators.

theorem AVenhance.Infra.Section4.amnr_hatXi_mixed_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) {b : AmnrSpace → Homogenization.Vec 2} {S : ℝ} (hS : 0 ≤ S) (w : List (Option (Fin 2))) (hw : IsAmnrMixedWord w) (hbudget : amnrBudget w ≤ Nstar β) (z : AmnrSpace) : |amnrWord b w (fun (y : AmnrSpace) => I.hatXiML m l y.1) z| ≤ I.Chat * amnrWeight S (tauP β I.Λ m)⁻¹ w

Mixed derivatives of the actual cutoff use only its source time bounds.

theorem AVenhance.Infra.Section4.amnrWord_zero (b : AmnrSpace → Homogenization.Vec 2) (w : List (Option (Fin 2))) : amnrWord b w 0 = 0

Every directional word annihilates the zero function.

theorem AVenhance.Infra.Section4.amnr_hatXi_product_word_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (f : AmnrSpace → ℝ) (b : AmnrSpace → Homogenization.Vec 2) (w : List (Option (Fin 2))) (z : AmnrSpace) (hfar : tauPP β I.Λ m / 2 + tauP β I.Λ m < |z.1 - ↑l * tauPP β I.Λ m|) : amnrWord b w ((fun (y : AmnrSpace) => I.hatXiML m l y.1) * f) z = 0

Outside the closed source window, every jet of the cutoff-flow product vanishes by locality, including jets at zero values of the cutoff.