The running time of the answer-reduced linear-constraints processor

Slice P4h of planning/aldous-lyons-track.md, for the complexity clause of TailoredAnswerReduction. The processor's nine stages (ArRoutine.lpCore) are, in cost: the parameter program (ArRoutine.ParTime); four calls to the input sampler through the universal machine, each on a marginal query of a constant-size header and a question's seed bits, at most linear in the input (AnswerReduction.size_margQuery_le), so that one call costs (λn + 1)^μ (c W X)^μ (margCallX_pdom); two runs of the circuit function and two of the proof check, polynomial-time functions run on encodings (argCircL_eq, argPrfL_eq: the stages' arguments are encodings on every input, the input sampler's questions and the readable answers read as bit strings); and the last stage, a polynomial-time function of the context. So the processor's time on (n, d) is dominated by (C (W + 1)^M X^E)^{μ + 1} with X = |d| + 1 (lpD_time), for every W above (λn + 1)^μ + σ + λ + n, when |𝒱| ≤ σ and the input sampler runs within (λn + 1)^μ (|d| + 1)^μ. Neither the input's calculator nor its processor is ever run: they enter the circuit function's input as data.

The stages' arguments are encodings

theorem MIPRE.Tailored.AnsRed.Typed.argCircL_eq (k rA rB : ℕ) (X : Cost.Data) (P : Cost.Prog × Cost.Prog × Cost.Prog) (lms : ℕ × ℕ × ℕ) (n : ℕ) (prm : ArParams) (hP : (progsL k).toFun X = Cost.encode P) (hl : (lmsL k).toFun X = Cost.encode lms) (hn : (nL k).toFun X = Cost.encode n) (hp : (AnswerReduction.res (k - 1)).toFun X = Cost.encode prm) : (argCircL k rA rB).toFun X = Cost.encode (P, lms, n, prm, CL.Detyping.Program.readBits.toFun ((AnswerReduction.res rA).toFun X), CL.Detyping.Program.readBits.toFun ((AnswerReduction.res rB).toFun X))

A circuit stage's argument is the encoding of the circuit function's input, as soon as the hardcoded data, the index and the parameters are encodings.

theorem MIPRE.Tailored.AnsRed.Typed.argPrfL_eq (k rC : ℕ) (o : Cost.PolyTimeFun LpIn Cost.Unary) (q : Cost.PolyTimeFun LpIn Cost.BitStr) (a : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data) (X : Cost.Data) (prm : ArParams) (C : SAT.Circuit) (hp : (AnswerReduction.res (k - 1)).toFun X = Cost.encode prm) (hC : (AnswerReduction.res rC).toFun X = Cost.encode C) : (argPrfL k rC o q a).toFun X = Cost.encode (prm, o.toFun ((preL k).toFun X), nF.toFun ((preL k).toFun X), (ptsF q).toFun ((preL k).toFun X), CL.Detyping.Program.readBits.toFun ((a k).toFun X), C.gates)

A proof stage's argument is the encoding of the proof check's input, as soon as the parameters and the circuit are encodings.

Sizes

theorem MIPRE.Tailored.AnsRed.Typed.length_seedL_le (k : ℕ) (q : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data) (X : Cost.Data) : List.length ((seedL k q).toFun X) ≤ ((q k).toFun X).size

A question's seed bits are no longer than its field.

theorem MIPRE.Tailored.AnsRed.Typed.lpHdat_pdom : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ} (P : Cost.Prog × Cost.Prog × Cost.Prog) (lam mu sigma : ℕ), 1 ≤ X → Cost.esize P.1 ≤ W → Cost.esize P.2.1 ≤ W → Cost.esize P.2.2 ≤ W → lam ≤ W → sigma ≤ W → Pipeline.PDom W X mu c m e (Cost.encode (P, lam, mu, sigma)).size

The hardcoded data (V.progs, λ, μ, σ), at K = μ.

theorem MIPRE.Tailored.AnsRed.Typed.margCallX_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) * X → t ≤ Q * (q.size + 1) ^ K → Pipeline.PDom W X K c m e (Cost.esize sp + ((Cost.encode n).cons q).size + t)

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, for a query linear in X.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.lpD_time {R : ArRoutine} (ℓ : ℕ) (hR : R.ParTime) : ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W X : ℕ} (V : TailoredVerifier (ℓ + 1)) (lam mu sigma n : ℕ) (d : Cost.Data), 1 ≤ X → AnswerReduction.arg lam mu sigma n ≤ W → V.size ≤ sigma → V.sampler.TimeBoundAt n ((lam * n + 1) ^ mu) mu → d.size + 1 ≤ X → ∃ (r : Cost.Data) (t : ℕ), Pipeline.PDom W X mu C M E t ∧ (R.lpD ℓ V.progs lam mu sigma).prog.Runs ((Cost.encode n).cons d) r t

The running time of the linear-constraints processor, on every input (n, d): dominated by (C (W + 1)^M X^E)^{μ + 1} for X > |d| and W ≥ (λn + 1)^μ + σ + λ + n, when |𝒱| ≤ σ and the input sampler runs within (λn + 1)^μ (|d| + 1)^μ.