Conditional producer for the R46 source-scale contract with an abstract amplitude.

The generic flux estimate uses Section 2 flow-distortion data and the n=0 previous-iterate energy estimate. The big-bound estimate producer constructs the flow data through the Section 2 chain, so only the TGradientContract remains a conditional input.

theorem AVenhance.Infra.Section5.Contracts.R46Source.epsilon_two_delta_le_delta_r46Source (β : ℝ) (I : Ingredients β) (m : ℕ) : epsilon β I.Λ m ^ (2 * delta β) ≤ epsilon β I.Λ m ^ delta β

theorem AVenhance.Infra.Section5.Contracts.r46TimeL2_flux_le_of_flowBounds_and_energy {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (Cmat : ℝ) (hflow : FlowBoundsData I Φ hΦ Cmat) (m : ℕ) (hm : 1 ≤ m) (κm κprev C B : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (hF : ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (r46Flux I hΦ m κm T t)) (hκm : 0 < κm) (hκprev : 0 < κprev) (hκ : κm ≤ κprev) (henergy : √κprev * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T t) x) ≤ C * B) : (r46TimeL2 fun (t : ℝ) => r46Flux I hΦ m κm T t) ≤ ENNReal.ofReal (C * epsilon β I.Λ (m - 1) ^ delta β * √κm * B)

R46's space-time flux estimate with the amplitude left abstract. The energy premise is exactly the n = 0 gradient estimate represented by TGradientContract.