The deterministic time hierarchy theorem (weak form)

Arora–Barak Theorem 3.1 (weak form). If g is clock-constructible and (f(n) + n + 1)² = o(g(n)), then some language is decidable in time O((n + 1)² · (g n + 1)) but not in time O(f).

The witness is the diagonal language diagLang clk of the diagonalizer diagTM clk built from a clock-constructibility witness clk for g:

• Upper bound — diagTM clk itself decides diagLang clk within diagTime C g, which diagTime_le_poly bounds pointwise by (C + 786) · (n + 1)² · (g n + 1).
• Lower bound — if some TM k decided diagLang clk in time O(f), the single-tape reduction would give a decider M₁ : TM 1 at quadratic cost, and padding its description encodeDesc (descOfTM M₁) with junk produces an input x long enough that the simulation budget 16(k+1)(f₀ |x| + |x| + 1)² falls below g |x|. On such an x the diagonalizer flips M₁'s verdict on x itself (diagTM_flips) — contradiction.

Main results

threshold from a big-O bound

• time_hierarchy_weak — the separation, existential form
• time_hierarchy_weak_ssubset — the separation as a strict inclusion DTIME f ⊂ DTIME ((n + 1)² · (g n + 1))
• DTIME_pow_ssubset — concrete polynomial corollary: DTIME((n + 1)^a) ⊂ DTIME((n + 1)^(2a + 5)) for a ≥ 1

theorem Complexity.time_hierarchy_weak {f g : ℕ → ℕ} (hg : TM.ClockConstructible g) (hg1 : ∀ (n : ℕ), 1 ≤ g n) (hfg : LittleO (fun (n : ℕ) => (f n + n + 1) ^ 2) g) : ∃ L ∈ DTIME fun (n : ℕ) => (n + 1) ^ 2 * (g n + 1), L ∉ DTIME f

The deterministic time hierarchy theorem (weak form, AB Theorem 3.1). For clock-constructible g ≥ 1 with (f n + n + 1)² = o(g n), there is a language decidable in time O((n + 1)² · (g n + 1)) but not in time O(f). The (·)² slack absorbs the single-tape reduction; the (n + 1)² factor is the universal machine's per-step cost.

theorem Complexity.time_hierarchy_weak_ssubset {f g : ℕ → ℕ} (hg : TM.ClockConstructible g) (hg1 : ∀ (n : ℕ), 1 ≤ g n) (hfg : LittleO (fun (n : ℕ) => (f n + n + 1) ^ 2) g) : DTIME f ⊂ DTIME fun (n : ℕ) => (n + 1) ^ 2 * (g n + 1)

The time hierarchy theorem as a strict inclusion: DTIME f ⊂ DTIME ((n + 1)² · (g n + 1)) under the same hypotheses.

theorem Complexity.DTIME_pow_ssubset (a : ℕ) (ha : 1 ≤ a) : (DTIME fun (n : ℕ) => (n + 1) ^ a) ⊂ DTIME fun (n : ℕ) => (n + 1) ^ (2 * a + 5)

Polynomial time hierarchy: DTIME((n+1)^a) ⊂ DTIME((n+1)^(2a+5)) for every a ≥ 1. Instantiates the hierarchy theorem at the clock-constructible bound g = (n+1)^(2a+3).