The running time of the parameter routine

Piece AR-3f of planning/answer-reduction.md. The routine parProg of answer reduction computes the PCP's parameters pd n by loops whose lengths are the values λ, n, μ, Q = (λn + 1)^μ and the parameters k, m, s; so its time is polynomial in those values, and dominated in the sense of MIPRE.Pipeline.PDom by any W ≥ Q, λ, σ, n at K = μ (parProg_time), provided the PCP's parameters are polynomial in (log n, log T, Q, σ) (ParamsBound), as the paper's pcpparams are. The bit length of T = 2^{(Q + 5)(μ + 1)} is (Q + 5)(μ + 1) + 1, a product of a quantity below W and one below K + 1.

def MIPRE.AnswerReduction.ParamsBound (PD : SAT.PcpDecider) (R : Polynomial ℕ) : Prop

The PCP's parameters are polynomial in (log n, log T, Q, σ), by the polynomial R.

Equations

• MIPRE.AnswerReduction.ParamsBound PD R = ∀ (n T Q σ : ℕ), (PD.params n T Q σ).k + (PD.params n T Q σ).m + (PD.params n T Q σ).s ≤ Polynomial.eval (n.size + T.size + Q + σ) R

@[reducible, inline]

abbrev MIPRE.AnswerReduction.linC : ℕ

The constant dominating the routine's linear quantities.

Equations

• MIPRE.AnswerReduction.linC = 40 + 2 * 40 + 40 + 3

theorem MIPRE.AnswerReduction.pdLin {W X K v : ℕ} (hX : 1 ≤ X) (h : v ≤ 40 * W + 40 * (K + 1) + 40) : Pipeline.PDom W X K linC 1 0 v

theorem MIPRE.AnswerReduction.pdQ {W X K v : ℕ} (hX : 1 ≤ X) (h : v ≤ 40 * W + 40 * (K + 1) + 40 + 4 * (W + 1) ^ 2) : Pipeline.PDom W X K (linC + 4) 2 0 v

A linear function of W and K + 1 plus a square in W: the routine's quantities, λn + 1 among them.

theorem MIPRE.AnswerReduction.lam_mul_add_one_le (lam n W : ℕ) (hl : lam ≤ W) (hn : n ≤ W) : lam * n + 1 ≤ (W + 1) ^ 2

theorem MIPRE.AnswerReduction.size_X0 (lam mu sigma n : ℕ) : ((Cost.encode (lam, mu, sigma)).cons (Cost.encode n)).size = Cost.esize lam + Cost.esize mu + Cost.esize sigma + Cost.esize n + 3

theorem MIPRE.AnswerReduction.budCore_time : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ} (lam mu sigma n : ℕ), 1 ≤ X → arQ lam mu n ≤ W → lam ≤ W → sigma ≤ W → n ≤ W → Pipeline.PRuns W X mu c m e ParRoutine.budCore ((Cost.encode (lam, mu, sigma)).cons (Cost.encode n)) (Cost.encode (arQ lam mu n, tPcp lam mu n))

The running time of the budgets' routine.

theorem MIPRE.AnswerReduction.size_tPcp (lam mu n : ℕ) : (tPcp lam mu n).size = (arQ lam mu n + 5) * (mu + 1) + 1

The argument of the parameter bound, |n| + |T| + Q + σ.

theorem MIPRE.AnswerReduction.params_pdom (PD : SAT.PcpDecider) (R : Polynomial ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ}, ParamsBound PD R → ∀ (lam mu sigma n : ℕ), 1 ≤ X → arQ lam mu n ≤ W → sigma ≤ W → n ≤ W → Pipeline.PDom W X mu c m e (20 * ((arPar PD lam mu sigma n).k + (arPar PD lam mu sigma n).m + (arPar PD lam mu sigma n).s) + 20)

The PCP's parameters are dominated, with the contexts that hold them.

theorem MIPRE.AnswerReduction.ctxQT_pdom : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ} (lam mu sigma n : ℕ), 1 ≤ X → arQ lam mu n ≤ W → lam ≤ W → sigma ≤ W → n ≤ W → Pipeline.PDom W X mu c m e ((Cost.encode (arQ lam mu n, tPcp lam mu n)).cons ((Cost.encode (lam, mu, sigma)).cons (Cost.encode n))).size

The context after the budgets, ((Q, T), (λ, μ, σ), n), is dominated.

theorem MIPRE.AnswerReduction.parCore_time (PD : SAT.PcpDecider) (R : Polynomial ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ}, ParamsBound PD R → ∀ (lam mu sigma n : ℕ), 1 ≤ X → arQ lam mu n ≤ W → lam ≤ W → sigma ≤ W → n ≤ W → Pipeline.PRuns W X mu c m e (ParRoutine.core PD) ((Cost.encode (lam, mu, sigma)).cons (Cost.encode n)) ((family PD lam mu sigma).pd n)

The running time of the routine's core, on ((λ, μ, σ), n).

theorem MIPRE.AnswerReduction.parProg_time (PD : SAT.PcpDecider) (R : Polynomial ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ}, ParamsBound PD R → ∀ (lam mu sigma n : ℕ), 1 ≤ X → arQ lam mu n ≤ W → lam ≤ W → sigma ≤ W → n ≤ W → Pipeline.PRuns W X mu c m e (parProg PD lam mu sigma) (Cost.encode n) ((family PD lam mu sigma).pd n)

The running time of the parameter routine parProg, on the index n.