The running times of the answer-reduced sampler and calculator

Slice P4h of planning/aldous-lyons-track.md, for the complexity clause of TailoredAnswerReduction. The output verifier's programs run the routine's parameter program as a stage; everything else they run is a polynomial-time function or, in the processor, the input sampler. So one hypothesis on the routine suffices, ArRoutine.ParTime: its parameter program runs within (c (W + 1)^m X^e)^{μ + 1} (MIPRE.Pipeline.PRuns) for every W above (λn + 1)^μ + σ + λ + n (AnswerReduction.arg), as the MIP* answer reduction's does (MIPRE.AnswerReduction.parProg_time). Under it:

• params_pdom: the parameters' encoding is dominated, and with it every parameter (le_size_arParams);
• arSampler_time: the sampler, the product of the oracularized input sampler and the low-degree half, detyped (CL.ProductSampler.prog_time, CL.Detyping.sampler_time);
• arSampler_dim_pdom: its dimension;
• lenD_time and lenD_len_pdom: the calculator, and the lengths it outputs;
• lenD_total: the calculator halts on every input — the contract's len_total, which needs no hypothesis.

theorem MIPRE.Tailored.AnsRed.Typed.le_of_arg_le {lam mu sigma n W : ℕ} (h : AnswerReduction.arg lam mu sigma n ≤ W) : (lam * n + 1) ^ mu ≤ W ∧ sigma ≤ W ∧ lam ≤ W ∧ n ≤ W

The four bounds W ≥ (λn + 1)^μ + σ + λ + n gives.

theorem MIPRE.Tailored.AnsRed.Typed.le_size_arParams (t j d : ℕ) (L : PcpDims) (e : Cost.Data) : t + j + d + L.ℓ + L.dm + L.r + L.s ≤ (Cost.encode (arParams t j d L e)).size ∧ 2 ^ j ≤ (Cost.encode (arParams t j d L e)).size

Every parameter is below the size of the parameters' encoding.

theorem MIPRE.Tailored.AnsRed.Typed.lms_pdom : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ} (lam mu sigma : ℕ), 1 ≤ X → lam ≤ W → sigma ≤ W → Pipeline.PDom W X mu c m e (Cost.encode (lam, mu, sigma)).size

(λ, μ, σ), at K = μ.

def MIPRE.Tailored.AnsRed.Typed.ArRoutine.ParTime (R : ArRoutine) : Prop

The parameter program runs in polynomial time: for every W above (λn + 1)^μ + σ + λ + n, within (c (W + 1)^m X^e)^{μ + 1}. The one cost hypothesis on a routine; the routine P4i fixes satisfies it.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.params_pdom {R : ArRoutine} (hR : R.ParTime) : ∃ (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 (Cost.encode (R.params lam mu sigma n)).size

The parameters' encoding is dominated.

The sampler

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.ldCore_time {R : ArRoutine} (hR : R.ParTime) : ∃ (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 R.ldCore (Cost.encode ((lam, mu, sigma), n)) ((R.fam lam mu sigma).pd n)

The parameter program projected to the low-degree half's parameters.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.ldPar_time {R : ArRoutine} (hR : R.ParTime) : ∃ (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 (R.toLd.parPF.toFun (lam, mu, sigma)) (Cost.encode n) ((R.fam lam mu sigma).pd n)

The low-degree half's parameter program, (λ, μ, σ) hardcoded.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.arProgs_size_pdom {R : ArRoutine} : ∃ (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 (R.toLd.parPF.toFun (lam, mu, sigma)))

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

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.arTyped_time {R : ArRoutine} (hR : R.ParTime) (ℓ : ℕ) : ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W : ℕ} (S : CL.Sampler (ℓ + 1)) (lam mu sigma n : ℕ), AnswerReduction.arg lam mu sigma n ≤ W → Cost.esize S.prog ≤ W → S.TimeBoundAt n ((lam * n + 1) ^ mu) mu → (R.toLd.arTyped lam mu sigma S).TimeBoundAt n ((C * (W + 1) ^ M) ^ (mu + 1)) (E * (mu + 1))

The running time of the typed answer-reduced sampler: the product's accounting with the oracularized sampler's and the low-degree half's parameter program's.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.arSampler_time {R : ArRoutine} (hR : R.ParTime) (ℓ : ℕ) : ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W : ℕ} (S : CL.Sampler (ℓ + 1)) (lam mu sigma n : ℕ), AnswerReduction.arg lam mu sigma n ≤ W → Cost.esize S.prog ≤ W → S.TimeBoundAt n ((lam * n + 1) ^ mu) mu → (R.toLd.arSampler lam mu sigma S).TimeBoundAt n ((C * (W + 1) ^ M) ^ (mu + 1)) (E * (mu + 1))

The running time of the answer-reduced sampler, detyped.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.arSampler_dim_pdom {R : ArRoutine} (hR : R.ParTime) (ℓ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ} (S : CL.Sampler (ℓ + 1)) (lam mu sigma n : ℕ), 1 ≤ X → AnswerReduction.arg lam mu sigma n ≤ W → S.dim n ≤ W → Pipeline.PDom W X mu c m e ((R.toLd.arSampler lam mu sigma S).dim n)

The dimension of the answer-reduced sampler is dominated: the graph view's bits, the input sampler's dimension and (2M + 1) t bits of the low-degree half.

The calculator

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenD_time {R : ArRoutine} (hR : R.ParTime) : ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X : ℕ} (lam mu sigma n : ℕ) (d : Cost.Data), 1 ≤ X → AnswerReduction.arg lam mu sigma n ≤ W → d.size + 1 ≤ X → ∃ (r : Cost.Data) (t : ℕ), Pipeline.PDom W X mu C M E t ∧ (R.lenD lam mu sigma).prog.Runs ((Cost.encode n).cons d) r t

The running time of the answer-length calculator, on every input: the parameter stage, then the polynomial-time function lenF.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenD_len_pdom {R : ArRoutine} (hR : R.ParTime) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ} (lam mu sigma n : ℕ), 1 ≤ X → AnswerReduction.arg lam mu sigma n ≤ W → ∀ (x : Cost.BitStr) (κ : Bool) (k : ℕ), LenIs (R.lenD lam mu sigma) n x κ k → Pipeline.PDom W X mu c m e k

The lengths the calculator outputs are dominated: products of a codeword count, a number of coefficients and the field width, each below a power of the parameters' size.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lenD_total (R : ArRoutine) (lam mu sigma n s : ℕ) : LenTotal (R.lenD lam mu sigma) n s

The calculator halts on every input (TailoredAnswerReduction.len_total).