The running time of the typed answer-reduced decider

Piece AR-3f of planning/answer-reduction.md, for lem:ar-typed-decider. The decider's eight stages (MIPRE/Background/AnswerReduction/ArDecider) are, in cost: the parameter routine and the budgets' routine (parCore_time, budCore_time); four calls to the input sampler through the universal machine, each on a marginal query of a constant-size header and the oracle half of a question (size_margQuery_le), so that one call costs Q (c W)^μ when the oracle halves are at most W long (PDom.ofCall); two runs of the PCP verifier and the final verdict, polynomial-time functions of the context. So the decider's time on (n, d) is dominated by (C (W + 1)^M X^E)^{μ + 1} (typedDecider_time) whenever |d| is, for any W above Q = (λn + 1)^μ, λ, σ, n and both input programs' sizes, when the input sampler runs within Q (|d| + 1)^μ and the two questions' oracle halves are at most W long — as they are on every input the detyping compiler hands the decider. No answer is ever handed to the input decider.

Sizes

theorem MIPRE.AnswerReduction.size_margQuery_le (ℓ : ℕ) (w : Player) (ob : Cost.BitStr) (d : Cost.Data) (hob : List.length ob ≤ d.size) : (Cost.encode (1, w, ℓ + 1, ob, [])).size ≤ 4 * d.size + 4 * ℓ + 40

A marginal query is linear in the input.

theorem MIPRE.AnswerReduction.margCall_pdom (ℓ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X K : ℕ} (sp : Cost.Prog) (n Q : ℕ) (q : Cost.Data) (t : ℕ), 1 ≤ X → Cost.esize sp ≤ W → n ≤ W → Q ≤ W → q.size + 1 ≤ (4 * ℓ + 44) * (W + 1) → t ≤ Q * (q.size + 1) ^ K → Pipeline.PDom W X K c m e (Cost.esize sp + ((Cost.encode n).cons q).size + t)

The cost of one marginal call through the universal machine, before the machine's overhead: the input sampler's program, the query, and the input sampler's time on it.

theorem MIPRE.AnswerReduction.next_pdom (c m e c' m' e' : ℕ) : ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X K : ℕ} (x r : Cost.Data), 1 ≤ X → Pipeline.PDom W X K c m e x.size → Pipeline.PDom W X K c' m' e' r.size → Pipeline.PDom W X K C M E (r.cons x).size

A context grows by one result.

theorem MIPRE.AnswerReduction.hdat_pdom : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X K : ℕ} (sp dp : Cost.Prog) (lam sigma : ℕ), 1 ≤ X → Cost.esize sp ≤ W → Cost.esize dp ≤ W → lam ≤ W → sigma ≤ W → Pipeline.PDom W X K c m e (Cost.encode (sp, dp, lam, K, sigma)).size

The hardcoded data (S̄, D̄, λ, μ, σ), at K = μ.

theorem MIPRE.AnswerReduction.input_pdom (cd md ed : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X K : ℕ} (n : ℕ) (d : Cost.Data), 1 ≤ X → n ≤ W → Pipeline.PDom W X K cd md ed d.size → Pipeline.PDom W X K c m e ((Cost.encode n).cons d).size

The index and the rest of the input.

theorem MIPRE.AnswerReduction.typedDecider_time (ℓ : ℕ) (PD : SAT.PcpDecider) (R : Polynomial ℕ) (cd md ed : ℕ) : ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ), ParamsBound PD R → 1 ≤ X → arQ lam mu n ≤ W → lam ≤ W → sigma ≤ W → n ≤ W → Cost.esize V.sampler.prog ≤ W → Cost.esize V.decider.prog ≤ W → V.sampler.TimeBoundAt n (arQ lam mu n) mu → ∀ (d : Cost.Data), Pipeline.PDom W X mu cd md ed d.size → List.length (CL.Detyping.Program.readBits.toFun (Cost.PolyTimeFun.treeHead.toFun (Cost.PolyTimeFun.treeTail.toFun d))) ≤ W + List.length (dB PD lam mu sigma n) → List.length (CL.Detyping.Program.readBits.toFun (Cost.PolyTimeFun.treeHead.toFun (Cost.PolyTimeFun.treeTail.toFun (Cost.PolyTimeFun.treeTail.toFun (Cost.PolyTimeFun.treeTail.toFun d))))) ≤ W + List.length (dB PD lam mu sigma n) → ∃ (r : Cost.Data) (t : ℕ), Pipeline.PDom W X mu C M E t ∧ (typedDecider PD V lam mu sigma).prog.Runs ((Cost.encode n).cons d) r t

The running time of the typed answer-reduced decider, on every input (n, d) whose size is dominated and whose two question fields have oracle halves no longer than W — as the detyped decider's inputs have: their oracle halves are the input sampler's questions.