The running time of the repeated answer-length calculator

repLen_timeBound: with the input sampler and calculator within R at index n, the repeated calculator halts on every input (n, d) within c (W + 1)^m (|d| + 1)^{e (R.k + 1)}, for a bound W on the parameters (LenDom) and constants c, m, e independent of everything. The proof follows the stages of lenCore_runsLe: the calls to the input programs are bounded by their time bounds through the universal machine, every query to the calculator being of size linear in |d| (size_lenQs_le), and the polynomial-time stages by dom_poly.

Sizes

theorem MIPRE.Tailored.RepProg.length_rawList_le (d : Cost.Data) : (CL.Detyping.Program.rawList d).length ≤ d.size

theorem MIPRE.Tailored.RepProg.size_treeHead_le (d : Cost.Data) : (Cost.PolyTimeFun.treeHead.toFun d).size ≤ d.size

theorem MIPRE.Tailored.RepProg.length_readQ_le (d : Cost.Data) : List.length (readQ d) ≤ d.size

theorem MIPRE.Tailored.RepProg.mem_lenQs {n : ℕ} {d : Cost.Data} {s k : ℕ} {q : Cost.Data} (hq : q ∈ lenQs n d s k) : ∃ (xi : Cost.BitStr) (b : Bool), q = Cost.encode (n, xi, b) ∧ Cost.esize xi ≤ 4 * d.size + 1

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

theorem MIPRE.Tailored.RepProg.length_lenQs (n : ℕ) (d : Cost.Data) (s k : ℕ) : (lenQs n d s k).length = 2 * k

theorem MIPRE.Tailored.RepProg.esize_bool_le (b : Bool) : Cost.esize b ≤ 3

theorem MIPRE.Tailored.RepProg.esize_dimension : Cost.esize CL.Sampler.Query.dimension ≤ 20

The cost of the core, dominated

theorem MIPRE.Tailored.RepProg.dom_lenCoreCost (cd md ed cT mT eT cZ mZ eZ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {sp lp : Cost.Prog} {lam tau n : ℕ} {d : Cost.Data} {s k Td T Z : ℕ} {rs : List Cost.Data}, 1 ≤ X → 1 ≤ W → d.size + 1 ≤ X → Cost.esize sp ≤ W → Cost.esize lp ≤ W → lam ≤ W → tau ≤ W → n ≤ W → s ≤ W → k ≤ 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 → (Cost.Data.list (lenQs n d s k)).size ≤ Z → (Cost.Data.list rs).size ≤ Z → Repeat.Dom W X K c m e (lenCoreCost sp lp lam tau n d s k Td T Z rs)

The cost of the core is dominated, given dominations of the dimension query's cost Td, the calls' cost T, and the bound Z on the last loop.

The time bound

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

The parameters of the repeated calculator 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

theorem MIPRE.Tailored.RepProg.size_encode_dimension : (Cost.encode CL.Sampler.Query.dimension).size = 9

theorem MIPRE.Tailored.RepProg.dim_univ_le {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) (R : Budget) (hS : S.TimeBoundAt n R.S R.k) : Calls.RunsLe Cost.selfUniversal.univ ((Cost.encode S.prog).cons (Cost.encode (n, CL.Sampler.Query.dimension))) (Cost.encode (S.dim n)) (Polynomial.eval (Cost.esize S.prog + (Cost.esize n + 10) + R.S * 10 ^ R.k) Cost.selfUniversal.bound)

The dimension query through the universal machine, within its bound.

theorem MIPRE.Tailored.RepProg.len_calls_le (L : Decider) (n : ℕ) (R : Budget) (hL : L.TimeBoundAt n R.D R.k) (d : Cost.Data) (s k : ℕ) (q : Cost.Data) : q ∈ lenQs n d s k → ∃ (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 * d.size + 6) + R.D * (4 * d.size + 6) ^ R.k) Cost.selfUniversal.bound)

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

theorem MIPRE.Tailored.RepProg.dom_yCall : ∃ (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 + 4 * d.size + 6) + D * (4 * d.size + 6) ^ K)

The argument of the calls' bound, dominated.

def MIPRE.Tailored.RepProg.lenZ (W n : ℕ) (d : Cost.Data) (T : ℕ) : ℕ

The bound on the queries and results of the loop of calls.

Equations

• MIPRE.Tailored.RepProg.lenZ W n d T = 2 * W * (MIPRE.Cost.esize n + 4 * d.size + 6) + 2 * W + 1 + (2 * W * T + 2 * W + 1) + 1

theorem MIPRE.Tailored.RepProg.dom_lenZ (cT mT eT : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {n T : ℕ} {d : Cost.Data}, 1 ≤ X → n ≤ W → d.size + 1 ≤ X → Repeat.Dom W X K cT mT eT T → Repeat.Dom W X K c m e (lenZ W n d T)

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

The running time of the repeated calculator.