The running time of the repeated linear-constraints processor

repLp_timeBound: with the input sampler, calculator and processor within R at index n, the repeated processor halts on every input (n, d) within c (W + 1)^m (|d| + 1)^{e (R.k + 1)}, along the stages of lpCore_runsLe, as repLen_timeBound does for the calculator. Every query to the input programs is of size linear in |d| (mem_lpLenQs, mem_lpPQs): the blocks of the questions and the readable answers are pieces of the input.

Sizes

theorem MIPRE.Tailored.RepProg.size_treeTail_le (d : Cost.Data) : (Cost.PolyTimeFun.treeTail.toFun d).size ≤ d.size

theorem MIPRE.Tailored.RepProg.length_readBits_le (d : Cost.Data) : List.length (CL.Detyping.Program.readBits.toFun d) ≤ d.size

theorem MIPRE.Tailored.RepProg.length_readX_le (d : Cost.Data) : List.length (readX d) ≤ d.size

theorem MIPRE.Tailored.RepProg.length_readY_le (d : Cost.Data) : List.length (readY d) ≤ d.size

theorem MIPRE.Tailored.RepProg.length_readAR_le (d : Cost.Data) : List.length (readAR d) ≤ d.size

theorem MIPRE.Tailored.RepProg.length_readBR_le (d : Cost.Data) : List.length (readBR d) ≤ d.size

theorem MIPRE.Tailored.RepProg.esize_block_le {l : List Bool} {s k : ℕ} {xi : Cost.BitStr} (h : xi ∈ blocks l s k) : Cost.esize xi ≤ 4 * l.length + 1

theorem MIPRE.Tailored.RepProg.mem_lpLenQs {st : LpSt} {q : Cost.Data} (hq : q ∈ lpLenQs st) : ∃ (xi : Cost.BitStr) (b : Bool), q = Cost.encode (st.1.1.2.1, xi, b) ∧ Cost.esize xi ≤ 4 * st.1.1.2.2.size + 1

Every query to the input calculator is (n, xᵢ, κ) with xᵢ of size linear in the input.

theorem MIPRE.Tailored.RepProg.mem_lpPQs {st : LpSt} {rs : List Cost.Data} {q : Cost.Data} (hq : q ∈ lpPQs st rs) : ∃ (xi : Cost.BitStr) (yi : Cost.BitStr) (a : Cost.BitStr) (b : Cost.BitStr), q = Cost.encode (st.1.1.2.1, xi, yi, a, b) ∧ Cost.esize xi ≤ 4 * st.1.1.2.2.size + 1 ∧ Cost.esize yi ≤ 4 * st.1.1.2.2.size + 1 ∧ Cost.esize a ≤ 4 * st.1.1.2.2.size + 1 ∧ Cost.esize b ≤ 4 * st.1.1.2.2.size + 1

Every query to the input processor is (n, xᵢ, yᵢ, a^R_i, b^R_i) with every component of size linear in the input.

@[simp]

theorem MIPRE.Tailored.RepProg.length_lpLenQs (st : LpSt) : (lpLenQs st).length = 4 * List.length st.2

theorem MIPRE.Tailored.RepProg.length_lpPQs_le (st : LpSt) (rs : List Cost.Data) : (lpPQs st rs).length ≤ List.length st.2

The cost of the core, dominated

theorem MIPRE.Tailored.RepProg.esize_lpPads_le (rs : List Cost.Data) (k : ℕ) : Cost.esize (lpPads rs k) ≤ Polynomial.eval (Cost.esize (rs, Cost.unary k)) lpPadsF.timeBound

theorem MIPRE.Tailored.RepProg.dom_lpCoreCost (cd md ed cT₁ mT₁ eT₁ cZ₁ mZ₁ eZ₁ cT₂ mT₂ eT₂ cZ₂ mZ₂ eZ₂ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {sp lp pp : Cost.Prog} {lam tau n : ℕ} {d : Cost.Data} {s Td T₁ Z₁ T₂ Z₂ : ℕ} {rs₁ rs₂ : List Cost.Data}, 1 ≤ X → 1 ≤ W → d.size + 1 ≤ X → Cost.esize sp ≤ W → Cost.esize lp ≤ W → Cost.esize pp ≤ W → lam ≤ W → tau ≤ W → n ≤ W → s ≤ W → Repetition.reps lam tau n ≤ W → Repeat.Dom W X K cd md ed Td → Repeat.Dom W X K cT₁ mT₁ eT₁ T₁ → Repeat.Dom W X K cZ₁ mZ₁ eZ₁ Z₁ → Repeat.Dom W X K cT₂ mT₂ eT₂ T₂ → Repeat.Dom W X K cZ₂ mZ₂ eZ₂ Z₂ → (Cost.Data.list (lpLenQs (lpSt sp lp pp lam tau n d s))).size ≤ Z₁ → (Cost.Data.list rs₁).size ≤ Z₁ → (Cost.Data.list (lpPQs (lpSt sp lp pp lam tau n d s) rs₁)).size ≤ Z₂ → (Cost.Data.list rs₂).size ≤ Z₂ → Repeat.Dom W X K c m e (lpCoreCost sp lp pp lam tau n d s Td T₁ Z₁ T₂ Z₂ rs₁ rs₂)

The cost of the core is dominated.

The time bound

structure MIPRE.Tailored.RepProg.LpDom {ℓ : ℕ} (S : CL.Sampler ℓ) (L P : Decider) (lam tau n : ℕ) (R : Budget) (W : ℕ) extends MIPRE.Tailored.RepProg.LenDom S L lam tau n R W : Prop

The parameters of the repeated processor at index n, bounded by W.

• S_le : R.S ≤ W
• D_le : R.D ≤ W
• lam_le : lam ≤ W
• tau_le : tau ≤ W
• n_le : n ≤ W
• sizeS_le : Cost.esize S.prog ≤ W
• sizeL_le : Cost.esize L.prog ≤ W
• pow_le : 10 ^ R.k ≤ W
• reps_le : Repetition.reps lam tau n ≤ W
• dim_le : S.dim n ≤ W
• sizeP_le : Cost.esize P.prog ≤ W

theorem MIPRE.Tailored.RepProg.lp_len_calls_le (L : Decider) (n : ℕ) (R : Budget) (hL : L.TimeBoundAt n R.D R.k) (st : LpSt) (hn : st.1.1.2.1 = n) (q : Cost.Data) : q ∈ lpLenQs st → ∃ (r : Cost.Data), Calls.RunsLe Cost.selfUniversal.univ ((Cost.encode L.prog).cons q) r (Polynomial.eval (Cost.esize L.prog + (Cost.esize n + 4 * st.1.1.2.2.size + 6) + R.D * (4 * st.1.1.2.2.size + 6) ^ R.k) Cost.selfUniversal.bound)

The calls to the input calculator, within a common bound.

theorem MIPRE.Tailored.RepProg.lp_p_calls_le (P : Decider) (n : ℕ) (R : Budget) (hP : P.TimeBoundAt n R.D R.k) (st : LpSt) (hn : st.1.1.2.1 = n) (rs : List Cost.Data) (q : Cost.Data) : q ∈ lpPQs st rs → ∃ (r : Cost.Data), Calls.RunsLe Cost.selfUniversal.univ ((Cost.encode P.prog).cons q) r (Polynomial.eval (Cost.esize P.prog + (Cost.esize n + 16 * st.1.1.2.2.size + 12) + R.D * (16 * st.1.1.2.2.size + 12) ^ R.k) Cost.selfUniversal.bound)

The calls to the input processor, within a common bound.

theorem MIPRE.Tailored.RepProg.dom_yCallP : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {p n D : ℕ} {d : Cost.Data}, 1 ≤ X → 10 ^ K ≤ W → p ≤ W → n ≤ W → D ≤ W → d.size + 1 ≤ X → Repeat.Dom W X K c m e (p + (Cost.esize n + 16 * d.size + 12) + D * (16 * d.size + 12) ^ K)

The argument of the processor calls' bound, dominated.

def MIPRE.Tailored.RepProg.zB (M Q T : ℕ) : ℕ

A bound on the queries and results of a loop of at most M calls, queries of size at most Q, results of size at most T.

Equations

• MIPRE.Tailored.RepProg.zB M Q T = M * Q + M + 1 + (M * T + M + 1) + 1

theorem MIPRE.Tailored.RepProg.dom_zB (cM mM eM cQ mQ eQ cT mT eT : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {M Q T : ℕ}, 1 ≤ X → Repeat.Dom W X K cM mM eM M → Repeat.Dom W X K cQ mQ eQ Q → Repeat.Dom W X K cT mT eT T → Repeat.Dom W X K c m e (zB M Q T)

theorem MIPRE.Tailored.RepProg.size_list_le_zB {l : List Cost.Data} {M Q : ℕ} (hl : l.length ≤ M) (h : ∀ q ∈ l, q.size ≤ Q) : (Cost.Data.list l).size ≤ M * Q + M + 1

theorem MIPRE.Tailored.RepProg.repLp_timeBound : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {ℓ : ℕ} (S : CL.Sampler ℓ) (L P : Decider) (lam tau n : ℕ) (R : Budget) (W : ℕ), LpDom S L P lam tau n R W → S.TimeBoundAt n R.S R.k → L.TimeBoundAt n R.D R.k → P.TimeBoundAt n R.D R.k → (repLp S L P lam tau).TimeBoundAt n (c * (W + 1) ^ m) (e * (R.k + 1))

The running time of the repeated processor.