The Hm expansion vanishes in the gaps between the large-scale cutoff supports. This is the endpoint input in the source's transported energy argument.

theorem AVenhance.Infra.Section4.hatZetaML_eq_zero_of_cellGap {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l k : ℤ) {t : ℝ} (ht : t ∈ Set.Ioo ((↑l + 1 / 2) * tauPP β I.Λ m - tauP β I.Λ m) ((↑l + 1 / 2) * tauPP β I.Λ m + tauP β I.Λ m)) : I.hatZetaML m k t = 0

Every translated large-scale zeta cutoff vanishes in a gap of radius tauP around a half-cell boundary.

theorem AVenhance.Infra.Section4.LMN_eq_zero_of_cellGap {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) {t κ : ℝ} (n : ℕ) (ht : t ∈ Set.Ioo ((↑l + 1 / 2) * tauPP β I.Λ m - tauP β I.Λ m) ((↑l + 1 / 2) * tauPP β I.Λ m + tauP β I.Λ m)) : I.LMN κ m n t = 0

The actual memory coefficient L_{m,n} is identically zero on every large-scale cutoff gap.

theorem AVenhance.Infra.Section4.Amnr_eq_zero_of_cellGap {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (n : ℕ) (l : ℤ) (r : ℕ) (t : ℝ) : t ∈ Set.Ioo ((↑l + 1 / 2) * tauPP β I.Λ m - tauP β I.Λ m) ((↑l + 1 / 2) * tauPP β I.Λ m + tauP β I.Λ m) → ∀ (x : Homogenization.Vec 2) (i j k : Fin 2), I.Amnr hΦ m κ n T r t x i j k = 0

Every recursively defined A_{m,n,r} tensor vanishes throughout a large-scale cutoff gap. The induction uses the literal corrected recursion, and only differentiates a function that is locally identically zero there.

theorem AVenhance.Infra.Section4.Hmr_eq_zero_of_cellGap {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (l : ℤ) {t : ℝ} (ht : t ∈ Set.Ioo ((↑l + 1 / 2) * tauPP β I.Λ m - tauP β I.Λ m) ((↑l + 1 / 2) * tauPP β I.Λ m + tauP β I.Λ m)) (x : Homogenization.Vec 2) : I.Hmr hΦ m κ T r t x = 0

Each H_{m,r} vanishes in the same cutoff gap, since its entire divergence field is spatially zero there.

theorem AVenhance.Infra.Section4.Hm_eq_zero_at_halfCell {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (l : ℤ) : I.Hm hΦ m κ T ((↑l + 1 / 2) * tauPP β I.Λ m) = fun (x : Homogenization.Vec 2) => 0

The H_m expansion vanishes at every half-cell boundary.

theorem AVenhance.Infra.Section4.hmEndpoint_eq_zero_at_halfCell {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (l : ℤ) : Section5.hmEndpoint I hΦ m κ T r ((↑l + 1 / 2) * tauPP β I.Λ m) = fun (x : Homogenization.Vec 2) => 0

Each endpoint potential in the telescope vanishes at every half-cell boundary. This is the companion endpoint to Hm_eq_zero_at_halfCell.