The running time of the typed answer-reduced sampler

Piece AR-3f of planning/answer-reduction.md, for lem:ar-typed-sampler. The typed sampler is the product of the oracularized sampler of the input sampler and the directly answered PCP sampler, whose parameters the routine parProg computes (MIPRE/Background/AnswerReduction/ArSampler). Its time at index n is dominated by (C (W + 1)^M)^{μ + 1} at degree E (μ + 1) (typedSampler_time) for any W above Q = (λn + 1)^μ, λ, σ, n and the input sampler's size, when the input sampler runs within Q (|d| + 1)^μ: the product's accounting (CL.ProductSampler.prog_time) with the oracularized sampler's (oracleSampler_timeBound) and the routine's (parProg_time).

theorem MIPRE.AnswerReduction.progs_size_pdom (PD : SAT.PcpDecider) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ} (sp : Cost.Prog) (lam mu sigma : ℕ), 1 ≤ X → Cost.esize sp ≤ W → lam ≤ W → sigma ≤ W → Pipeline.PDom W X mu c m e (Cost.esize (OracleSampler.prog sp) + Cost.esize (parProg PD lam mu sigma))

The sizes of the two programs the product hardcodes are dominated.

theorem MIPRE.AnswerReduction.typedSampler_time (ℓ : ℕ) (PD : SAT.PcpDecider) (R : Polynomial ℕ) : ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W : ℕ} (S : CL.Sampler (ℓ + 1)) (lam mu sigma n : ℕ), ParamsBound PD R → arQ lam mu n ≤ W → lam ≤ W → sigma ≤ W → n ≤ W → Cost.esize S.prog ≤ W → S.TimeBoundAt n (arQ lam mu n) mu → (typedSampler S PD lam mu sigma).TimeBoundAt n ((C * (W + 1) ^ M) ^ (mu + 1)) (E * (mu + 1))

The running time of the typed answer-reduced sampler.