feat(universal): simulate t steps in O(t log t) time (#800)

Complexity.lean

@@ -1178,6 +1178,7 @@ public import Complexity.Computability.Complexity.Classes.Hierarchy.Polynomial
 public import Complexity.Computability.Complexity.Classes.Hierarchy.ShortDesc
 public import Complexity.Computability.Complexity.Classes.Hierarchy.Space
 public import Complexity.Computability.Complexity.Classes.Hierarchy.Time
+public import Complexity.Computability.Complexity.Classes.Hierarchy.TimePolylog
 public import Complexity.Computability.Complexity.Classes.IP
 public import Complexity.Computability.Complexity.Classes.IP.CoinFixing
 public import Complexity.Computability.Complexity.Classes.IP.GameTree
@@ -1664,22 +1665,26 @@ public import Complexity.Computability.Machines.Turing.MultiTape.BlockTrace
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Append
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Comp
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.CopyWord
+public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.DivConq
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Encoding
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Foldl
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Id
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Ite
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.IterateWhile
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.MultiPass
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Reverse
+public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.StackLoop
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.StepMachine
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.StreamFold
+public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TakeDropUnary
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormalForm
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyZeroSpace
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Transducer
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.ZipTransducer
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Arith
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Bounds
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Cases
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.FunProp
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Lists
@@ -1898,6 +1903,8 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.Kernel
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelIterateWhile
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelNormalForm
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelOnWords
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelStackLoop
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTakeDropUnary
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTransducer
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelZeroSpace
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelZipTransducer
@@ -1965,6 +1972,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.Prepar
 public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.ReadInput
 public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.RepeatUntilBlank
 public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.RewindWork
+public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.RunsBetween
 public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.Sequential
 public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.Shadow
 public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.Tidy.Basic
@@ -1974,6 +1982,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.Transf
 public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.TransformsWords
 public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileCond
 public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WhileInput
+public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.WordMoves
 public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount
@@ -2037,6 +2046,11 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Universal.PolyT
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.ResourceBound
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Space
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.SpaceBudget
+public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Windowed
+public import Complexity.Computability.Machines.Turing.MultiTape.Universal.WindowedBound
+public import Complexity.Computability.Machines.Turing.MultiTape.Universal.WindowedComplexity
+public import Complexity.Computability.Machines.Turing.MultiTape.Universal.WindowedInit
+public import Complexity.Computability.Machines.Turing.MultiTape.Universal.WindowedParts
 public import Complexity.Computability.Machines.Turing.SingleTape.Partrec
 public import Complexity.Computability.Machines.Turing.SingleTape.PostTuringMachine
 public import Complexity.Computability.Machines.Turing.TM2.ConfigBound

Complexity/Computability/Complexity/Classes/Hierarchy/LogClock.lean

@@ -20,11 +20,13 @@ 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`; it does not prove the textbook logarithmic-overhead
-universal simulation.
+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.
 -/
@@ -35,18 +37,22 @@ namespace Cslib.Complexity
 
 open Turing.MultiTapeTM Filter
 
-/-- The native deterministic hierarchy using a logarithmically inflated clock. The upper bound
-charges the existing universal interpreter explicitly. -/
-theorem DTIME_ssubset_DTIME_of_log_clock {f g : ℕ → ℕ}
-    (hf : TimeConstructible f) (hn : ∀ n, n ≤ f n)
-    (hg : ∀ᶠ n in atTop, (n + 1) ^ 5 * (f n * (Nat.size (f n) + 1) + 1) ^ 3 ≤ g n) :
-    DTIME encBits f ⊂ DTIME encBits g := by
-  refine DTIME_ssubset_DTIME_of_clock hf.mul_size_succ (fun c => ?_) hg
+/-- The logarithmic clock of an at-least-linear `f` eventually exceeds every `c * f n + c`. -/
+theorem eventually_mul_add_le_mul_size_succ {f : ℕ → ℕ} (hn : ∀ n, n ≤ f n) (c : ℕ) :
+    ∀ᶠ n in atTop, c * f n + c ≤ f n * (Nat.size (f n) + 1) := by
   filter_upwards [eventually_ge_atTop (max c (2 ^ c))] with n hnc
   have hcf : c ≤ f n := (le_max_left _ _).trans (hnc.trans (hn n))
   have hsize : c < Nat.size (f n) :=
     Nat.lt_size.mpr ((le_max_right _ _).trans (hnc.trans (hn n)))
   have := Nat.mul_le_mul_left (f n) hsize.le
   nlinarith
 
+/-- The native deterministic hierarchy using a logarithmically inflated clock. The upper bound
+charges the existing universal interpreter explicitly. -/
+theorem DTIME_ssubset_DTIME_of_log_clock {f g : ℕ → ℕ}
+    (hf : TimeConstructible f) (hn : ∀ n, n ≤ f n)
+    (hg : ∀ᶠ n in atTop, (n + 1) ^ 5 * (f n * (Nat.size (f n) + 1) + 1) ^ 3 ≤ g n) :
+    DTIME encBits f ⊂ DTIME encBits g :=
+  DTIME_ssubset_DTIME_of_clock hf.mul_size_succ (eventually_mul_add_le_mul_size_succ hn) hg
+
 end Cslib.Complexity

Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean

@@ -8,8 +8,9 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
-import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible
+import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Transducer
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Streaming
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame
 import Complexity.Computability.Machines.Turing.MultiTape.Universal.Bound
 import Mathlib.Data.Nat.Size
@@ -31,8 +32,8 @@ which is `O(|x|)`. Padded descriptions are short.
 
 * `Cslib.Complexity.Diagonal.shortDesc_eq_decide`: shortness compares the length of the
   description with the number of binary digits of the length of the word.
-* `Cslib.Complexity.Diagonal.computableInO_shortDesc`: shortness is decided within quadratic
-  time and linear space.
+* `Cslib.Complexity.Diagonal.computableInO_shortDesc`: shortness is decided within linear time
+  and space, by halving the length of the word once per bit of the description.
 
 ## References
 
@@ -56,29 +57,135 @@ theorem shortDesc_eq_decide (x : List Bool) :
   rw [shortDesc, encNat_apply, Nat.size_eq_bits_len]
   exact decide_eq_decide.mpr (Nat.lt_size.symm.trans Nat.lt_iff_add_one_le)
 
-/-- Shortness is decided within quadratic time and linear space. -/
-theorem computableInO_shortDesc :
-    ComputableInO shortDesc encBits encBool (fun x => (x.length + 1) ^ 2)
-      fun x => x.length + 1 := by
-  have hu : ComputableInO unframe encBits encBits (fun x => x.length) fun x => x.length :=
-    ComputableInO.of_linear (.of_unframe fun _ => rfl)
-  have ha := ComputableInDegree.unary_succ.inO_one.comp
-    (ComputableInO.lengthUnary.comp hu)
-  have hb := ComputableInO.lengthUnary.comp
-    (ComputableInO.lengthNat.of_enc_eq (encC := encBits)
-      (g := fun x : List Bool => encNat x.length) fun _ => rfl)
-  have h := ComputableInO.unaryLe.comp (ha.prod hb)
-  refine (h.mono 64 (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_
-  · have h₁ := length_unframe_le x
-    have h₂ := Universal.length_encNat_le x.length
-    simp only [Function.comp_apply, length_encPair, encUnary_apply,
-      List.length_replicate] at h₁ h₂ ⊢
+/-! ### Shortness in linear time -/
+
+/-- The transducer halving a unary number: it keeps every second bit. -/
+private def halveT : Transducer Bool Bool where
+  q₀ := false
+  step q _ := (!q, if q then [true] else [])
+  final _ := []
+  length_step_le q _ := by cases q <;> simp
+  length_final_le _ := by simp
+
+private lemma run_halveT (q : Bool) (k : ℕ) :
+    halveT.run q (List.replicate k true) = List.replicate ((k + q.toNat) / 2) true := by
+  induction k generalizing q with
+  | zero => cases q <;> rfl
+  | succ k ih =>
+    rw [List.replicate_succ, Transducer.run_cons, ih]
+    cases q
+    · simp only [halveT, Bool.not_false, Bool.false_eq_true, ↓reduceIte, List.nil_append,
+        Bool.toNat_true, Bool.toNat_false]
+    · have e : (k + 1 + Bool.toNat true) / 2 = (k + Bool.toNat false) / 2 + 1 := by
+        simp only [Bool.toNat_true, Bool.toNat_false]
+        omega
+      rw [e, List.replicate_succ]
+      rfl
+
+/-- The transducer emitting nothing. -/
+private def silentT : Transducer Bool Unit where
+  q₀ := ()
+  step _ _ := ((), [])
+  final _ := []
+  length_step_le _ _ := by simp
+  length_final_le _ := by simp
+
+private lemma run_silentT (w : List Bool) : silentT.run () w = [] := by
+  induction w with
+  | nil => rfl
+  | cons b w ih => exact ih
+
+/-- The transducer reporting whether a unary number is positive. -/
+private def posT : Transducer Bool Bool where
+  q₀ := false
+  step _ _ := (true, [])
+  final q := [q]
+  length_step_le _ _ := by simp
+  length_final_le _ := by simp
+
+private lemma run_posT (q : Bool) (k : ℕ) :
+    posT.run q (List.replicate k true) = [q || decide (0 < k)] := by
+  induction k generalizing q with
+  | zero => simp [posT]
+  | succ k ih =>
+    rw [List.replicate_succ, Transducer.run_cons, ih]
+    simp [posT]
+
+private lemma iterate_div_two (n i : ℕ) : (· / 2)^[i] n = n / 2 ^ i := by
+  induction i with
+  | zero => simp
+  | succ i ih =>
+    rw [Function.iterate_succ_apply', ih, pow_succ, Nat.div_div_eq_div_mul]
+
+private lemma sum_div_two_pow_le (n L : ℕ) : ∑ i ∈ Finset.range L, n / 2 ^ i ≤ 2 * n := by
+  induction L generalizing n with
+  | zero => simp
+  | succ L ih =>
+    rw [Finset.sum_range_succ']
+    have h (i : ℕ) : n / 2 ^ (i + 1) = n / 2 / 2 ^ i := by
+      rw [pow_succ', Nat.div_div_eq_div_mul]
+    simp only [h, pow_zero, Nat.div_one]
+    have := ih (n / 2)
+    omega
+
+/-- Comparing `2 ^ L` with `n`, both in unary, in linear time: `n` is halved `L` times, which costs
+`n + n / 2 + ⋯`, and the result is tested for positivity. -/
+private theorem computableTidilyInO_two_pow_le :
+    ComputableTidilyInO (fun p : ℕ × ℕ => decide (2 ^ p.2 ≤ p.1)) (encPair encUnary encUnary)
+      encBool (fun p => (encPair encUnary encUnary p).length)
+      fun p => (encPair encUnary encUnary p).length := by
+  have hN : ComputableTidilyInTimeAndSpace (· / 2) encUnary encUnary
+      (fun k => 4 * (encUnary k).length + 8) fun _ => 0 :=
+    halveT.computableTidilyInTimeAndSpace fun k => by
+      rw [encUnary_apply, encUnary_apply, run_halveT]
+      rfl
+  have hE : ComputableTidilyInTimeAndSpace (fun _ : ℕ => ([] : List Bool)) encUnary encBits
+      (fun k => 4 * (encUnary k).length + 8) fun _ => 0 :=
+    silentT.computableTidilyInTimeAndSpace fun k => (run_silentT _).symm
+  have hF : ComputableTidilyInTimeAndSpace (fun k : ℕ => [decide (0 < k)]) encUnary encBits
+      (fun k => 4 * (encUnary k).length + 8) fun _ => 0 :=
+    posT.computableTidilyInTimeAndSpace fun k => by
+      rw [encUnary_apply, run_posT]
+      rfl
+  obtain ⟨c, h⟩ := ComputableTidilyInTimeAndSpace.iterate_unary_stream_sum hN hE hF
+    (R := fun x i => 17 * (x.1 / 2 ^ i) + 17) (Q := fun _ => 0) (B := fun x => x.1)
+    (fun x i _ => by
+      simp only [encUnary_apply, List.length_replicate, iterate_div_two]
+      have : x.1 / 2 ^ (i + 1) ≤ x.1 / 2 ^ i :=
+        Nat.div_le_div_left (Nat.pow_le_pow_right (by norm_num) (Nat.le_succ i)) (by positivity)
+      omega)
+    (fun _ _ _ => le_rfl)
+    (fun x i _ => by
+      simp only [encUnary_apply, List.length_replicate, iterate_div_two]
+      exact Nat.div_le_self _ _)
+  refine ComputableTidilyInO.of_bounds (h.of_enc_eq fun p => ?_) (100 * c + 100)
+    (fun p => ?_) (fun p => ?_) fun p => ?_
+  · simp only [encBool_apply, encBits_apply, iterate_div_two, List.map_const',
+      List.flatten_replicate_nil, List.nil_append, List.cons.injEq, and_true]
+    exact decide_eq_decide.mpr (Nat.div_pos_iff.trans (and_iff_right (by positivity))).symm
+  · have hs := sum_div_two_pow_le p.1 p.2
+    have hq : p.1 / 2 ^ p.2 ≤ p.1 := Nat.div_le_self _ _
+    simp only [encUnary_apply, List.length_replicate, iterate_div_two, length_encPair,
+      Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_const, Finset.card_range,
+      smul_eq_mul]
+    nlinarith
+  · simp only [length_encPair, encUnary_apply, List.length_replicate]
     nlinarith
-  · have h₁ := length_unframe_le x
-    have h₂ := Universal.length_encNat_le x.length
-    simp only [Function.comp_apply, length_encPair, encUnary_apply,
-      List.length_replicate] at h₁ h₂ ⊢
+  · simp only [encBool_apply, List.length_singleton]
+    nlinarith
+
+/-- **Shortness is decided within linear time and space.** The length of the word and of the
+framed description are written in unary, and the first is halved once per bit of the second. -/
+theorem computableInO_shortDesc :
+    ComputableInO shortDesc encBits encBool (fun x => x.length) fun x => x.length := by
+  have hu : ComputableTidilyInO unframe encBits encBits (fun x => x.length) fun x => x.length :=
+    ComputableTidilyInO.of_linear (.of_unframe fun _ => rfl)
+  have hl := ComputableInO.lengthUnary.tidy
+  have h := computableTidilyInO_two_pow_le.comp (hl.prod (hl.comp hu))
+  refine (h.mono 8 (fun x => ?_) fun x => ?_).computableInO
+  all_goals
+    have h₁ := length_unframe_le x
+    simp only [Function.comp_apply, length_encPair, encUnary_apply, List.length_replicate] at h₁ ⊢
     omega
-  · simp only [Function.comp_apply, shortDesc_eq_decide]
 
 end Cslib.Complexity.Diagonal

Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean

@@ -60,12 +60,15 @@ Hence `DTIME f ⊂ DTIME g`
   with the clock `(n + 1) * f n` (`Cslib.Complexity.DTIME_ssubset_DTIME`). As `n ≤ f n`, the gap
   `(f n + 1) ^ 11 ≤ g n` suffices.
 
-The polynomial gap is the overhead of the native universal machine, which is polynomial in the
-description and in the clock. The textbook gap `f n * log (f n) = o(g n)` needs a simulation with
-logarithmic overhead and is not claimed here. `Hierarchy.LogClock` reduces the clock inflation
-to `f n * (Nat.size (f n) + 1)`. `Hierarchy.Polynomial` uses native padding to prove strictness
-between every pair of distinct positive integer polynomial degrees, despite this
-interpreter overhead.
+The polynomial gap is the overhead of the polynomial-certificate universal interpreter, which is
+polynomial in the description and in the clock. `Hierarchy.TimePolylog` uses the `O(t log t)`
+universal simulation instead and narrows the gap to a polylogarithmic factor: `g` need only
+eventually exceed `n + (log (n + 1) + 1) ^ k * (J n + 1) * (log (J n + 1) + 1)` for an absolute
+constant `k`, or `(f n + 1) * (log (f n + 1) + 1) ^ k` for a time-constructible `f`. The textbook
+gap `f n * log (f n) = o(g n)` needs the diagonal to clock the universal machine's own steps and is
+not claimed. `Hierarchy.LogClock` reduces the clock inflation to `f n * (Nat.size (f n) + 1)`.
+`Hierarchy.Polynomial` uses native padding to prove strictness between every pair of distinct
+positive integer polynomial degrees, despite this interpreter overhead.
 
 ## Main definitions
 
@@ -396,7 +399,8 @@ theorem DTIME_ssubset_DTIME_of_clock {f g J : ℕ → ℕ} (hJ : TimeConstructib
 /-- **The time hierarchy theorem.** If `f` is time-constructible and `n ≤ f n`, then `DTIME f` is
 strictly contained in every `DTIME g` with `(n + 1) ^ 8 * (f n + 1) ^ 3 ≤ g n` eventually
 [Arora and Barak, Theorem 3.1][AroraBarak09], [Sipser, Theorem 9.10][Sipser2013]. The gap is the
-polynomial overhead of the native universal machine, not the textbook `f n * log (f n)`. -/
+polynomial overhead of the polynomial-certificate universal interpreter;
+`Cslib.Complexity.exists_DTIME_ssubset_DTIME_polylog` narrows it to a polylogarithmic factor. -/
 theorem DTIME_ssubset_DTIME {f g : ℕ → ℕ} (hf : TimeConstructible f) (hn : ∀ n, n ≤ f n)
     (hg : ∀ᶠ n in atTop, (n + 1) ^ 8 * (f n + 1) ^ 3 ≤ g n) :
     DTIME encBits f ⊂ DTIME encBits g := by