diff --git a/Complexity.lean b/Complexity.lean
index 9262ffb5f..5a871acc3 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1166,6 +1166,7 @@ public import Complexity.Computability.Complexity.Classes.BooleanHierarchy.PH
 public import Complexity.Computability.Complexity.Classes.CeqP
 public import Complexity.Computability.Complexity.Classes.CeqP.Time
 public import Complexity.Computability.Complexity.Classes.Constructible
+public import Complexity.Computability.Complexity.Classes.Constructible.FunctionTime
 public import Complexity.Computability.Complexity.Classes.Constructible.Log
 public import Complexity.Computability.Complexity.Classes.Constructible.TwoPow
 public import Complexity.Computability.Complexity.Classes.Constructible.UnaryClock
@@ -1204,6 +1205,7 @@ 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.Hierarchy.WordRAM
 public import Complexity.Computability.Complexity.Classes.IP
 public import Complexity.Computability.Complexity.Classes.IP.CoinFixing
 public import Complexity.Computability.Complexity.Classes.IP.GameTree
@@ -1375,6 +1377,7 @@ public import Complexity.Computability.Complexity.Classes.Time.AcceptCount
 public import Complexity.Computability.Complexity.Classes.Time.BoundedExists
 public import Complexity.Computability.Complexity.Classes.Time.Polynomial
 public import Complexity.Computability.Complexity.Classes.Time.Verifier
+public import Complexity.Computability.Complexity.Classes.Time.WordRAM
 public import Complexity.Computability.Complexity.Classes.Toda
 public import Complexity.Computability.Complexity.Classes.Toda.Counting
 public import Complexity.Computability.Complexity.Classes.Toda.Hierarchy
diff --git a/Complexity/Computability/Complexity/Classes/Constructible/FunctionTime.lean b/Complexity/Computability/Complexity/Classes/Constructible/FunctionTime.lean
new file mode 100644
index 000000000..6211579d5
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/Constructible/FunctionTime.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.Constructible
+public import Complexity.Computability.Complexity.Classes.FunctionTime
+
+/-!
+# Constructible bounds in function time
+
+A time-constructible bound `T` is computed in binary within time `O(T n)` from any word of length
+`n`. Run on the encoding of an instance, the same machine computes `T |enc a|` in
+`FTIME enc encNat T`, for every input encoding `enc`. Clocked simulations use this to compute
+their clock from the input.
+
+## Main results
+
+* `Cslib.Complexity.TimeConstructible.mem_FTIME`: a time-constructible bound of the encoded
+  length is in function time.
+-/
+
+public section
+
+namespace Cslib.Complexity
+
+open Turing.MultiTapeTM
+
+variable {α : Type} {enc : α ↪ List Bool}
+
+/-- **A time-constructible bound is computed within its own time.** For every input encoding
+`enc`, the bound `T |enc a|` of the encoded length is in `FTIME enc encNat T`. -/
+theorem TimeConstructible.mem_FTIME {T : ℕ → ℕ} (hT : TimeConstructible T) :
+    (fun a => T (enc a).length) ∈ FTIME enc encNat T := by
+  obtain ⟨c, s, K, Q, hQ, tm, htm⟩ := hT
+  exact ⟨c, c, s, K, Q, hQ, tm, fun a => htm (enc a)⟩
+
+end Cslib.Complexity
diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/WordRAM.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/WordRAM.lean
new file mode 100644
index 000000000..18a6d4c49
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/Hierarchy/WordRAM.lean
@@ -0,0 +1,172 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.Time.WordRAM
+import Complexity.Computability.Complexity.Classes.Constructible.Log
+import Complexity.Computability.Complexity.Classes.Hierarchy.TimePolylog
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
+import Complexity.Foundations.Data.Nat.PolynomialBound.Closure
+import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
+
+/-!
+# A time hierarchy for the word RAM
+
+For a time-constructible, polynomially bounded `T` with `n ≤ T n`, some problem is decided by one
+fixed word-RAM program over `Basis.additive` within `O(T(n) ^ 5)` instructions, at logarithmic
+word sizes, and by no such program within `O(T n)` instructions
+(`Cslib.WordRAM.exists_mem_RAMTIME_pow_five_notMem_RAMTIME`). Equivalently,
+`RAMTIME .additive encBits T ⊂ RAMTIME .additive encBits (T ^ 5)`
+(`Cslib.WordRAM.RAMTIME_ssubset_RAMTIME_pow_five`).
+
+The proof composes the two simulations of
+`Complexity.Computability.Complexity.Classes.Time.WordRAM` with the time hierarchy for multi-tape
+Turing machines. A program in time `O(T)` is simulated in
+`DTIME ((n + T n + 1) ^ 4 * (Nat.size n + 1) ^ 3)`, that is `O(T⁴ log³ T)`. The
+polylogarithmic-gap hierarchy (`Cslib.Complexity.exists_DTIME_not_subset_DTIME_of_clock_polylog`),
+with the clock `(T n * (Nat.size (T n) + 1)) ^ 4`, gives a problem in `DTIME (T ^ 5)` outside that
+class. It is in `RAMTIME (T ^ 5)` by the linear simulation of machines, since `T ^ 5` is
+polynomially bounded.
+
+The exponent `5` is an artifact of the composition. The exponent `4` of the Turing-machine
+simulation of the word RAM comes from the simulator's association-list memory, and the fifth
+factor absorbs the logarithms and the polylogarithmic gap of the universal machine. For their RAM
+model, with instruction costs `l(n)`, Cook and Reckhow diagonalize over RAMs directly and need only
+`liminf T₁ n / T₂ n = 0` [Cook and Reckhow, abstract][CookReckhow1973]; that sharper route is not
+attempted here. The lower class is over `Basis.additive`, the basis for which an explicit
+simulation overhead is proved.
+
+## Main results
+
+* `Cslib.WordRAM.exists_mem_RAMTIME_pow_five_notMem_RAMTIME`: a problem in word-RAM time
+  `O(T ^ 5)` and not in word-RAM time `O(T)`.
+* `Cslib.WordRAM.RAMTIME_ssubset_RAMTIME_pow_five`: the hierarchy as a strict inclusion.
+
+## References
+
+* [S. A. Cook and R. A. Reckhow, *Time bounded random access machines*][CookReckhow1973]
+-/
+
+public section
+
+namespace Cslib.WordRAM
+
+open Cslib.Complexity Filter Turing.MultiTapeTM
+
+/-- The clock `(m * (Nat.size m + 1)) ^ 4` beats `c * (n + m + 1) ^ 4 * (Nat.size n + 1) ^ 3 + c`
+for `n ≤ m` once `Nat.size m` exceeds `82 * c`. -/
+private theorem mul_overhead_add_le_clock (c : ℕ) {n m : ℕ} (hnm : n ≤ m)
+    (hm : max 1 (2 ^ (82 * c)) ≤ m) :
+    c * ((n + m + 1) ^ 4 * (Nat.size n + 1) ^ 3) + c ≤ (m * (Nat.size m + 1)) ^ 4 := by
+  have hm1 : 1 ≤ m := (le_max_left _ _).trans hm
+  have hsize : 82 * c < Nat.size m := Nat.lt_size.mpr ((le_max_right _ _).trans hm)
+  have hsn : Nat.size n ≤ Nat.size m := Nat.size_le_size hnm
+  have hX : 1 ≤ m ^ 4 * (Nat.size m + 1) ^ 3 :=
+    Nat.mul_pos (Nat.pow_pos hm1) (Nat.pow_pos (Nat.succ_pos _))
+  have hf : (n + m + 1) ^ 4 * (Nat.size n + 1) ^ 3 ≤ 81 * (m ^ 4 * (Nat.size m + 1) ^ 3) := by
+    calc _ ≤ (3 * m) ^ 4 * (Nat.size m + 1) ^ 3 := by gcongr; omega
+      _ = _ := by ring
+  calc c * ((n + m + 1) ^ 4 * (Nat.size n + 1) ^ 3) + c
+      ≤ c * (81 * (m ^ 4 * (Nat.size m + 1) ^ 3)) + c * (m ^ 4 * (Nat.size m + 1) ^ 3) :=
+        Nat.add_le_add (Nat.mul_le_mul_left c hf) (Nat.le_mul_of_pos_right c hX)
+    _ = 82 * c * (m ^ 4 * (Nat.size m + 1) ^ 3) := by ring
+    _ ≤ (Nat.size m + 1) * (m ^ 4 * (Nat.size m + 1) ^ 3) := Nat.mul_le_mul_right _ (by omega)
+    _ = (m * (Nat.size m + 1)) ^ 4 := by ring
+
+/-- For every `k`, the bound of the polylogarithmic-gap hierarchy for the clock
+`J = (m * (Nat.size m + 1)) ^ 4`, `n + (log (n + 1) + 1) ^ k * (J + 1) * (log (J + 1) + 1)`, is
+at most `m ^ 5` for `n ≤ m` and large `m`. -/
+private theorem exists_polylogBound_clock_le_pow_five (k : ℕ) : ∃ M, ∀ {n m : ℕ}, n ≤ m → M ≤ m →
+    n + (Nat.log 2 (n + 1) + 1) ^ k *
+      (((m * (Nat.size m + 1)) ^ 4 + 1) * (Nat.log 2 ((m * (Nat.size m + 1)) ^ 4 + 1) + 1)) ≤
+      m ^ 5 := by
+  obtain ⟨L₀, hL₀⟩ := eventually_atTop.mp
+    (PolynomiallyBounded.eventually_lt_two_pow (f := fun L => 34 * (L + 1) ^ (k + 5))
+      (by fun_prop))
+  refine ⟨max 1 (2 ^ L₀), fun {n m} hnm hm => ?_⟩
+  have hm1 : 1 ≤ m := (le_max_left _ _).trans hm
+  have hL : L₀ < Nat.size m := Nat.lt_size.mpr ((le_max_right _ _).trans hm)
+  -- `2 ^ size m ≤ 2 m`, so `34 (size m + 1) ^ (k + 5) < 2 m`.
+  have hpow : 2 ^ Nat.size m ≤ 2 * m := by
+    have : 2 ^ (Nat.size m - 1) ≤ m := Nat.lt_size.mp (by omega)
+    calc 2 ^ Nat.size m = 2 * 2 ^ (Nat.size m - 1) := by
+          rw [← pow_succ']
+          congr 1
+          omega
+      _ ≤ 2 * m := by omega
+  have hY := hL₀ (Nat.size m) hL.le
+  have hlt : m < 2 ^ Nat.size m := Nat.lt_size_self m
+  have hℓ : Nat.size m + 1 ≤ 2 ^ Nat.size m := Nat.lt_two_pow_self
+  have hlogn : Nat.log 2 (n + 1) ≤ Nat.size m := by
+    calc Nat.log 2 (n + 1) ≤ Nat.log 2 (2 ^ Nat.size m) := Nat.log_mono_right (by omega)
+      _ = Nat.size m := Nat.log_pow (by norm_num) _
+  have hJ : (m * (Nat.size m + 1)) ^ 4 + 1 ≤ 2 ^ (8 * Nat.size m) := by
+    have h₁ : m * (Nat.size m + 1) < 2 ^ Nat.size m * 2 ^ Nat.size m :=
+      Nat.mul_lt_mul_of_lt_of_le hlt hℓ (Nat.pow_pos (by norm_num))
+    have h₂ : (m * (Nat.size m + 1)) ^ 4 < (2 ^ Nat.size m * 2 ^ Nat.size m) ^ 4 :=
+      Nat.pow_lt_pow_left h₁ (by norm_num)
+    calc _ ≤ (2 ^ Nat.size m * 2 ^ Nat.size m) ^ 4 := h₂
+      _ = 2 ^ (8 * Nat.size m) := by rw [← pow_add, ← pow_mul]; ring_nf
+  have hlogJ : Nat.log 2 ((m * (Nat.size m + 1)) ^ 4 + 1) ≤ 8 * Nat.size m := by
+    calc _ ≤ Nat.log 2 (2 ^ (8 * Nat.size m)) := Nat.log_mono_right hJ
+      _ = 8 * Nat.size m := Nat.log_pow (by norm_num) _
+  have hJ2 : (m * (Nat.size m + 1)) ^ 4 + 1 ≤ 2 * (m ^ 4 * (Nat.size m + 1) ^ 4) := by
+    have : 1 ≤ m ^ 4 * (Nat.size m + 1) ^ 4 :=
+      Nat.mul_pos (Nat.pow_pos hm1) (Nat.pow_pos (Nat.succ_pos _))
+    rw [mul_pow]
+    omega
+  have hm4 : m ≤ m ^ 4 := Nat.le_self_pow (by norm_num) _
+  have hY1 : 1 ≤ (Nat.size m + 1) ^ (k + 5) := Nat.pow_pos (Nat.succ_pos _)
+  calc n + (Nat.log 2 (n + 1) + 1) ^ k *
+        (((m * (Nat.size m + 1)) ^ 4 + 1) * (Nat.log 2 ((m * (Nat.size m + 1)) ^ 4 + 1) + 1))
+      ≤ m + (Nat.size m + 1) ^ k *
+          ((2 * (m ^ 4 * (Nat.size m + 1) ^ 4)) * (8 * (Nat.size m + 1))) := by
+        gcongr
+        omega
+    _ = m + 16 * (Nat.size m + 1) ^ (k + 5) * m ^ 4 := by ring
+    _ ≤ m ^ 4 + 16 * (Nat.size m + 1) ^ (k + 5) * m ^ 4 := Nat.add_le_add_right hm4 _
+    _ = (1 + 16 * (Nat.size m + 1) ^ (k + 5)) * m ^ 4 := by ring
+    _ ≤ m * m ^ 4 := Nat.mul_le_mul_right _ (by omega)
+    _ = m ^ 5 := by ring
+
+/-- **A time hierarchy for the word RAM.** For a time-constructible, polynomially bounded `T` with
+`n ≤ T n`, some problem is decided by one fixed program over `Basis.additive` within `O(T(n) ^ 5)`
+instructions at logarithmic word sizes, and by no fixed program over `Basis.additive` within
+`O(T n)` instructions at logarithmic word sizes. -/
+theorem exists_mem_RAMTIME_pow_five_notMem_RAMTIME {T : ℕ → ℕ} (hT : TimeConstructible T)
+    (hn : ∀ n, n ≤ T n) (hpoly : PolynomiallyBounded T) :
+    ∃ A : Set (List Bool), A ∈ RAMTIME .additive encBits (fun n => T n ^ 5) ∧
+      A ∉ RAMTIME .additive encBits T := by
+  obtain ⟨k, hk⟩ := exists_DTIME_not_subset_DTIME_of_clock_polylog
+  obtain ⟨M, hM⟩ := exists_polylogBound_clock_le_pow_five k
+  have hpow : Turing.MultiTapeTM.ComputableInPolyTime (fun m : ℕ => m ^ 4) encNat encNat :=
+    ComputableInPolyTime.binary_pow' ComputableInPolyTime.id' (ComputableInPolyTime.const 4)
+  have hJ : TimeConstructible fun n => (T n * (Nat.size (T n) + 1)) ^ 4 :=
+    hT.mul_size_succ.comp_of_computableInPolyTime hpow fun n => Nat.le_self_pow (by norm_num) _
+  have hsep := hk (f := fun n => (n + T n + 1) ^ 4 * (Nat.size n + 1) ^ 3)
+    (g := fun n => T n ^ 5) hJ
+    (fun c => Eventually.frequently <| by
+      filter_upwards [eventually_ge_atTop (max 1 (2 ^ (82 * c)))] with n hc
+      exact mul_overhead_add_le_clock c (hn n) (hc.trans (hn n)))
+    (by
+      filter_upwards [eventually_ge_atTop M] with n hM'
+      exact hM (hn n) (hM'.trans (hn n)))
+  obtain ⟨A, hAg, hAf⟩ := Set.not_subset.mp hsep
+  exact ⟨A, DTIME_subset_RAMTIME_additive (by fun_prop) hAg,
+    fun h => hAf (RAMTIME_additive_subset_DTIME hT h)⟩
+
+/-- **The word-RAM time hierarchy as a strict inclusion.** For a time-constructible, polynomially
+bounded `T` with `n ≤ T n`, `RAMTIME .additive encBits T ⊂ RAMTIME .additive encBits (T ^ 5)`. -/
+theorem RAMTIME_ssubset_RAMTIME_pow_five {T : ℕ → ℕ} (hT : TimeConstructible T)
+    (hn : ∀ n, n ≤ T n) (hpoly : PolynomiallyBounded T) :
+    RAMTIME .additive encBits T ⊂ RAMTIME .additive encBits fun n => T n ^ 5 := by
+  obtain ⟨A, hA, hA'⟩ := exists_mem_RAMTIME_pow_five_notMem_RAMTIME hT hn hpoly
+  exact (Set.ssubset_iff_of_subset
+    (RAMTIME_mono fun n => Nat.le_self_pow (by norm_num) _)).mpr ⟨A, hA, hA'⟩
+
+end Cslib.WordRAM
diff --git a/Complexity/Computability/Complexity/Classes/Time/WordRAM.lean b/Complexity/Computability/Complexity/Classes/Time/WordRAM.lean
new file mode 100644
index 000000000..c8dd5f1a3
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/Time/WordRAM.lean
@@ -0,0 +1,176 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.Constructible
+public import Complexity.Computability.Complexity.Classes.FunctionTime.WordRAM
+public import Complexity.Computability.WordRAM.MapOp
+public import Complexity.Computability.WordRAM.OfTuring
+import Complexity.Computability.Complexity.Classes.Constructible.FunctionTime
+import Complexity.Computability.Complexity.Classes.Constructible.Log
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryPrimitives
+import Complexity.Foundations.Data.Nat.PolynomialBound.Closure
+
+/-!
+# Deterministic time on the word RAM
+
+`Cslib.WordRAM.RAMTIME B enc T` is the class of problems decided by one fixed word-RAM program over
+the basis `B` within `c * T n + c` instructions, for a constant `c`, on instances whose encoding
+under `enc` has length `n`, at every word size of at least the logarithmic threshold
+`logWidth k n`, for a constant `k > 0`. The conventions are those of
+`Cslib.WordRAM.UniformPolynomialTime` in `Complexity.Computability.Complexity.Classes.P.WordRAM`:
+the input words are the bits `(enc a).map Bool.toNat`, and the size is `|enc a|`. The program may
+read the word size; the time bound does not depend on it.
+
+The two simulations between the word RAM and multi-tape Turing machines relate `RAMTIME` to
+`Cslib.Complexity.DTIME`:
+
+* **RAM ⇒ TM.** For a time-constructible `T`, a program over `Basis.additive` in time `O(T)` is
+  simulated by a machine in time `O((n + T n + 1) ^ 4 * (log n + 1) ^ 3)`
+  (`Cslib.WordRAM.RAMTIME_additive_subset_DTIME`). This is the explicit overhead of
+  `Cslib.WordRAM.Program.DecidesInTime.mem_DTIME`, run on the clock `(c + 1) * (T n + 1)`, with
+  the constants `c` and `k` absorbed into the `DTIME` constant.
+* **TM ⇒ RAM.** For a polynomially bounded `g`, a machine in time `O(g)` is simulated by a program
+  over `Basis.additive` in time `O(g)` (`Cslib.WordRAM.DTIME_subset_RAMTIME_additive`), the
+  simulation of `Cslib.WordRAM.OfTuring.executes_simProgram`. The polynomial bound is needed for
+  logarithmic words to hold the addresses of the simulated tapes.
+
+## Main definitions
+
+* `Cslib.WordRAM.RAMTIME`: deterministic time on the word RAM.
+
+## Main results
+
+* `Cslib.WordRAM.RAMTIME_mono`, `Cslib.WordRAM.RAMTIME_subset_of_hom`: monotonicity in the time
+  bound and in the basis.
+* `Cslib.WordRAM.RAMTIME_additive_subset_DTIME`: word-RAM time in deterministic time.
+* `Cslib.WordRAM.DTIME_subset_RAMTIME_additive`: deterministic time in word-RAM time.
+
+## References
+
+* [S. A. Cook and R. A. Reckhow, *Time bounded random access machines*][CookReckhow1973]
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM
+
+open Turing.MultiTapeTM Cslib.Complexity
+
+variable {α : Type} {enc : α ↪ List Bool}
+
+/-- **Deterministic time on the word RAM.** The problems decided by one fixed program over the
+basis `B` within `c * T n + c` instructions, for a constant `c`, on the bits of an instance whose
+encoding under `enc` has length `n`, at every word size of at least `logWidth k n`, for a constant
+`k > 0`. -/
+def RAMTIME (B : Basis) (enc : α ↪ List Bool) (T : ℕ → ℕ) : Set (Set α) :=
+  {A | ∃ c, UniformDecidableInTimeLogWord B A (fun _ a => (enc a).map Bool.toNat)
+    (fun a => (enc a).length) fun a _ => c * T (enc a).length + c}
+
+/-- `RAMTIME` is monotone in the time bound. -/
+theorem RAMTIME_mono {B : Basis} {T₁ T₂ : ℕ → ℕ} (h : ∀ n, T₁ n ≤ T₂ n) :
+    RAMTIME B enc T₁ ⊆ RAMTIME B enc T₂ := by
+  rintro A ⟨c, k, hk, hd⟩
+  exact ⟨c, k, hk, hd.mono (fun a _ => Nat.add_le_add_right (Nat.mul_le_mul_left _ (h _)) _)
+    fun _ _ hw => hw⟩
+
+/-- `RAMTIME` grows with the basis. -/
+theorem RAMTIME_subset_of_hom {B B' : Basis} (φ : B.Hom B') {T : ℕ → ℕ} :
+    RAMTIME B enc T ⊆ RAMTIME B' enc T := by
+  rintro A ⟨c, k, hk, hd⟩
+  exact ⟨c, k, hk, hd.mapOp φ⟩
+
+/-! ## Word-RAM time in deterministic time -/
+
+/-- **Word-RAM time in deterministic time.** For a time-constructible `T`, a problem decided by a
+fixed program over `Basis.additive` in time `O(T n)` at logarithmic word sizes is in
+`DTIME ((n + T n + 1) ^ 4 * (Nat.size n + 1) ^ 3)`. For `n ≤ T n` this is
+`O(T(n) ^ 4 log³ n)`. -/
+theorem RAMTIME_additive_subset_DTIME {T : ℕ → ℕ} (hT : TimeConstructible T) :
+    RAMTIME .additive enc T ⊆
+      DTIME enc fun n => (n + T n + 1) ^ 4 * (Nat.size n + 1) ^ 3 := by
+  rintro A ⟨c, k, hk, r, p, hp⟩
+  -- Run the simulation on the clock `(c + 1) * (T n + 1)`, which dominates `c * T n + c`.
+  have hg : Turing.MultiTapeTM.ComputableInPolyTime (fun m : ℕ => (c + 1) * (m + 1)) encNat
+      encNat :=
+    ComputableInPolyTime.binary_mul' (ComputableInPolyTime.const (c + 1))
+      (ComputableInPolyTime.binary_add.comp
+        (ComputableInPolyTime.id'.prod (ComputableInPolyTime.const 1)))
+  have hclock : TimeConstructible fun n => (c + 1) * (T n + 1) :=
+    hT.comp_of_computableInPolyTime hg fun n => by nlinarith
+  have hp' := hp.mono (time' := fun a _ => (c + 1) * (T (enc a).length + 1))
+    (fun a _ => by nlinarith) fun _ _ hw => hw
+  have hA := Program.DecidesInTime.mem_DTIME (T := fun n => (c + 1) * (T n + 1)) hk hp'
+    hclock.mem_FTIME
+  refine DTIME_mono_of_le_mul_add (C := (c + 1) + (c + 2) ^ 4 * (k + 1) ^ 3) (fun n => ?_) hA
+  have hz : 1 ≤ (Nat.size n + 1) ^ 3 := Nat.one_le_pow _ _ (by omega)
+  have h₁ : (c + 1) * (T n + 1) ≤ (c + 1) * ((n + T n + 1) ^ 4 * (Nat.size n + 1) ^ 3) := by
+    refine Nat.mul_le_mul_left _ ?_
+    calc T n + 1 ≤ n + T n + 1 := by omega
+      _ ≤ (n + T n + 1) ^ 4 := Nat.le_self_pow (by norm_num) _
+      _ ≤ _ := Nat.le_mul_of_pos_right _ hz
+  have h₂ : (n + (c + 1) * (T n + 1) + 1) ^ 4 * (k * (Nat.size n + 1) + 1) ^ 3 ≤
+      (c + 2) ^ 4 * (k + 1) ^ 3 * ((n + T n + 1) ^ 4 * (Nat.size n + 1) ^ 3) := by
+    calc _ ≤ ((c + 2) * (n + T n + 1)) ^ 4 * ((k + 1) * (Nat.size n + 1)) ^ 3 := by
+          gcongr
+          · nlinarith
+          · nlinarith
+      _ = _ := by ring
+  calc (c + 1) * (T n + 1) + (n + (c + 1) * (T n + 1) + 1) ^ 4 * (k * (Nat.size n + 1) + 1) ^ 3
+      ≤ (c + 1) * ((n + T n + 1) ^ 4 * (Nat.size n + 1) ^ 3) +
+          (c + 2) ^ 4 * (k + 1) ^ 3 * ((n + T n + 1) ^ 4 * (Nat.size n + 1) ^ 3) :=
+        Nat.add_le_add h₁ h₂
+    _ = ((c + 1) + (c + 2) ^ 4 * (k + 1) ^ 3) * ((n + T n + 1) ^ 4 * (Nat.size n + 1) ^ 3) := by
+        ring
+    _ ≤ _ := Nat.le_add_right _ _
+
+/-! ## Deterministic time in word-RAM time -/
+
+section OfTuring
+
+open OfTuring
+
+/-- **Deterministic time in word-RAM time.** For a polynomially bounded `g`, a problem in
+`DTIME g` is decided by one fixed program over `Basis.additive` within `O(g n)` instructions at
+every word size above a logarithmic threshold: the simulator of a machine deciding it
+(`Cslib.WordRAM.OfTuring.simProgram`), run on the bits of the instance. -/
+theorem DTIME_subset_RAMTIME_additive {g : ℕ → ℕ} (hg : PolynomiallyBounded g) :
+    DTIME enc g ⊆ RAMTIME .additive enc g := by
+  rintro A ⟨c₁, c₂, s, hA⟩
+  obtain ⟨f, ⟨K, Q, hfin, tm, htm⟩, hfA⟩ := decidableInTimeAndSpace_iff.mp hA
+  have := Fintype.ofFinite Q
+  -- The words of the simulator stay below `D (n + 1) ^ e`.
+  have hS : PolynomiallyBounded fun n => simBound K (Fintype.card Q) n (c₁ * g n + c₂) := by
+    unfold simBound
+    fun_prop
+  obtain ⟨D, e, hD⟩ := polynomiallyBounded_iff_le.1 hS
+  refine ⟨(c₁ + c₂) * (stepCost K (Fintype.card Q) + 2) + 2 * K + 13, D + e + 2, by omega,
+    regs K, simProgram tm.tr tm.q₀ (Fintype.equivFin Q), fun a w hw _ => ?_⟩
+  obtain ⟨hhalt, hout⟩ := (htm a).runFrom_of_le le_rfl
+  have hb : simBound K (Fintype.card Q) (enc a).length (c₁ * g (enc a).length + c₂) < 2 ^ w :=
+    calc _ ≤ D * ((enc a).length + 1) ^ e := hD _
+      _ < 2 ^ logWidth (D + e) (enc a).length := lt_two_pow_logWidth _ _ _
+      _ ≤ 2 ^ w := Nat.pow_le_pow_right (by norm_num)
+        ((logWidth_mono (by omega) le_rfl).trans hw)
+  have hw2 : 2 ≤ w := le_trans (by unfold logWidth; nlinarith) hw
+  obtain ⟨n, hn, hex⟩ := executes_simProgram (fun _ _ _ => rfl) (Fintype.equivFin Q) hhalt hb
+    (by rw [hout]; simp only [encBool_apply, List.length_singleton]; omega)
+  rw [hout, encBool_apply, Cslib.BitString.lsbValue_singleton] at hex
+  refine ⟨(f a).toNat, n, hex, hn.trans ?_, Bool.toNat_le _, ?_⟩
+  · unfold simTime
+    dsimp only
+    nlinarith [Nat.zero_le (c₂ * (stepCost K (Fintype.card Q) + 2) * g (enc a).length),
+      Nat.zero_le (c₁ * (stepCost K (Fintype.card Q) + 2)),
+      Nat.zero_le ((2 * K + 13) * g (enc a).length)]
+  · rw [hfA a]
+    cases f a <;> simp
+
+end OfTuring
+
+end Cslib.WordRAM
diff --git a/ComplexityTests/WordRAMTimeHierarchy.lean b/ComplexityTests/WordRAMTimeHierarchy.lean
new file mode 100644
index 000000000..f720c9091
--- /dev/null
+++ b/ComplexityTests/WordRAMTimeHierarchy.lean
@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Complexity.Classes.Hierarchy.WordRAM
+import Complexity.Foundations.Data.Nat.PolynomialBound.Closure
+
+/-!
+# Word-RAM time classes and their hierarchy
+
+A two-instruction program puts `Set.univ` in constant word-RAM time. The two simulations and the
+hierarchy are instantiated at the quadratic bound `(n + 1) ^ 2`: quadratic word-RAM time over
+`Basis.additive` is strictly contained in word-RAM time `(n + 1) ^ 10`.
+-/
+
+namespace ComplexityTests.WordRAMTimeHierarchy
+
+open Cslib Cslib.WordRAM Cslib.Complexity Turing.MultiTapeTM
+
+/-! ## A member of a word-RAM time class -/
+
+/-- Write `1` and return it. -/
+def acceptProgram : Program .additive 1 := [.op (.const 0 1), .halt 0]
+
+/-- **`Set.univ` is in constant word-RAM time**, by a two-instruction program. -/
+example : (Set.univ : Set (List Bool)) ∈ RAMTIME .additive encBits fun _ => 1 := by
+  refine ⟨2, 1, Nat.one_pos, 1, acceptProgram, fun l w hw _ => ?_⟩
+  have hw1 : 1 ≤ w := le_trans (by simp [logWidth]) hw
+  have h1 : Fits w 1 := fits_iff.mpr (Nat.one_lt_two_pow (by omega))
+  refine ⟨1, 2, ?_, by norm_num, le_rfl, by simp⟩
+  refine .of_run (fuel := 2) ?_
+  simp [run, Cslib.WordRAM.step, WordSizeDependentProgram.const, acceptProgram, Op.eval,
+    State.init, Data.put, h1]
+
+/-! ## The two simulations at a quadratic bound -/
+
+/-- Quadratic word-RAM time over `Basis.additive` is in deterministic time
+`O((n + (n + 1) ^ 2 + 1) ^ 4 * (log n + 1) ^ 3)`. -/
+example : RAMTIME .additive encBits (fun n => (n + 1) ^ 2) ⊆
+    DTIME encBits fun n => (n + (n + 1) ^ 2 + 1) ^ 4 * (Nat.size n + 1) ^ 3 :=
+  RAMTIME_additive_subset_DTIME timeConstructible_succ_sq
+
+/-- Deterministic time `(n + 1) ^ 10` is in word-RAM time `(n + 1) ^ 10` over `Basis.additive`. -/
+example : DTIME encBits (fun n => (n + 1) ^ 10) ⊆ RAMTIME .additive encBits fun n => (n + 1) ^ 10 :=
+  DTIME_subset_RAMTIME_additive (by fun_prop)
+
+/-! ## The hierarchy at a quadratic bound -/
+
+/-- **Some problem is decided in word-RAM time `((n + 1) ^ 2) ^ 5` and not in quadratic word-RAM
+time**, over `Basis.additive`. -/
+example : ∃ A : Set (List Bool), A ∈ RAMTIME .additive encBits (fun n => ((n + 1) ^ 2) ^ 5) ∧
+    A ∉ RAMTIME .additive encBits fun n => (n + 1) ^ 2 :=
+  exists_mem_RAMTIME_pow_five_notMem_RAMTIME timeConstructible_succ_sq (fun n => by nlinarith)
+    (by fun_prop)
+
+/-- **Quadratic word-RAM time is strictly contained in word-RAM time `((n + 1) ^ 2) ^ 5`**, over
+`Basis.additive`. -/
+example : RAMTIME .additive encBits (fun n => (n + 1) ^ 2) ⊂
+    RAMTIME .additive encBits fun n => ((n + 1) ^ 2) ^ 5 :=
+  RAMTIME_ssubset_RAMTIME_pow_five timeConstructible_succ_sq (fun n => by nlinarith) (by fun_prop)
+
+/-- The separating problem is decided over every basis containing `Basis.additive`, such as
+`Basis.standard`. -/
+example : ∃ A : Set (List Bool), A ∈ RAMTIME .standard encBits (fun n => ((n + 1) ^ 2) ^ 5) ∧
+    A ∉ RAMTIME .additive encBits fun n => (n + 1) ^ 2 := by
+  obtain ⟨A, hA, hA'⟩ := exists_mem_RAMTIME_pow_five_notMem_RAMTIME timeConstructible_succ_sq
+    (fun n => by nlinarith) (by fun_prop)
+  exact ⟨A, RAMTIME_subset_of_hom Basis.additiveHomStandard hA, hA'⟩
+
+end ComplexityTests.WordRAMTimeHierarchy
diff --git a/ROADMAP.md b/ROADMAP.md
index 1e06639fc..6054af4ba 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -180,12 +180,14 @@ index links to canonical definitions rather than keeping a second set.
 - **Time hierarchies** ([#1572]): native polynomial padding separates every pair of integer
   degrees `1 ≤ a < b`, in deterministic and in nondeterministic time, and the `O(t log t)`
   universal simulation ([#800]) gives `DTIME f ⊂ DTIME g` for time-constructible `f ≥ n` once
-  `(f + 1) * polylog f ≤ g`, with an absolute exponent (`Hierarchy/TimePolylog`). For
-  nondeterministic time, padding amplifies the coarse lazy-diagonal hierarchy, which separates
-  degree `d` from degree `6 * d + 14`. Remaining targets include the textbook `f log f = o(g)`
-  hierarchy, which needs the diagonal to clock the universal machine's own steps, noninteger
-  polynomial degrees, and sharp nondeterministic and alternating time hierarchies with certified
-  simulators.
+  `(f + 1) * polylog f ≤ g`, with an absolute exponent (`Hierarchy/TimePolylog`). Composing it
+  with the word-RAM simulations gives `RAMTIME T ⊂ RAMTIME T⁵` over `Basis.additive` for
+  polynomial `T` (`Hierarchy/WordRAM`). For nondeterministic time, padding amplifies the coarse
+  lazy-diagonal hierarchy, which separates degree `d` from degree `6 * d + 14`. Remaining targets
+  include the textbook `f log f = o(g)` hierarchy, which needs the diagonal to clock the universal
+  machine's own steps, noninteger polynomial degrees, a word-RAM hierarchy by direct
+  diagonalization with a smaller gap, and sharp nondeterministic and alternating time
+  hierarchies with certified simulators.
 - The space hierarchy for `log n ≤ g n`, which needs a universal simulation that does not hold
   its input.
 - **Space:** Savitch bounds for general space-constructible functions.