Source-scale estimate for the additional transition-window remainder. The transition-window flux L² estimate remains an explicit source input.

theorem AVenhance.Infra.Section5.timeHMinusOneNorm_R46_sourceScale {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm C : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (hF : ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (r46Flux I hΦ m κm T t)) (hper : ∀ t ∈ Set.Ioo 0 1, IsZ2Periodic (r46Flux I hΦ m κm T t)) (hsource : (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(gradNormSq (r46Flux I hΦ m κm T t)) ^ 2) ^ (1 / 2) ≤ ENNReal.ofReal (section5SourceScale β I.Λ m κm C θ₀)) : (timeHMinusOneNorm fun (t : ℝ) => R46 I hΦ m κm T t) ≤ ENNReal.ofReal (section5SourceScale β I.Λ m κm C θ₀)

Conditional source-scale estimate for R46: the premise is the missing space-time L² estimate on its exact transition-window flux.