Uniform producer

theorem AVenhance.Infra.Section5.RelativeError.e44_initialTrace_contract (β C₀ : ℝ) : ∃ (Ctr : ℝ) (L : ℝ), 1 ≤ Ctr ∧ Integration.OnA8Instances β C₀ L fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (_T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => 6 / 5 ≤ β → epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R → e44PositiveTraceInput β I κ M m θ₀ θprev Ctr

Uniform AV-parameter positive trace. The recursion constants, and hence Ctr, are selected from l_recurse β C₀ before the Ingredients instance. The gate and later-scale hypothesis match the step-down part (ii) consumers.