A logarithmic clock for the native time hierarchy

The clock f n * (Nat.size (f n) + 1) eventually exceeds every constant multiple of an at-least-linear f. Its constructibility follows from binary-polynomial postprocessing. Using this clock replaces the earlier inflation (n + 1) * f n by O(f n * log (f n)), which is smaller when f is polynomially bounded.

The resulting hierarchy still pays for the native universal interpreter: the upper bound is (n + 1) ^ 5 * (f n * (Nat.size (f n) + 1) + 1) ^ 3. This is a quantitative improvement in the clock for polynomially bounded f. Hierarchy.TimePolylog combines this clock with the O(t log t) universal simulation, narrowing the gap to a polylogarithmic factor.

Main results

• Cslib.Complexity.eventually_mul_add_le_mul_size_succ: the clock eventually exceeds every c * f n + c.
• Cslib.Complexity.DTIME_ssubset_DTIME_of_log_clock: the native hierarchy with a logarithmically inflated clock.

theorem Cslib.Complexity.eventually_mul_add_le_mul_size_succ {f : ℕ → ℕ} (hn : ∀ (n : ℕ), n ≤ f n) (c : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, c * f n + c ≤ f n * ((f n).size + 1)

The logarithmic clock of an at-least-linear f eventually exceeds every c * f n + c.

theorem Cslib.Complexity.DTIME_ssubset_DTIME_of_log_clock {f g : ℕ → ℕ} (hf : TimeConstructible f) (hn : ∀ (n : ℕ), n ≤ f n) (hg : ∀ᶠ (n : ℕ) in Filter.atTop, (n + 1) ^ 5 * (f n * ((f n).size + 1) + 1) ^ 3 ≤ g n) : DTIME Turing.MultiTapeTM.encBits f ⊂ DTIME Turing.MultiTapeTM.encBits g

The native deterministic hierarchy using a logarithmically inflated clock. The upper bound charges the existing universal interpreter explicitly.