Source-scale estimate for the time-cutoff term. The missing §4 bound is stated on its spatial L² norm; the negative-norm transfer is proved.

theorem AVenhance.Infra.Section5.timeHMinusOneNorm_cutoff1_sourceScale {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm C : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (hL2 : ∀ t ∈ Set.Ioo 0 1, Homogenization.MemL2On unitCube (cutoff1 I hΦ m κm T t)) (hmean : ∀ t ∈ Set.Ioo 0 1, Homogenization.MeanZeroOn unitCube (cutoff1 I hΦ m κm T t)) (hsource : (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal ((2 * Real.pi)⁻¹ * √(l2NormSq (cutoff1 I hΦ m κm T t))) ^ 2) ^ (1 / 2) ≤ ENNReal.ofReal (section5SourceScale β I.Λ m κm C θ₀)) : (timeHMinusOneNorm fun (t : ℝ) => cutoff1 I hΦ m κm T t) ≤ ENNReal.ofReal (section5SourceScale β I.Λ m κm C θ₀)

Conditional source-scale estimate for cutoff1, after inserting the source-level spatial L² bound into Poincaré duality.