The running time of the parameter program

Slice P4i of planning/aldous-lyons-track.md: the parameter program arParCore κ runs within (c (W + 1)^m X^e)^{μ + 1} for every W ≥ (λn + 1)^μ + σ + λ + n (arParCore_time), the routine's ArRoutine.ParTime.

Its loops run as long as the values they write: Q, μ, σ (the budgets' routine, by MIPRE.AnswerReduction.budCore_time), r, s and 2^j. All of them are dominated (vals_pdom): ◇ = (μ + 2)(Q + 4) and K = E₁ (μ + 1)(oW + Q + 4) are products of quantities below W and below μ + 1, which the exponent μ + 1 of the bound absorbs (PDom.ofLeK); T = 2^K is only written in binary, of K + 1 bits; r ≤ c (|T| + |σ'| + 1) and s ≤ P(|n| + |T| + Q + σ') by the window describer's bounds; and 2^j ≤ 2m + 1. The sizes of the data between the stages are dominated as the outputs of runs (PRuns.size_le).

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.pushU_time (g : Cost.PolyTimeFun Cost.Data ℕ) (c m e c' m' e' : ℕ) : ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} (x : Cost.Data), 1 ≤ X → Pipeline.PDom W X K c m e x.size → Pipeline.PDom W X K c' m' e' (g.toFun x) → Pipeline.PRuns W X K C M E (pushU g) x ((Cost.encode (Cost.unary (g.toFun x))).cons x)

The running time of a loop stage: the data and the number written dominated.

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.two_pow_size_le (m : ℕ) : 2 ^ m.size ≤ 2 * m + 1

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.size_le_self (m : ℕ) : m.size ≤ m

theorem MIPRE.Tailored.AnsRed.Typed.ArPar.vals_pdom (κ : Params.ArConsts) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ} (lam mu sigma n : ℕ), 1 ≤ X → AnswerReduction.arg lam mu sigma n ≤ W → Pipeline.PDom W X mu c m e (Params.pQ lam mu n + mu + sigma + Params.pR κ lam mu sigma n + Params.pS κ lam mu sigma n + 2 ^ Params.pJ κ lam mu sigma n)

The values the loops write are dominated.

theorem MIPRE.Tailored.AnsRed.Typed.arParCore_time (κ : Params.ArConsts) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ} (lam mu sigma n : ℕ), 1 ≤ X → AnswerReduction.arg lam mu sigma n ≤ W → Pipeline.PRuns W X mu c m e (arParCore κ) (Cost.encode ((lam, mu, sigma), n)) (Cost.encode (arParams (Params.pTw κ lam mu sigma n) (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (Params.pExtra κ lam mu sigma n)))

The running time of the parameter program: within (c (W + 1)^m X^e)^{μ + 1} for every W ≥ (λn + 1)^μ + σ + λ + n.