The running time of the repeated decider

repDecider_timeBound: when the input sampler and decider run within R.S (|d| + 1)^{R.k} and R.D (|d| + 1)^{R.k} at index n, the repeated decider on (λ, τ, β) runs within c (W + 1)^m (|d| + 1)^{e (R.k + 1)} for constants c, m, e independent of everything and W any number dominating the parameters (DecDom). The cost is the explicit one of prepProg_runs and coordLoop_runs_bounded, dominated piece by piece as in SamplerCost.lean; the one point of care is that the sanitized inputs of the loop are no larger than the raw ones (size_encode_bitsOf_le, size_parse_bitsOf_le), so that the input decider is called on data of size below |d| and its bound needs no factor c^{R.k}.

Sizes of the sanitized inputs

theorem MIPRE.Repeat.length_toList_le (d : Cost.Data) : d.toList.length + 1 ≤ d.size

theorem MIPRE.Repeat.size_ofBool_bitOf_le (a : Cost.Data) : (Cost.Data.ofBool a.bitOf).size ≤ a.size

theorem MIPRE.Repeat.size_list_map_ofBool_bitOf_le (l : List Cost.Data) : (Cost.Data.list (List.map Cost.Data.ofBool (List.map Cost.Data.bitOf l))).size ≤ (Cost.Data.list l).size

theorem MIPRE.Repeat.size_encode_bitsOf_le (d : Cost.Data) : (Cost.encode (Cost.Data.bitsOf d.toList)).size ≤ d.size

Sanitizing a datum into a bit string does not increase its size.

theorem MIPRE.Repeat.size_parse_bitsOf_le (d : Cost.Data) : (Cost.Data.parse (Cost.Data.bitsOf d.toList)).size ≤ d.size

theorem MIPRE.Repeat.mem_decQueries {dD nD : Cost.Data} {s : ℕ} (k : ℕ) (remX remY remA remB : List Cost.Data) (q : Cost.Data) : q ∈ Cost.Prog.decQueries dD nD s k remX remY remA remB → ∃ (xi : Cost.Data) (yi : Cost.Data) (ai : Cost.Data) (bi : Cost.Data), q = Cost.Prog.decQuery dD nD xi yi ai bi ∧ xi.size ≤ (Cost.Data.list remX).size ∧ yi.size ≤ (Cost.Data.list remY).size ∧ ai.size ≤ (Cost.Data.list remA).size ∧ bi.size ≤ (Cost.Data.list remB).size

Every query of the loop has the shape (D̄, (n, xᵢ, yᵢ, aᵢ, bᵢ)) with each component no larger than the list it is cut from.

Domination of the primitives' costs

theorem MIPRE.Repeat.dom_bitsCost : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {L sz : ℕ}, 1 ≤ X → L ≤ X → sz ≤ X → Dom W X K c m e (Cost.Prog.bitsCost L sz)

theorem MIPRE.Repeat.dom_lenCost : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {L sz : ℕ}, 1 ≤ X → L ≤ X → sz ≤ X → Dom W X K c m e (Cost.Prog.lenCost L sz)

theorem MIPRE.Repeat.dom_eqCost (c₁ m₁ e₁ c₂ m₂ e₂ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {l₁ l₂ : Cost.Data}, 1 ≤ X → Dom W X K c₁ m₁ e₁ l₁.size → Dom W X K c₂ m₂ e₂ l₂.size → Dom W X K c m e (Cost.Prog.eqCost l₁ l₂)

theorem MIPRE.Repeat.dom_parseCost : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {x : Cost.BitStr}, 1 ≤ X → List.length x ≤ X → Dom W X K c m e (Cost.Prog.parseCost x)

theorem MIPRE.Repeat.dom_serCost : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {d : Cost.Data}, 1 ≤ X → d.size ≤ X → Dom W X K c m e (Cost.Prog.serCost d)

theorem MIPRE.Repeat.dom_dblCost : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {mm a : ℕ}, 1 ≤ X → 2 ^ mm ≤ W → a ≤ W → Dom W X K c m e (Cost.Prog.dblCost mm a)

theorem MIPRE.Repeat.dom_esize' {W X K x : ℕ} (hx : x ≤ W) : Dom W X K (4 + 1) 1 0 (Cost.encode x).size

theorem MIPRE.Repeat.dom_prepCost (cd md ed : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {sP dP : Cost.Data} {lam tau beta n s : ℕ} {xD yD aD bD : Cost.Data} {td : ℕ}, 1 ≤ X → 1 ≤ W → Dom W X K cd md ed td → sP.size ≤ W → dP.size ≤ W → lam ≤ W → tau ≤ W → beta ≤ W → n ≤ W → s ≤ W → 2 ^ (tau * (lam.size + n.size)) ≤ W → 2 ^ (beta * (lam.size + n.size)) ≤ W → xD.size + yD.size + aD.size + bD.size + 3 ≤ X → Dom W X K c m e (Cost.Prog.prepCost sP dP lam tau beta n s xD yD aD bD td)

The cost of the preparation, prepCost, dominated.

theorem MIPRE.Repeat.dom_yM : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {p n RD M : ℕ}, 1 ≤ X → p ≤ W → n ≤ W → RD ≤ W → M + 1 ≤ X → Dom W X K c m e (p + (Cost.esize n + M + 1) + RD * (M + 1) ^ K)

The argument of the bound on a call of the input decider from the loop, on data of size at most M.

The calls of the loop

theorem MIPRE.Repeat.loop_calls_time (D : Decider) (n : ℕ) (R : Budget) (hD : D.TimeBoundAt n R.D R.k) (s k : ℕ) (remX remY remA remB : List Cost.Data) : ∃ (fq : Cost.Data → Cost.Data), ∀ q ∈ Cost.Prog.decQueries (Cost.encode D.prog) (Cost.encode n) s k remX remY remA remB, ∃ t ≤ Polynomial.eval (Cost.esize D.prog + (Cost.esize n + ((Cost.Data.list remX).size + (Cost.Data.list remY).size + (Cost.Data.list remA).size + (Cost.Data.list remB).size + 3) + 1) + R.D * ((Cost.Data.list remX).size + (Cost.Data.list remY).size + (Cost.Data.list remA).size + (Cost.Data.list remB).size + 3 + 1) ^ R.k) Cost.selfUniversal.bound, Cost.Eval [q] Cost.selfUniversal.univ (fq q) t

The calls of the coordinate loop to the input decider, through the universal machine, within a uniform bound: M bounds the size of the data each is called on.

The running time

structure MIPRE.Repeat.DecDom {ℓ : ℕ} (S : CL.Sampler ℓ) (D : Decider) (lam tau beta n : ℕ) (R : Budget) (W : ℕ) : Prop

The hypotheses on the dominating number W.

• S_le : R.S ≤ W
• D_le : R.D ≤ W
• lam_le : lam ≤ W
• tau_le : tau ≤ W
• beta_le : beta ≤ W
• n_le : n ≤ W
• sizeS_le : Cost.esize S.prog ≤ W
• sizeD_le : Cost.esize D.prog ≤ W
• pow_le : 10 ^ R.k ≤ W
• reps_le : Repetition.reps lam tau n ≤ W
• parse_le : Repetition.parseBound lam beta n ≤ W
• dim_le : S.dim n ≤ W

theorem MIPRE.Repeat.DecDom.one_le {ℓ : ℕ} {S : CL.Sampler ℓ} {D : Decider} {lam tau beta n : ℕ} {R : Budget} {W : ℕ} (hW : DecDom S D lam tau beta n R W) : 1 ≤ W

theorem MIPRE.Repeat.size_encode_decParams_le {ℓ : ℕ} {S : CL.Sampler ℓ} {D : Decider} {lam tau beta n : ℕ} {R : Budget} {W : ℕ} (hW : DecDom S D lam tau beta n R W) : (Cost.encode ((S.prog, D.prog), lam, tau, beta)).size ≤ 14 * W + 7

The size of the parameters datum.

theorem MIPRE.Repeat.decMalformed_time : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {ℓ : ℕ} (S : CL.Sampler ℓ) (D : Decider) (lam tau beta n : ℕ) (R : Budget) (W : ℕ) (d : Cost.Data), DecDom S D lam tau beta n R W → (d = Cost.Data.nil ∨ (∃ (xD : Cost.Data), d = xD.cons Cost.Data.nil) ∨ ∃ (xD : Cost.Data) (yD : Cost.Data), d = xD.cons (yD.cons Cost.Data.nil)) → ∃ (r : Cost.Data), ∃ t ≤ c * (W + 1) ^ m * (d.size + 1) ^ (e * (R.k + 1)), (repDeciderProg S.prog D.prog lam tau beta).Runs ((Cost.encode n).cons d) r t

On a malformed input (fewer than three components), the repeated decider rejects at once.

theorem MIPRE.Repeat.decWellformed_time : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {ℓ : ℕ} (S : CL.Sampler ℓ) (D : Decider) (lam tau beta n : ℕ) (R : Budget) (W : ℕ) (xD yD aD bD : Cost.Data), DecDom S D lam tau beta n R W → S.TimeBoundAt n R.S R.k → D.TimeBoundAt n R.D R.k → ∃ (r : Cost.Data), ∃ t ≤ c * (W + 1) ^ m * ((xD.cons (yD.cons (aD.cons bD))).size + 1) ^ (e * (R.k + 1)), (repDeciderProg S.prog D.prog lam tau beta).Runs ((Cost.encode n).cons (xD.cons (yD.cons (aD.cons bD)))) r t

On a well-formed input (x, y, a, b) (any four data), the repeated decider halts within a dominated time.

theorem MIPRE.Repeat.repDecider_timeBound : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {ℓ : ℕ} (S : CL.Sampler ℓ) (D : Decider) (lam tau beta n : ℕ) (R : Budget) (W : ℕ), DecDom S D lam tau beta n R W → S.TimeBoundAt n R.S R.k → D.TimeBoundAt n R.D R.k → (repDecider S.prog D.prog lam tau beta).TimeBoundAt n (c * (W + 1) ^ m) (e * (R.k + 1))

The running time of the repeated decider: constants c, m, e uniform in everything such that, whenever W dominates the parameters at n and the input sampler and decider run within R.S (|d| + 1)^{R.k} and R.D (|d| + 1)^{R.k} there, the repeated decider runs within c (W + 1)^m (|d| + 1)^{e (R.k + 1)}.