The running time of the detyped decider

The detyped decider (CL.Detyping.DeciderProgram.prog) runs three stages on its input (n, d): the typed sampler on the dimension query, the cutoff routine on n, and the router, which either answers directly or calls the typed decider once, on a typed input whose questions have the typed sampler's dimension and whose answers are within the inner cut (route_call_typed). So its time is dominated in the sense of MIPRE.Pipeline.PDom as soon as the three programs' are, the typed decider's on those inputs only (prog_time).

theorem MIPRE.CL.Detyping.DeciderProgram.route_call_typed {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (n s inner outer : ℕ) (d payload : Cost.Data) (h : (route E).toFun (context ((Cost.encode n).cons d) s inner outer) = (true, payload)) : ∃ (u : T) (v : T) (x : Cost.BitStr) (y : Cost.BitStr) (a : Cost.BitStr) (b : Cost.BitStr), payload = (Cost.encode (n, u, x, v, y, a, b)).cons Cost.Data.nil ∧ List.length x = s ∧ List.length y = s ∧ List.length a ≤ inner ∧ List.length b ≤ inner

The one call of the router is to the typed decider on a typed input, with the index, questions of the typed sampler's dimension and answers within the inner cut, whatever the input.

theorem MIPRE.CL.Detyping.DeciderProgram.prog_time {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] {ℓ : ℕ} (cS mS eS cC mC eC cD mD eD : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W K : ℕ} (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram), ∀ n ≤ W, S.TimeBoundAt n ((cS * (W + 1) ^ mS) ^ (K + 1)) (eS * (K + 1)) → (∀ {X : ℕ}, 1 ≤ X → Pipeline.PRuns W X K cC mC eC C.prog (Cost.encode n) (Cost.encode (C.inner n, C.outer n))) → (∀ {X : ℕ}, 1 ≤ X → ∀ (u v : T) (x y a b : Cost.BitStr), List.length x = S.dim n → List.length y = S.dim n → List.length a ≤ C.inner n → List.length b ≤ C.inner n → ∃ (r : Cost.Data), Pipeline.PRuns W X K cD mD eD D.prog (Cost.encode (n, u, x, v, y, a, b)) r) → (decider E S D C).TimeBoundAt n ((c * (W + 1) ^ m) ^ (K + 1)) (e * (K + 1))

The running time of the detyped decider: dominated as soon as the typed sampler runs within (cS (W + 1)^{mS})^{K + 1} at degree eS (K + 1) at n, the cutoff routine within a dominated time, and the typed decider within one on the typed inputs the router hands it.

theorem MIPRE.CL.Detyping.samplerCoefficient_eq {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (n B k : ℕ) : samplerCoefficient E n B k = Polynomial.eval (Cost.esize n + 2) (Cost.Prog.routeCost (Program.route E) (Program.post (graphDim T)) B k)

The detyped sampler's coefficient is its runtime polynomial's value at 1: the router's cost at the size of the index.

theorem MIPRE.CL.Detyping.sampler_time {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (cS mS eS : ℕ) : ∃ (c : ℕ) (m : ℕ) (d : ℕ), ∀ {W K : ℕ} (S : TypedSampler ℓ T) (hℓ : 0 < ℓ), ∀ n ≤ W, S.TimeBoundAt n ((cS * (W + 1) ^ mS) ^ (K + 1)) (eS * (K + 1)) → (sampler E S hℓ).TimeBoundAt n ((c * (W + 1) ^ m) ^ (K + 1)) (d * (K + 1))

The running time of the detyped sampler: dominated as soon as the typed sampler's is.