diff --git a/Complexity.lean b/Complexity.lean
index 96fe9eb428..ab8cc3ee6e 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2559,6 +2559,8 @@ public import Complexity.Computability.WordRAM.Randomized.UniformLoopExit
 public import Complexity.Computability.WordRAM.Realization.Basic
 public import Complexity.Computability.WordRAM.Realization.Bind
 public import Complexity.Computability.WordRAM.Realization.Branch
+public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueue
+public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueueDispatch
 public import Complexity.Computability.WordRAM.Realization.Client.MemoryStack
 public import Complexity.Computability.WordRAM.Realization.Glue
 public import Complexity.Computability.WordRAM.Realization.GlueVector
diff --git a/Complexity/Computability/WordRAM/Realization/Client/MemoryQueue.lean b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueue.lean
new file mode 100644
index 0000000000..027f71c9e6
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueue.lean
@@ -0,0 +1,546 @@
+/-
+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.WordRAM.Realization.Loop
+public import Complexity.Computability.WordRAM.Realization.Bind
+public import Complexity.Computability.WordRAM.Realization.Reindex
+public import Complexity.Computability.WordRAM.Realization.GlueVector
+public import Complexity.Computability.WordRAM.Realization.Grade
+public import Complexity.Computability.WordRAM.Realization.Client.MemoryStack
+public import Complexity.DataStructure.Queue.Memory
+
+/-!
+# Native consumption of the two-stack memory queue
+
+The existing source transfer stops when a rear pop returns `none`. A bounded native loop keeps
+an explicit active flag: after that result, remaining iterations return the flag without
+queries. Their local work remains charged. One uniform emitter consumes complete runtime
+layouts, the flag and the fuel; it is fixed before the layouts' allocation addresses.
+
+The body composes the existing memory-stack certificates. Both native branches, result copies,
+binds and loop control contribute to the explicit grading. The source program remains the
+queue's linked `transfer`; the domain and cost proofs reuse its storage invariants. A separate
+operation dispatcher and local framed adapter can consume this transfer certificate.
+
+## Main definitions
+
+* `transferBody`, `transferSafe`: one iteration and its actual intermediate memory domains.
+* `layoutWords`, `bodyWords`, `transferWords`: faithful runtime layouts, flag and fuel encodings.
+
+## Main results
+
+* `transfer_eq_iterate`: exact source equality, including early termination.
+* `memMethods_enqueue`, `memMethods_dequeue`: the existing queue methods' source decompositions.
+* `realizes_transferBody`, `realizes_source_transfer`: native certificates with explicit work.
+* `transfer_invariant`: the storage invariants discharge every reached iteration's domain.
+* `source_transfer_cost`, `source_transfer_work_bound`: six memory units per item and a separate
+  envelope paying the certified local work when the fuel is the actual rear count.
+
+## References
+
+The two-stack queue and its semantic potential argument are reused from
+[Cormen, Leiserson, Rivest and Stein, *Introduction to Algorithms*, Exercise 10.1-6 and
+Chapter 17][CLRS2009]. The native realization and local-work grading here are original
+infrastructure over those existing programs.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization.MemoryQueue
+
+open Cslib.DataStructure
+
+/-- One active transfer iteration moves a rear item to the front. Once inactive, the remaining
+bounded iterations perform no memory operation. Both layouts are runtime data. -/
+def transferBody (d : (Stack.Memory.Layout × Stack.Memory.Layout) × Bool) : Memory.Prog Bool :=
+  if d.2 then do
+    let a ← Stack.Memory.pop d.1.2
+    match a with
+    | none => pure false
+    | some v => do
+        Stack.Memory.push d.1.1 v
+        pure true
+  else pure false
+
+/-- Inactive tail iterations issue no memory query and leave the source program pure. -/
+theorem iterate_inactive (L : Stack.Memory.Layout × Stack.Memory.Layout) (n : ℕ) :
+    iterate transferBody L n false = pure false := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simpa [iterate, transferBody] using ih
+
+/-- The source's early stop is represented exactly, rather than replaced by repeated pops on an
+empty rear stack. Inactive native iterations are paid by the loop-work ledger. -/
+theorem transfer_eq_iterate (L₁ L₂ : Stack.Memory.Layout) (w C n : ℕ) :
+    link (Stack.Memory.pairMethods L₁ L₂ w C) (Queue.transfer n) =
+      (iterate transferBody (L₁, L₂) n true).bind (fun _ => pure ()) := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    simp only [Queue.transfer, link, PFunctor.FreeM.liftM, iterate, transferBody]
+    simp only [Stack.Memory.pairMethods, Stack.Memory.methods, ↓reduceIte,
+      PFunctor.FreeM.bind_eq_bind, bind_assoc]
+    congr 1
+    funext a
+    cases a with
+    | none => simp [iterate_inactive]
+    | some v =>
+      simp only [PFunctor.FreeM.liftM]
+      exact congrArg (fun p => (Stack.Memory.push L₁ v).bind (fun _ => p)) ih
+
+/-- Enqueue uses the rear stack's existing push program unchanged. -/
+theorem memMethods_enqueue (L₁ L₂ : Stack.Memory.Layout) (w C v : ℕ) :
+    Queue.Memory.memMethods L₁ L₂ w C (.enqueue v) = Stack.Memory.push L₂ v := by
+  simp only [Queue.Memory.memMethods, Queue.methods, link, PFunctor.FreeM.liftM,
+    Stack.Memory.pairMethods, Stack.Memory.methods]
+  change (Stack.Memory.push L₂ v).bind pure = _
+  exact PFunctor.FreeM.bind_pure _
+
+/-- The existing dequeue dispatches between an immediate front pop and a runtime-sized transfer.
+All layout values and the rear count remain ordinary runtime data. -/
+theorem memMethods_dequeue (L₁ L₂ : Stack.Memory.Layout) (w C : ℕ) :
+    Queue.Memory.memMethods L₁ L₂ w C .dequeue = (do
+      let a ← Stack.Memory.pop L₁
+      match a with
+      | some v => pure (some v)
+      | none => do
+          let n ← Stack.Memory.size L₂
+          let _ ← iterate transferBody (L₁, L₂) n true
+          Stack.Memory.pop L₁) := by
+  simp only [Queue.Memory.memMethods, Queue.methods, link, PFunctor.FreeM.liftM,
+    Stack.Memory.pairMethods, Stack.Memory.methods]
+  congr 1
+  funext a
+  cases a with
+  | some v => rfl
+  | none =>
+    simp only [PFunctor.FreeM.liftM, Stack.Memory.pairMethods, Stack.Memory.methods]
+    congr 1
+    funext n
+    change ℕ at n
+    rw [PFunctor.FreeM.liftM_bind]
+    change (link (Stack.Memory.pairMethods L₁ L₂ w C) (Queue.transfer n)).bind _ = _
+    rw [transfer_eq_iterate]
+    simp only [PFunctor.FreeM.liftM, Stack.Memory.pairMethods, Stack.Memory.methods,
+      PFunctor.FreeM.bind_eq_bind, bind_assoc, pure_bind]
+    change (iterate transferBody (L₁, L₂) n true).bind
+      (fun _ => (Stack.Memory.pop L₁).bind pure) = _
+    rw [PFunctor.FreeM.bind_pure]
+    rfl
+
+/-- Both complete runtime stack layouts, front followed by rear. -/
+def layoutWords : (Stack.Memory.Layout × Stack.Memory.Layout) ↪ (Fin 8 → ℕ) :=
+  (MemoryStack.layoutWords.prodMap MemoryStack.layoutWords).trans
+    (Fin.appendEquiv 4 4).toEmbedding
+
+/-- The two layouts followed by the active Boolean's tag and retained zero word. -/
+def bodyWords : ((Stack.Memory.Layout × Stack.Memory.Layout) × Bool) ↪ (Fin 10 → ℕ) :=
+  (layoutWords.prodMap boolWords).trans (Fin.appendEquiv 8 2).toEmbedding
+
+private def replyWords : (((Stack.Memory.Layout × Stack.Memory.Layout) × Bool) × Option ℕ) ↪
+    (Fin 12 → ℕ) :=
+  (bodyWords.prodMap optionWords).trans (Fin.appendEquiv 10 2).toEmbedding
+
+private theorem body_test (d : (Stack.Memory.Layout × Stack.Memory.Layout) × Bool) :
+    test (.eq 8 9) (bodyWords d) ↔ d.2 = false := by
+  change d.2.toNat = 0 ↔ d.2 = false
+  cases d.2 <;> decide
+
+private theorem reply_test
+    (d : ((Stack.Memory.Layout × Stack.Memory.Layout) × Bool) × Option ℕ) :
+    test (.eq 10 9) (replyWords d) ↔ d.2 = none := by
+  change optionWords d.2 0 = 0 ↔ d.2 = none
+  cases d.2 <;> simp [optionWords]
+
+private theorem returnFlag {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ)) (b : Bool) :
+    Realizes .exact (fun _ => pure b) input boolWords
+      (fun w _ _ => Fits w b.toNat) (fun _ _ => 4) := by
+  let g : Fin 2 → (Fin k → ℕ) → ℕ := fun i _ => boolWords b i
+  have h := Realizes.glueVector (B := .exact) input boolWords (fun _ => b) g g (fun _ => 1)
+    (fun _ _ => rfl) (P := fun _ => True)
+    (fun _ => GlueComputes.const _ (fun _ _ => le_rfl))
+  apply h.consequence (hwork := fun _ _ => by simp)
+  intro w d s _ _ hb
+  refine ⟨trivial, fun i => ?_⟩
+  fin_cases i
+  · exact hb
+  · exact fits_zero w
+
+private theorem returnInactive {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ)) :
+    Realizes .exact (fun _ => pure false) input boolWords
+      (fun _ _ _ => True) (fun _ _ => 4) :=
+  (returnFlag input false).consequence
+    (fun w _ _ _ _ _ => fits_zero w) (fun _ _ => le_rfl)
+
+/-- The visible domains of the actual pop/branch/push composition, at the actual intermediate
+memory. The inactive path has no stack precondition; the true result tag must fit when pushed. -/
+def transferSafe (w : ℕ) (d : (Stack.Memory.Layout × Stack.Memory.Layout) × Bool)
+    (s : Memory.State) : Prop :=
+  if d.2 then
+    d.1.2.Valid w d.1.2.items.length ∧ Stack.Memory.Inv d.1.2 s ∧
+      match (Memory.spec 0).clientResult s (Stack.Memory.pop d.1.2) with
+      | none => True
+      | some _ =>
+          d.1.1.Valid w d.1.1.items.length ∧
+            Stack.Memory.Inv d.1.1 ((Memory.spec 0).clientState s (Stack.Memory.pop d.1.2)) ∧
+            ((Memory.spec 0).clientState s (Stack.Memory.pop d.1.2)).mem d.1.1.count.base <
+              d.1.1.items.length ∧ Fits w 1
+  else True
+
+/-- The transfer body consumes the already certified stack methods. Its constant local-work
+allowance includes pop/push glue, both native conditionals, result copies and every bind. -/
+theorem realizes_transferBody :
+    Realizes .exact transferBody bodyWords boolWords transferSafe (fun _ _ => 39) := by
+  have hpop := MemoryStack.realizes_pop.reindex
+    (fun d : (Stack.Memory.Layout × Stack.Memory.Layout) × Bool => d.1.2)
+    bodyWords ![4, 5, 6, 7] (by intro d i; fin_cases i <;> rfl)
+  have hpush := MemoryStack.realizes_push.reindex
+    (fun d : ((Stack.Memory.Layout × Stack.Memory.Layout) × Bool) × Option ℕ =>
+      (d.1.1.1, d.2.getD 0)) replyWords ![0, 1, 2, 3, 11] (by
+        intro d i
+        fin_cases i <;> try rfl
+        rcases d with ⟨d, a⟩
+        cases a <;> rfl)
+  let pushInput := (replyWords.prodMap
+    (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding).trans
+      (Fin.appendEquiv 12 0).toEmbedding
+  have hsome := (hpush.bind (returnFlag pushInput true)).consequence
+    (safe' := fun w d s => d.1.1.1.Valid w d.1.1.1.items.length ∧
+      Stack.Memory.Inv d.1.1.1 s ∧ s.mem d.1.1.1.count.base < d.1.1.1.items.length ∧ Fits w 1)
+    (work' := fun _ _ => 15)
+    (fun _ _ _ _ _ h => ⟨⟨h.1, h.2.1, h.2.2.1⟩, h.2.2.2⟩)
+    (fun _ _ => le_rfl)
+  have hreply := Realizes.branch (.eq 10 9) (returnInactive replyWords) hsome
+  have hreply_program :
+      (fun d => if test (.eq 10 9) (replyWords d) then (pure false : Memory.Prog Bool)
+        else (Stack.Memory.push d.1.1.1 (d.2.getD 0)).bind (fun _ => pure true)) =
+      (fun d : ((Stack.Memory.Layout × Stack.Memory.Layout) × Bool) × Option ℕ =>
+        match d.2 with
+        | none => pure false
+        | some v => (Stack.Memory.push d.1.1.1 v).bind (fun _ => pure true)) := by
+    funext d
+    rcases d with ⟨⟨⟨L₁, L₂⟩, active⟩, a⟩
+    simp only [reply_test]
+    cases a <;> rfl
+  rw [hreply_program] at hreply
+  have hactive := hpop.bind hreply
+  have houter := Realizes.branch (.eq 8 9) (returnInactive bodyWords) hactive
+  have houter_program :
+      (fun d => if test (.eq 8 9) (bodyWords d) then (pure false : Memory.Prog Bool)
+        else (Stack.Memory.pop d.1.2).bind (fun a => match a with
+          | none => pure false
+          | some v => (Stack.Memory.push d.1.1 v).bind (fun _ => pure true))) =
+      transferBody := by
+    funext d
+    rcases d with ⟨⟨L₁, L₂⟩, active⟩
+    simp only [body_test]
+    cases active <;> rfl
+  rw [houter_program] at houter
+  apply houter.consequence
+  · intro w d s _ _ h
+    rcases d with ⟨⟨L₁, L₂⟩, active⟩
+    simp only [body_test]
+    cases active
+    · trivial
+    · change (L₂.Valid w L₂.items.length ∧ Stack.Memory.Inv L₂ s) ∧ _
+      refine ⟨⟨h.1, h.2.1⟩, ?_⟩
+      cases ha : (Memory.spec 0).clientResult s (Stack.Memory.pop L₂) with
+      | none => simp only [reply_test, ↓reduceIte]
+      | some v =>
+        simpa only [reply_test, ha, reduceCtorEq, ↓reduceIte] using h.2.2
+  · intro d s
+    split
+    · omega
+    · split <;> omega
+
+/-- Runtime layout words, a constant active tag/zero pair, and runtime transfer fuel. -/
+def transferWords {k : ℕ}
+    (input : (Stack.Memory.Layout × Stack.Memory.Layout) ↪ (Fin k → ℕ)) :
+    ((Stack.Memory.Layout × Stack.Memory.Layout) × ℕ) ↪ (Fin (k + 2 + 1) → ℕ) :=
+  (⟨fun d => ((d.1, true), d.2), by
+    intro a b h
+    have hL := congrArg (fun d => d.1.1) h
+    have hn := congrArg Prod.snd h
+    exact Prod.ext hL hn⟩ :
+      ((Stack.Memory.Layout × Stack.Memory.Layout) × ℕ) ↪
+        (((Stack.Memory.Layout × Stack.Memory.Layout) × Bool) × ℕ)).trans
+    (((((input.prodMap boolWords).trans (Fin.appendEquiv k 2).toEmbedding).prodMap
+      (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans
+        (Fin.appendEquiv (k + 2) 1).toEmbedding))
+
+/-- A single uniform body certificate gives the complete existing early-stop transfer program.
+The loop and the final bind are both charged, even on the no-query path. -/
+theorem realizes_transfer {k : ℕ}
+    (input : (Stack.Memory.Layout × Stack.Memory.Layout) ↪ (Fin k → ℕ))
+    {safe : ℕ → ((Stack.Memory.Layout × Stack.Memory.Layout) × Bool) → Memory.State → Prop}
+    {work : ((Stack.Memory.Layout × Stack.Memory.Layout) × Bool) → Memory.State → ℕ}
+    (hbody : Realizes .exact transferBody
+      ((input.prodMap boolWords).trans (Fin.appendEquiv k 2).toEmbedding)
+      boolWords safe work) (w C : ℕ) :
+    Realizes .exact
+      (fun d => link (Stack.Memory.pairMethods d.1.1 d.1.2 w C) (Queue.transfer d.2))
+      (transferWords input) (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+      (fun w d s => iterationSafe transferBody safe w d.1 d.2 true s)
+      (fun d s => iterationWork transferBody work d.1 d.2 true s + 1) := by
+  let hloop := (Realizes.iterateRuntime input boolWords hbody).reindex
+    (fun d : (Stack.Memory.Layout × Stack.Memory.Layout) × ℕ => ((d.1, true), d.2))
+    (transferWords input) id (fun _ _ => rfl)
+  let nextInput := ((transferWords input).prodMap boolWords).trans
+    (Fin.appendEquiv (k + 2 + 1) 2).toEmbedding
+  have hunit : Realizes .exact (fun _ => (pure () : Memory.Prog Unit)) nextInput
+      (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+      (fun _ _ _ => True) (fun _ _ => 0) := by
+    have h := Realizes.glueVector (B := .exact) nextInput
+      (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding (fun _ => ())
+      (fun i => Fin.elim0 i) (fun i => Fin.elim0 i) (fun i => Fin.elim0 i)
+      (P := fun _ => True) (fun _ i => Fin.elim0 i) (fun i => Fin.elim0 i)
+    simpa using h
+  have h := hloop.bind hunit
+  simpa only [hloop, transfer_eq_iterate, and_true, Nat.add_zero] using h
+
+/-- The loop ledger charges every iteration, including pure inactive iterations. -/
+private theorem transfer_work_le (work : ((Stack.Memory.Layout × Stack.Memory.Layout) × Bool) →
+    Memory.State → ℕ) (K : ℕ) (hwork : ∀ d s, work d s ≤ K)
+    (L : Stack.Memory.Layout × Stack.Memory.Layout) (n : ℕ) (active : Bool) (s : Memory.State) :
+    iterationWork transferBody work L n active s ≤ (K + 1) * n := by
+  induction n generalizing active s with
+  | zero => simp [iterationWork]
+  | succ n ih =>
+    rw [iterationWork]
+    have hnext := ih ((Memory.spec 0).clientResult s (transferBody (L, active)))
+      ((Memory.spec 0).clientState s (transferBody (L, active)))
+    have hbody := hwork (L, active) s
+    nlinarith
+
+/-- The actual source transfer has one uniform native emitter before its runtime layouts and
+fuel. Forty local units per iteration pay the certified body and loop control; the final bind
+costs one more. The visible safety predicate follows exactly the reached semantic states. -/
+theorem realizes_source_transfer (w C : ℕ) :
+    Realizes .exact
+      (fun d => link (Stack.Memory.pairMethods d.1.1 d.1.2 w C) (Queue.transfer d.2))
+      (transferWords layoutWords) (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+      (fun w d s => iterationSafe transferBody transferSafe w d.1 d.2 true s)
+      (fun d _ => 40 * d.2 + 1) := by
+  apply (realizes_transfer layoutWords realizes_transferBody w C).consequence
+  · intro _ _ _ _ _ h
+    exact h
+  · intro d s
+    exact Nat.add_le_add_right
+      (transfer_work_le (fun _ _ => 39) 39 (fun _ _ => le_rfl) d.1 d.2 true s) 1
+
+private theorem stack_inv_step {L : Stack.Memory.Layout} {w C : ℕ} (hL : L.Valid w C)
+    {s : Memory.State} (hs : Stack.Memory.Inv L s) (o : Queue.StackOp ℕ)
+    (hv : (Stack.WordRAM.spec w C).valid (Stack.Memory.abs L s) o) :
+    (Memory.spec w).ValidHistory s
+        ((Memory.spec w).clientHistory s (Stack.Memory.methods L w C o)) ∧
+      Stack.Memory.Inv L ((Memory.spec 0).clientState s (Stack.Memory.methods L w C o)) := by
+  let M := Stack.Memory.refinement hL
+  have hvalid := ((Memory.spec w).demonicValid_iff_validHistory_runClient _ _).mp
+    (M.valid o hs hv)
+  have hcorrect := M.correct o hs hv ((Memory.spec w).clientRun_canonical s _ hvalid)
+  have hinv := hcorrect.2
+  change Stack.Memory.Inv L ((Memory.spec w).clientState s (Stack.Memory.methods L w C o)) at hinv
+  rw [clientState_width w] at hinv
+  exact ⟨hvalid, hinv⟩
+
+private theorem client_wellFormed {w : ℕ} {α : Type} {s : Memory.State} (hw : Memory.WellFormed w s)
+    (p : Memory.Prog α)
+    (hv : (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s p)) :
+    Memory.WellFormed w ((Memory.spec 0).clientState s p) := by
+  have h := hw.run hv
+  rw [StateTransitionSpec.run_runClient] at h
+  rw [clientState_width w] at h
+  exact h
+
+private theorem transfer_step {L₁ L₂ : Stack.Memory.Layout} {w C n : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hs₁ : Stack.Memory.Inv L₁ s) (hs₂ : Stack.Memory.Inv L₂ s)
+    (hn : s.mem L₂.count.base = n + 1)
+    (hlen : s.mem L₁.count.base + s.mem L₂.count.base ≤ C) :
+    let p := transferBody ((L₁, L₂), true)
+    let s' := (Memory.spec 0).clientState s p
+    transferSafe w ((L₁, L₂), true) s ∧
+      Memory.WellFormed w s' ∧ Stack.Memory.Inv L₁ s' ∧ Stack.Memory.Inv L₂ s' ∧
+      s'.mem L₂.count.base = n ∧ s'.mem L₁.count.base = s.mem L₁.count.base + 1 ∧
+      (Memory.spec 0).clientResult s p = true ∧ memoryCost p s = 6 := by
+  have hne : s.mem L₂.count.base ≠ 0 := by omega
+  let a := (Memory.spec 0).clientState s (Stack.Memory.pop L₂)
+  let v := s.mem (L₂.items.base + (s.mem L₂.count.base - 1))
+  let b := (Memory.spec 0).clientState a (Stack.Memory.push L₁ v)
+  have hpoprun := Stack.Memory.runClient_pop_of_pos (w := 0) L₂ s hne
+  have ha : a = ⟨Function.update s.mem L₂.count.base n, s.frontier⟩ := by
+    change ((Memory.spec 0).runClient s (Stack.Memory.pop L₂)).2.1 = _
+    rw [hpoprun]
+    simp only [hn, Nat.add_sub_cancel]
+  have hanswer : (Memory.spec 0).clientResult s (Stack.Memory.pop L₂) = some v := by
+    change ((Memory.spec 0).runClient s (Stack.Memory.pop L₂)).1 = _
+    rw [hpoprun]
+  have hc : L₁.count.base ≠ L₂.count.base :=
+    ne_of_mem_of_not_mem (L₁.count_mem_footprint h₁.count_length)
+      (Finset.disjoint_right.mp hd (L₂.count_mem_footprint h₂.count_length))
+  have hcountA : a.mem L₁.count.base = s.mem L₁.count.base := by
+    rw [ha]
+    exact Function.update_of_ne hc _ _
+  have hspare : a.mem L₁.count.base < C := by omega
+  obtain ⟨hvp, hInvRearA⟩ := stack_inv_step h₂ hs₂ .pop trivial
+  have hframeA := Stack.Memory.frame h₂ h₁ hd.symm hs₁ .pop trivial
+  rw [clientState_width w] at hframeA
+  have hInvFrontA : Stack.Memory.Inv L₁ a := hframeA.2
+  have hvpush : (Stack.WordRAM.spec w C).valid (Stack.Memory.abs L₁ a) (.push v) := by
+    exact ⟨by simpa only [Stack.Memory.length_abs] using hspare, hw.mem_fits _⟩
+  obtain ⟨hvq, hInvFrontB⟩ := stack_inv_step h₁ hInvFrontA (.push v) hvpush
+  have hframeB := Stack.Memory.frame h₁ h₂ hd hInvRearA (.push v) hvpush
+  rw [clientState_width w] at hframeB
+  have hInvRearB : Stack.Memory.Inv L₂ b := hframeB.2
+  have hrear : b.mem L₂.count.base = n := by
+    have h := congrArg List.length hframeB.1
+    simp only [Stack.Memory.length_abs] at h
+    change b.mem L₂.count.base = a.mem L₂.count.base at h
+    rw [h, ha]
+    exact Function.update_self _ _ _
+  have hfront : b.mem L₁.count.base = s.mem L₁.count.base + 1 := by
+    change ((Memory.spec 0).runClient a (Stack.Memory.push L₁ v)).2.1.mem L₁.count.base = _
+    rw [Stack.Memory.runClient_push]
+    simpa only [Function.update_self] using congrArg (· + 1) hcountA
+  have hwb : Memory.WellFormed w b :=
+    client_wellFormed (client_wellFormed hw _ hvp) _ hvq
+  have h1 : Fits w 1 := hw.frontier_fits.of_le (by
+    have h := hs₂.count_allocated
+    change L₂.count.base + L₂.count.length ≤ s.frontier at h
+    rw [h₂.count_length] at h
+    omega)
+  have hsafe : transferSafe w ((L₁, L₂), true) s := by
+    change L₂.Valid w L₂.items.length ∧ Stack.Memory.Inv L₂ s ∧ _
+    refine ⟨by simpa only [h₂.items_length] using h₂, hs₂, ?_⟩
+    rw [hanswer]
+    exact ⟨by simpa only [h₁.items_length] using h₁, hInvFrontA,
+      by simpa only [h₁.items_length] using hspare, h1⟩
+  have hbodyResult : (Memory.spec 0).clientResult s (transferBody ((L₁, L₂), true)) = true := by
+    change ((Memory.spec 0).runClient s ((Stack.Memory.pop L₂).bind _)).1 = true
+    rw [StateTransitionSpec.runClient_bind]
+    change ((Memory.spec 0).runClient a
+      (match (Memory.spec 0).clientResult s (Stack.Memory.pop L₂) with
+      | none => pure false
+      | some v => (Stack.Memory.push L₁ v).bind (fun _ => pure true))).1 = true
+    rw [hanswer]
+    rfl
+  have hbodyState : (Memory.spec 0).clientState s (transferBody ((L₁, L₂), true)) = b := by
+    change ((Memory.spec 0).runClient s ((Stack.Memory.pop L₂).bind _)).2.1 = b
+    rw [StateTransitionSpec.runClient_bind]
+    change ((Memory.spec 0).runClient a
+      (match (Memory.spec 0).clientResult s (Stack.Memory.pop L₂) with
+      | none => pure false
+      | some v => (Stack.Memory.push L₁ v).bind (fun _ => pure true))).2.1 = b
+    rw [hanswer]
+    rfl
+  have hpopcost : memoryCost (Stack.Memory.pop L₂) s = 3 := by
+    simp [memoryCost, StateTransitionSpec.clientHistory, hpoprun]
+  have hpushcost : memoryCost (Stack.Memory.push L₁ v) a = 3 := by
+    simp [memoryCost, StateTransitionSpec.clientHistory, Stack.Memory.runClient_push]
+  have hcost : memoryCost (transferBody ((L₁, L₂), true)) s = 6 := by
+    change memoryCost ((Stack.Memory.pop L₂).bind _) s = 6
+    rw [memoryCost_bind, hanswer]
+    change memoryCost (Stack.Memory.pop L₂) s +
+      memoryCost ((Stack.Memory.push L₁ v).bind (fun _ => pure true)) a = 6
+    rw [memoryCost_bind, hpopcost, hpushcost]
+    rfl
+  exact ⟨hsafe, hbodyState.symm ▸ hwb, hbodyState.symm ▸ hInvFrontB,
+    hbodyState.symm ▸ hInvRearB, hbodyState.symm ▸ hrear, hbodyState.symm ▸ hfront,
+    hbodyResult, hcost⟩
+
+/-- Disjoint allocated stacks within the combined capacity discharge the native transfer's
+actual intermediate domains. Transferring the rear count performs exactly six memory units per
+item, retains both storage invariants and moves every rear item into the front. -/
+theorem transfer_invariant {L₁ L₂ : Stack.Memory.Layout} {w C n : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hs₁ : Stack.Memory.Inv L₁ s) (hs₂ : Stack.Memory.Inv L₂ s)
+    (hn : s.mem L₂.count.base = n)
+    (hlen : s.mem L₁.count.base + s.mem L₂.count.base ≤ C) :
+    let p := iterate transferBody (L₁, L₂) n true
+    let s' := (Memory.spec 0).clientState s p
+    iterationSafe transferBody transferSafe w (L₁, L₂) n true s ∧
+      Memory.WellFormed w s' ∧ Stack.Memory.Inv L₁ s' ∧ Stack.Memory.Inv L₂ s' ∧
+      s'.mem L₂.count.base = 0 ∧ s'.mem L₁.count.base = s.mem L₁.count.base + n ∧
+      memoryCost p s = 6 * n := by
+  induction n generalizing s with
+  | zero => exact ⟨trivial, hw, hs₁, hs₂, hn, rfl, rfl⟩
+  | succ n ih =>
+    obtain ⟨hsafe, hw₁, hi₁, hi₂, hn₁, hf₁, hresult, hcost₁⟩ :=
+      transfer_step h₁ h₂ hd hw hs₁ hs₂ hn hlen
+    let s₁ := (Memory.spec 0).clientState s (transferBody ((L₁, L₂), true))
+    have hlen₁ : s₁.mem L₁.count.base + s₁.mem L₂.count.base ≤ C := by
+      rw [hn₁, hf₁]
+      omega
+    obtain ⟨hsafe', hw', hi₁', hi₂', hn', hf', hcost'⟩ := ih hw₁ hi₁ hi₂ hn₁ hlen₁
+    have hstate : (Memory.spec 0).clientState s (iterate transferBody (L₁, L₂) (n + 1) true) =
+        (Memory.spec 0).clientState s₁ (iterate transferBody (L₁, L₂) n true) := by
+      change (Memory.spec 0).clientState s ((transferBody ((L₁, L₂), true)).bind
+        (iterate transferBody (L₁, L₂) n)) = _
+      simp only [StateTransitionSpec.clientState, StateTransitionSpec.runClient_bind]
+      change (Memory.spec 0).clientState s₁
+        (iterate transferBody (L₁, L₂) n ((Memory.spec 0).clientResult s
+          (transferBody ((L₁, L₂), true)))) = _
+      rw [hresult]
+    have hfront : ((Memory.spec 0).clientState s₁ (iterate transferBody (L₁, L₂) n true)).mem
+        L₁.count.base = s.mem L₁.count.base + (n + 1) := by
+      rw [hf', hf₁]
+      omega
+    refine ⟨⟨hsafe, ?_⟩, hstate.symm ▸ hw', hstate.symm ▸ hi₁', hstate.symm ▸ hi₂',
+      hstate.symm ▸ hn', hstate.symm ▸ hfront, ?_⟩
+    · simpa only [hresult] using hsafe'
+    · change memoryCost ((transferBody ((L₁, L₂), true)).bind
+        (iterate transferBody (L₁, L₂) n)) s = _
+      rw [memoryCost_bind, hresult, hcost₁, hcost']
+      omega
+
+/-- The existing linked transfer has the same six-units-per-item memory history as the certified
+bounded loop. This statement counts memory units; the next lemma pays the actual local work. -/
+theorem source_transfer_cost {L₁ L₂ : Stack.Memory.Layout} {w C n : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hs₁ : Stack.Memory.Inv L₁ s) (hs₂ : Stack.Memory.Inv L₂ s)
+    (hn : s.mem L₂.count.base = n)
+    (hlen : s.mem L₁.count.base + s.mem L₂.count.base ≤ C) :
+    memoryCost (link (Stack.Memory.pairMethods L₁ L₂ w C) (Queue.transfer n)) s = 6 * n := by
+  obtain ⟨_, _, _, _, _, _, hcost⟩ := transfer_invariant h₁ h₂ hd hw hs₁ hs₂ hn hlen
+  rw [transfer_eq_iterate, memoryCost_bind]
+  change memoryCost (iterate transferBody (L₁, L₂) n true) s + 0 = _
+  exact hcost
+
+/-- The explicit native loop grading is dominated by memory charge only when the fuel is the
+actual rear count and the storage invariants hold. Oversized inactive tails are not free. -/
+theorem source_transfer_work_bound {L₁ L₂ : Stack.Memory.Layout} {w C n : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hs₁ : Stack.Memory.Inv L₁ s) (hs₂ : Stack.Memory.Inv L₂ s)
+    (hn : s.mem L₂.count.base = n)
+    (hlen : s.mem L₁.count.base + s.mem L₂.count.base ≤ C) :
+    40 * n + 1 ≤ 7 * memoryCost
+      (link (Stack.Memory.pairMethods L₁ L₂ w C) (Queue.transfer n)) s + 1 := by
+  rw [source_transfer_cost h₁ h₂ hd hw hs₁ hs₂ hn hlen]
+  omega
+
+/-- A concrete combined-currency envelope for the actual transfer certificate. Its local work
+is the grading supplied by `realizes_source_transfer`, with the same invariant assumptions. -/
+theorem source_transfer_combined_bound {L₁ L₂ : Stack.Memory.Layout} {w C n : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hs₁ : Stack.Memory.Inv L₁ s) (hs₂ : Stack.Memory.Inv L₂ s)
+    (hn : s.mem L₂.count.base = n)
+    (hlen : s.mem L₁.count.base + s.mem L₂.count.base ≤ C) :
+    combinedCost (link (Stack.Memory.pairMethods L₁ L₂ w C) (Queue.transfer n))
+        (fun _ => 40 * n + 1) s ≤
+      8 * memoryCost (link (Stack.Memory.pairMethods L₁ L₂ w C) (Queue.transfer n)) s + 1 := by
+  have h := source_transfer_work_bound h₁ h₂ hd hw hs₁ hs₂ hn hlen
+  simp only [combinedCost]
+  omega
+
+end Cslib.WordRAM.Realization.MemoryQueue
diff --git a/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueDispatch.lean b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueDispatch.lean
new file mode 100644
index 0000000000..ef6bdebd3d
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueDispatch.lean
@@ -0,0 +1,261 @@
+/-
+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.WordRAM.Realization.Client.MemoryQueue
+
+/-!
+# Native dispatch for the memory-oracle queue
+
+The existing enqueue and dequeue methods consume both complete runtime stack layouts. The
+dequeue branch tests a certified zero against the front-pop presence tag, so a payload equal to
+one cannot be mistaken for an empty result. The fallback computes the complete transfer argument
+encoding with certified vector glue before consuming the uniform transfer certificate.
+
+The visible entry domains follow the actual intermediate memory states. Local work includes
+argument staging, result copies, both dispatch alternatives and every bind; memory charges alone
+do not account for this work. No source queue or stack method is changed.
+
+## Main definitions
+
+* `enqueueWords`: both runtime layouts followed by the enqueue payload.
+* `dequeueSafe`, `dequeueWork`: actual-state domain and path-selected local-work ledger.
+
+## Main results
+
+* `realizes_enqueue`, `realizes_dequeue`: the existing complete queue methods have uniform
+  native emitters.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization.MemoryQueueDispatch
+
+open Cslib.DataStructure
+
+private abbrev Layouts := Stack.Memory.Layout × Stack.Memory.Layout
+private abbrev word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+private abbrev unitWords : Unit ↪ (Fin 0 → ℕ) := (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+
+/-- Both complete runtime layouts precede the unshifted payload. -/
+def enqueueWords : ((Stack.Memory.Layout × Stack.Memory.Layout) × ℕ) ↪ (Fin 9 → ℕ) :=
+  (MemoryQueue.layoutWords.prodMap (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans
+    (Fin.appendEquiv 8 1).toEmbedding
+
+/-- The rear-size reply is read at the actual state after the initial front pop. -/
+def dequeueFuel (L : Stack.Memory.Layout × Stack.Memory.Layout) (s : Memory.State) : ℕ :=
+  (Memory.spec 0).clientResult ((Memory.spec 0).clientState s (Stack.Memory.pop L.1))
+    (Stack.Memory.size L.2)
+
+/-- Only the fallback requires the transfer's actual-state domain and the final front-pop
+invariant. The memory-history admissibility premise of `Realizes` remains separate. -/
+def dequeueSafe (w : ℕ) (L : Stack.Memory.Layout × Stack.Memory.Layout)
+    (s : Memory.State) : Prop :=
+  L.1.Valid w L.1.items.length ∧ Stack.Memory.Inv L.1 s ∧
+    match (Memory.spec 0).clientResult s (Stack.Memory.pop L.1) with
+    | some _ => True
+    | none =>
+      let mid := (Memory.spec 0).clientState
+        ((Memory.spec 0).clientState s (Stack.Memory.pop L.1)) (Stack.Memory.size L.2)
+      iterationSafe MemoryQueue.transferBody MemoryQueue.transferSafe w L (dequeueFuel L s)
+        true mid ∧
+      Stack.Memory.Inv L.1 ((Memory.spec 0).clientState mid
+        (link (Stack.Memory.pairMethods L.1 L.2 0 0) (Queue.transfer (dequeueFuel L s))))
+
+/-- The immediate path pays 28 units. The fallback additionally pays forty units per actual
+rear-size reply and a total constant allowance of 69, including transfer argument staging. -/
+def dequeueWork (L : Stack.Memory.Layout × Stack.Memory.Layout) (s : Memory.State) : ℕ :=
+  match (Memory.spec 0).clientResult s (Stack.Memory.pop L.1) with
+  | some _ => 28
+  | none => 40 * dequeueFuel L s + 69
+
+/-- A convenient affine bound retains the actual queried fuel, even on the shorter path. -/
+theorem dequeueWork_le (L : Stack.Memory.Layout × Stack.Memory.Layout) (s : Memory.State) :
+    dequeueWork L s ≤ 40 * dequeueFuel L s + 69 := by
+  unfold dequeueWork
+  split <;> omega
+
+/-- Enqueue consumes the rear stack's certified push, with all runtime words retained. -/
+theorem realizes_enqueue (w C : ℕ) :
+    Realizes .exact
+      (fun d : (Stack.Memory.Layout × Stack.Memory.Layout) × ℕ =>
+        Queue.Memory.memMethods d.1.1 d.1.2 w C (.enqueue d.2))
+      enqueueWords (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+      (fun w d s => d.1.2.Valid w d.1.2.items.length ∧ Stack.Memory.Inv d.1.2 s ∧
+        s.mem d.1.2.count.base < d.1.2.items.length) (fun _ _ => 10) := by
+  have h := MemoryStack.realizes_push.reindex
+    (fun d : Layouts × ℕ => (d.1.2, d.2)) enqueueWords ![4, 5, 6, 7, 8]
+    (by intro d i; fin_cases i <;> rfl)
+  simpa only [MemoryQueue.memMethods_enqueue] using h
+
+private def replyInput := appendWords MemoryQueue.layoutWords optionWords
+private def zeroInput := appendWords replyInput word
+private def fuelInput := appendWords zeroInput word
+private def stagedInput := appendWords fuelInput (MemoryQueue.transferWords MemoryQueue.layoutWords)
+private def lastInput := appendWords stagedInput unitWords
+
+private theorem returnZero {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ)) :
+    Realizes .exact (fun _ => pure 0) input word
+      (fun _ _ _ => True) (fun _ _ => 1) := by
+  have h := Realizes.glue input
+    (GlueComputes.const (B := .exact) (P := fun _ => True) (bound := fun _ => 0)
+      0 (fun _ _ => le_rfl))
+  exact h.consequence (fun w _ _ _ _ _ => ⟨trivial, fits_zero w⟩) (fun _ _ => le_rfl)
+
+private theorem returnOption {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ))
+    (f : δ → Option ℕ) (ix : Fin 2 → Fin k)
+    (hf : ∀ d i, optionWords (f d) i = input d (ix i)) :
+    Realizes .exact (fun d => pure (f d)) input optionWords
+      (fun _ _ _ => True) (fun _ _ => 4) := by
+  have h := Realizes.glueVector (B := .exact) input optionWords f
+    (fun i v => v (ix i)) (fun i v => v (ix i)) (fun _ => 1) hf
+    (P := fun _ => True) (fun i => GlueComputes.proj (ix i) (fun _ _ => le_rfl))
+  exact h.consequence (fun _ _ _ hwords _ _ => ⟨trivial, fun i => hwords (ix i)⟩)
+    (fun _ _ => by simp)
+
+private def stageCoordinates (i : Fin 11) (v : Fin 12 → ℕ) : ℕ :=
+  Fin.append (Fin.append (fun j : Fin 8 => v (Fin.castLE (by omega) j))
+    (boolWords true)) (fun _ : Fin 1 => v 11) i
+
+private theorem stageTransfer :
+    Realizes .exact (fun d : ((Layouts × Option ℕ) × ℕ) × ℕ => pure (d.1.1.1, d.2))
+      fuelInput (MemoryQueue.transferWords MemoryQueue.layoutWords)
+      (fun w _ _ => Fits w 1) (fun _ _ => 22) := by
+  have hc (i : Fin 11) : GlueComputes .exact (fun _ : Fin 12 → ℕ => True)
+      (stageCoordinates i) (stageCoordinates i) 1 := by
+    fin_cases i
+    · exact GlueComputes.proj 0 (fun _ _ => le_rfl)
+    · exact GlueComputes.proj 1 (fun _ _ => le_rfl)
+    · exact GlueComputes.proj 2 (fun _ _ => le_rfl)
+    · exact GlueComputes.proj 3 (fun _ _ => le_rfl)
+    · exact GlueComputes.proj 4 (fun _ _ => le_rfl)
+    · exact GlueComputes.proj 5 (fun _ _ => le_rfl)
+    · exact GlueComputes.proj 6 (fun _ _ => le_rfl)
+    · exact GlueComputes.proj 7 (fun _ _ => le_rfl)
+    · exact GlueComputes.const 1 (fun _ _ => le_rfl)
+    · exact GlueComputes.const 0 (fun _ _ => le_rfl)
+    · exact GlueComputes.proj 11 (fun _ _ => le_rfl)
+  have h := Realizes.glueVector fuelInput (MemoryQueue.transferWords MemoryQueue.layoutWords)
+    (fun d => (d.1.1.1, d.2)) stageCoordinates stageCoordinates (fun _ => 1)
+    (fun _ i => by fin_cases i <;> rfl) hc
+  apply h.consequence (hwork := fun _ _ => by simp)
+  intro w d s hwords _ h1
+  refine ⟨trivial, fun i => ?_⟩
+  fin_cases i
+  · exact hwords 0
+  · exact hwords 1
+  · exact hwords 2
+  · exact hwords 3
+  · exact hwords 4
+  · exact hwords 5
+  · exact hwords 6
+  · exact hwords 7
+  · exact h1
+  · exact fits_zero w
+  · exact hwords 11
+
+private def afterSizeSafe (w : ℕ) (L : Layouts) (n : ℕ) (s : Memory.State) : Prop :=
+  Fits w 1 ∧ iterationSafe MemoryQueue.transferBody MemoryQueue.transferSafe w L n true s ∧
+    L.1.Valid w L.1.items.length ∧ Stack.Memory.Inv L.1 ((Memory.spec 0).clientState s
+      (link (Stack.Memory.pairMethods L.1 L.2 0 0) (Queue.transfer n)))
+
+/-- The complete existing dequeue has one emitter before either layout, any payload, the queried
+rear count and every intermediate state. Its local-work ledger includes the pure staging paths. -/
+theorem realizes_dequeue (w C : ℕ) :
+    Realizes .exact (fun L : Stack.Memory.Layout × Stack.Memory.Layout =>
+      Queue.Memory.memMethods L.1 L.2 w C .dequeue)
+      MemoryQueue.layoutWords optionWords dequeueSafe dequeueWork := by
+  have hfirst := MemoryStack.realizes_pop.reindex (fun L : Layouts => L.1)
+    MemoryQueue.layoutWords ![0, 1, 2, 3] (by intro d i; fin_cases i <;> rfl)
+  have hsize := MemoryStack.realizes_size.reindex
+    (fun d : (Layouts × Option ℕ) × ℕ => d.1.1.2) zeroInput ![4, 5, 6, 7]
+    (by intro d i; fin_cases i <;> rfl)
+  have htransfer := (MemoryQueue.realizes_source_transfer w C).reindex
+    (fun d : (((Layouts × Option ℕ) × ℕ) × ℕ) × (Layouts × ℕ) => d.2)
+    stagedInput (Fin.natAdd 12) (by
+      intro d i
+      change MemoryQueue.transferWords MemoryQueue.layoutWords d.2 i =
+        Fin.append (fuelInput d.1) (MemoryQueue.transferWords MemoryQueue.layoutWords d.2)
+          (Fin.natAdd 12 i)
+      rw [Fin.append_right])
+  have hlast := MemoryStack.realizes_pop.reindex
+    (fun d : ((((Layouts × Option ℕ) × ℕ) × ℕ) × (Layouts × ℕ)) × Unit => d.1.2.1.1)
+    lastInput ![12, 13, 14, 15] (by intro d i; fin_cases i <;> rfl)
+  have hstage := (stageTransfer.bind (htransfer.bind hlast)).consequence
+    (safe' := fun w d s => afterSizeSafe w d.1.1.1 d.2 s)
+    (work' := fun d _ => 40 * d.2 + 44)
+    (by
+      intro ww d s _ _ hh
+      simpa only [afterSizeSafe, StateTransitionSpec.clientResult, StateTransitionSpec.clientState,
+        StateTransitionSpec.runClient_pure, StateTransitionSpec.runClient_pure',
+        MemoryQueue.transfer_eq_iterate] using hh)
+    (by intro d s; change 22 + (40 * d.2 + 1 + 19 + 1) + 1 ≤ _; omega)
+  have hnone := (hsize.bind hstage).consequence
+    (safe' := fun w d s => afterSizeSafe w d.1.1
+      ((Memory.spec 0).clientResult s (Stack.Memory.size d.1.1.2))
+      ((Memory.spec 0).clientState s (Stack.Memory.size d.1.1.2)))
+    (work' := fun d s => 40 * (Memory.spec 0).clientResult s (Stack.Memory.size d.1.1.2) + 45)
+    (fun _ _ _ _ _ h => ⟨trivial, h⟩) (by
+      intro d s
+      change 0 + (40 * (Memory.spec 0).clientResult s (Stack.Memory.size d.1.1.2) + 44) + 1 ≤ _
+      omega)
+  have hsome := returnOption zeroInput (fun d => d.1.2) ![8, 9]
+    (by intro d i; fin_cases i <;> rfl)
+  have hbranch := Realizes.branch (.eq 8 10) hnone hsome
+  have h := hfirst.bind ((returnZero replyInput).bind hbranch)
+  have hprogram :
+      (fun L : Layouts => (Stack.Memory.pop L.1).bind (fun a =>
+        (pure 0 : Memory.Prog ℕ).bind (fun z =>
+          if test (.eq 8 10) (zeroInput ((L, a), z)) then
+            (Stack.Memory.size L.2).bind (fun n =>
+              (link (Stack.Memory.pairMethods L.1 L.2 w C) (Queue.transfer n)).bind
+                (fun _ => Stack.Memory.pop L.1))
+          else pure a))) =
+      (fun L : Layouts => Queue.Memory.memMethods L.1 L.2 w C .dequeue) := by
+    funext L
+    rw [MemoryQueue.memMethods_dequeue]
+    congr 1
+    funext a
+    cases a with
+    | some v => rfl
+    | none =>
+      change (Stack.Memory.size L.2).bind (fun n =>
+        (link (Stack.Memory.pairMethods L.1 L.2 w C) (Queue.transfer n)).bind
+          (fun _ => Stack.Memory.pop L.1)) = _
+      congr 1
+      funext n
+      rw [MemoryQueue.transfer_eq_iterate]
+      simp only [PFunctor.FreeM.bind_eq_bind, bind_assoc, pure_bind]
+  simp only [PFunctor.FreeM.bind_eq_bind, pure_bind] at h hprogram
+  rw [hprogram] at h
+  apply h.consequence
+  · intro w L s hwords _ ⟨hL, hInv, hnext⟩
+    have h1 : Fits w 1 := hL.count_length ▸ hwords 1
+    refine ⟨⟨hL, hInv⟩, trivial, ?_⟩
+    cases ha : (Memory.spec 0).clientResult s (Stack.Memory.pop L.1) with
+    | some v =>
+      change (if 1 = 0 then _ else True)
+      trivial
+    | none =>
+      simp only [ha] at hnext
+      change afterSizeSafe w L (dequeueFuel L s)
+        ((Memory.spec 0).clientState ((Memory.spec 0).clientState s (Stack.Memory.pop L.1))
+          (Stack.Memory.size L.2))
+      exact ⟨h1, hnext.1, hL, hnext.2⟩
+  · intro L s
+    unfold dequeueWork
+    cases ha : (Memory.spec 0).clientResult s (Stack.Memory.pop L.1) with
+    | some v =>
+      change 19 + (1 + (4 + 2) + 1) + 1 ≤ 28
+      omega
+    | none =>
+      change 19 + (1 + (40 * dequeueFuel L s + 45 + 2) + 1) + 1 ≤
+        40 * dequeueFuel L s + 69
+      omega
+
+end Cslib.WordRAM.Realization.MemoryQueueDispatch
diff --git a/ComplexityTests/WordRAMMemoryQueueDispatch.lean b/ComplexityTests/WordRAMMemoryQueueDispatch.lean
new file mode 100644
index 0000000000..0a73ee3d3b
--- /dev/null
+++ b/ComplexityTests/WordRAMMemoryQueueDispatch.lean
@@ -0,0 +1,186 @@
+/-
+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.WordRAM.Realization.Client.MemoryQueueDispatch
+import Complexity.Computability.WordRAM.Realization.Witness
+
+/-! One fixed native dequeue body handles an immediate payload equal to one, a runtime-sized
+transfer returning the maximum word, and an empty queue. The first case distinguishes the
+presence tag from a coincidentally equal payload. All cases retain inaccessible memory. -/
+
+namespace ComplexityTests.WordRAMMemoryQueueDispatch
+
+open Cslib Cslib.DataStructure Cslib.WordRAM Cslib.WordRAM.Realization
+open MemoryQueueDispatch
+
+private def front : Stack.Memory.Layout := ⟨⟨0, 1⟩, ⟨1, 2⟩⟩
+private def rear : Stack.Memory.Layout := ⟨⟨3, 1⟩, ⟨4, 2⟩⟩
+private def state (nf nr v : ℕ) : Memory.State :=
+  ⟨fun a => if a = 0 then nf else if a = 1 then v else if a = 3 then nr else
+    if a = 4 then 15 else if a = 5 then 7 else 9, 6⟩
+private def immediate := state 1 1 1
+private def fallback := state 0 2 9
+private def empty := state 0 0 9
+
+private theorem front_valid : front.Valid 4 2 := by
+  refine ⟨rfl, ?_, rfl, ?_⟩ <;> norm_num [front, Block.Owns, Fits]
+
+private theorem rear_valid : rear.Valid 4 2 := by
+  refine ⟨rfl, ?_, rfl, ?_⟩ <;> norm_num [rear, Block.Owns, Fits]
+
+private theorem state_wf {nf nr v : ℕ} (hf : Fits 4 nf) (hr : Fits 4 nr) (hv : Fits 4 v) :
+    Memory.WellFormed 4 (state nf nr v) := by
+  refine ⟨by change Fits 4 6; decide, fun a => ?_⟩
+  change Fits 4 (if a = 0 then nf else if a = 1 then v else if a = 3 then nr else
+    if a = 4 then 15 else if a = 5 then 7 else 9)
+  split_ifs <;> first | assumption | decide
+
+private theorem inv_front {nf nr v : ℕ} (h : nf ≤ 2) :
+    Stack.Memory.Inv front (state nf nr v) := by
+  refine ⟨?_, ?_, ?_⟩
+  · change 0 + 1 ≤ 6; omega
+  · change 1 + 2 ≤ 6; omega
+  · exact h
+
+private theorem inv_rear {nf nr v : ℕ} (h : nr ≤ 2) :
+    Stack.Memory.Inv rear (state nf nr v) := by
+  refine ⟨?_, ?_, ?_⟩
+  · change 3 + 1 ≤ 6; omega
+  · change 4 + 2 ≤ 6; omega
+  · exact h
+
+private theorem safe_immediate : dequeueSafe 4 (front, rear) immediate := by
+  change front.Valid 4 2 ∧ Stack.Memory.Inv front immediate ∧ True
+  exact ⟨front_valid, inv_front (by decide), trivial⟩
+
+private theorem safe_fallback : dequeueSafe 4 (front, rear) fallback := by
+  have hw : Memory.WellFormed 4 fallback := state_wf (by decide) (by decide) (by decide)
+  have hF : Stack.Memory.Inv front fallback := inv_front (by decide)
+  have hR : Stack.Memory.Inv rear fallback := inv_rear (by decide)
+  have hd : Disjoint front.footprint rear.footprint := by decide
+  have ht := MemoryQueue.transfer_invariant (n := 2) front_valid rear_valid hd hw hF hR
+    rfl (by decide)
+  change front.Valid 4 2 ∧ Stack.Memory.Inv front fallback ∧
+    iterationSafe MemoryQueue.transferBody MemoryQueue.transferSafe 4 (front, rear) 2 true
+      fallback ∧ Stack.Memory.Inv front ((Memory.spec 0).clientState fallback
+        (link (Stack.Memory.pairMethods front rear 0 0) (Queue.transfer 2)))
+  refine ⟨front_valid, hF, ht.1, ?_⟩
+  rw [MemoryQueue.transfer_eq_iterate]
+  simpa only [StateTransitionSpec.clientState, StateTransitionSpec.runClient_bind,
+    StateTransitionSpec.runClient_pure, StateTransitionSpec.runClient_pure'] using ht.2.2.1
+
+private theorem safe_empty : dequeueSafe 4 (front, rear) empty := by
+  change front.Valid 4 2 ∧ Stack.Memory.Inv front empty ∧ True ∧ Stack.Memory.Inv front empty
+  exact ⟨front_valid, inv_front (by decide), trivial, inv_front (by decide)⟩
+
+private theorem realization :
+    Realizes .exact (fun L : Stack.Memory.Layout × Stack.Memory.Layout =>
+      Queue.Memory.memMethods L.1 L.2 4 2 .dequeue)
+      MemoryQueue.layoutWords optionWords dequeueSafe dequeueWork := realizes_dequeue 4 2
+
+private noncomputable def registers : ℕ := realization.scratchSize + 12
+private noncomputable def src (i : Fin 8) : Fin registers :=
+  ⟨i.val, by have := i.isLt; unfold registers; omega⟩
+private noncomputable def frontier : Fin registers := ⟨8, by unfold registers; omega⟩
+private noncomputable def scratch (i : Fin (2 + realization.scratchSize + 1)) : Fin registers :=
+  ⟨9 + i.val, by have := i.isLt; unfold registers; omega⟩
+private noncomputable def code := realization.code frontier src scratch
+
+private noncomputable def data (s : Memory.State) : Data registers where
+  regs i := if h : i.val < 8 then MemoryQueue.layoutWords (front, rear) ⟨i.val, h⟩
+    else if i.val = 8 then 6 else 0
+  mem := s.mem
+
+private theorem encoded_fits (i : Fin 8) : Fits 4 (MemoryQueue.layoutWords (front, rear) i) := by
+  fin_cases i <;> decide
+
+private theorem execution (s : Memory.State) (hw : Memory.WellFormed 4 s) (hf : s.frontier = 6)
+    (hsafe : dequeueSafe 4 (front, rear) s)
+    (hvalid : (Memory.spec 4).ValidHistory s ((Memory.spec 4).clientHistory s
+      (Queue.Memory.memMethods front rear 4 2 .dequeue))) :
+    ∃ y, ExecWithin 4 code (data s) y
+        (realization.factor * (memoryCost (Queue.Memory.memMethods front rear 4 2 .dequeue) s +
+          dequeueWork (front, rear) s + 1)) ∧
+      memoryState frontier y = (Memory.spec 4).clientState s
+        (Queue.Memory.memMethods front rear 4 2 .dequeue) ∧
+      ∀ i : Fin 2, y.regs (scratch (Fin.castAdd (realization.scratchSize + 1) i)) =
+        optionWords ((Memory.spec 4).clientResult s
+          (Queue.Memory.memMethods front rear 4 2 .dequeue)) i := by
+  have hi : Function.Injective scratch := by
+    intro i j h
+    apply Fin.ext
+    have := congrArg Fin.val h
+    change 9 + i.val = 9 + j.val at this
+    omega
+  have hd (i : Fin 8) (j) : src i ≠ scratch j := by
+    intro h
+    have := congrArg Fin.val h
+    change i.val = 9 + j.val at this
+    have := i.isLt
+    omega
+  have hfr (j) : scratch j ≠ frontier := by
+    intro h
+    have := congrArg Fin.val h
+    change 9 + j.val = 8 at this
+    omega
+  have hsrc (i : Fin 8) : src i ≠ frontier := by
+    intro h
+    have := congrArg Fin.val h
+    change i.val = 8 at this
+    have := i.isLt
+    omega
+  have hb : (data s).Bounded 4 := by
+    refine ⟨fun i => ?_, hw.mem_fits⟩
+    change Fits 4 (if h : i.val < 8 then MemoryQueue.layoutWords (front, rear) ⟨i.val, h⟩
+      else if i.val = 8 then 6 else 0)
+    split
+    · exact encoded_fits _
+    · split <;> norm_num [Fits]
+  have hin : (data s).regs ∘ src = MemoryQueue.layoutWords (front, rear) := by
+    funext i
+    simp [data, src]
+  have hm : memoryState frontier (data s) = s := by
+    apply Memory.State.ext
+    · rfl
+    · simp [memoryState, data, frontier, hf]
+  obtain ⟨y, he, hmem, hout, _⟩ := (realization.code_spec frontier src scratch hi hd hfr hsrc).2
+    4 (front, rear) (data s) hb hin (hm ▸ hsafe) (hm ▸ hvalid)
+  rw [hm] at he hmem hout
+  exact ⟨y, he, hmem, hout⟩
+
+-- Payload one must take the immediate path, although its tag and payload are both one.
+example : ∃ y, ExecWithin 4 code (data immediate) y (realization.factor * 32) ∧
+    y.regs (scratch (Fin.castAdd (realization.scratchSize + 1) 0)) = 1 ∧
+    y.regs (scratch (Fin.castAdd (realization.scratchSize + 1) 1)) = 1 ∧
+    y.mem 0 = 0 ∧ y.mem 3 = 1 ∧ y.mem 100 = 9 := by
+  obtain ⟨y, he, hm, hout⟩ := execution immediate
+    (state_wf (by decide) (by decide) (by decide)) rfl safe_immediate (by decide)
+  refine ⟨y, he, hout 0, hout 1, ?_, ?_, ?_⟩
+  · exact congrArg (fun s : Memory.State => s.mem 0) hm
+  · exact congrArg (fun s : Memory.State => s.mem 3) hm
+  · exact congrArg (fun s : Memory.State => s.mem 100) hm
+
+-- The same code reads rear fuel two, executes the certified transfer, and returns word fifteen.
+example : ∃ y, ExecWithin 4 code (data fallback) y (realization.factor * 167) ∧
+    y.regs (scratch (Fin.castAdd (realization.scratchSize + 1) 0)) = 1 ∧
+    y.regs (scratch (Fin.castAdd (realization.scratchSize + 1) 1)) = 15 ∧
+    y.mem 0 = 1 ∧ y.mem 3 = 0 ∧ y.mem 100 = 9 := by
+  obtain ⟨y, he, hm, hout⟩ := execution fallback
+    (state_wf (by decide) (by decide) (by decide)) rfl safe_fallback (by decide)
+  refine ⟨y, he, hout 0, hout 1, ?_, ?_, ?_⟩
+  · exact congrArg (fun s : Memory.State => s.mem 0) hm
+  · exact congrArg (fun s : Memory.State => s.mem 3) hm
+  · exact congrArg (fun s : Memory.State => s.mem 100) hm
+
+-- Zero runtime fuel and the empty final pop return none with the same selected emitter.
+example : ∃ y, ExecWithin 4 code (data empty) y (realization.factor * 73) ∧
+    y.regs (scratch (Fin.castAdd (realization.scratchSize + 1) 0)) = 0 ∧
+    y.regs (scratch (Fin.castAdd (realization.scratchSize + 1) 1)) = 0 ∧ y.mem 100 = 9 := by
+  obtain ⟨y, he, hm, hout⟩ := execution empty
+    (state_wf (by decide) (by decide) (by decide)) rfl safe_empty (by decide)
+  exact ⟨y, he, hout 0, hout 1, congrArg (fun s : Memory.State => s.mem 100) hm⟩
+
+end ComplexityTests.WordRAMMemoryQueueDispatch
diff --git a/ComplexityTests/WordRAMRealizationQueue.lean b/ComplexityTests/WordRAMRealizationQueue.lean
new file mode 100644
index 0000000000..ed4807779f
--- /dev/null
+++ b/ComplexityTests/WordRAMRealizationQueue.lean
@@ -0,0 +1,185 @@
+/-
+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.WordRAM.Realization.Client.MemoryQueue
+import Complexity.Computability.WordRAM.Realization.Witness
+
+/-!
+A native transfer consumes the actual two-stack queue's linked memory program. The rear holds
+15 and 7 at word width four, including the maximum fitting payload. The selected code, register
+bank and exchange constant precede all runtime words; the memory proof is the generic kernel's.
+-/
+
+namespace ComplexityTests.WordRAMRealizationQueue
+
+open Cslib Cslib.DataStructure Cslib.WordRAM Cslib.WordRAM.Realization
+open Cslib.WordRAM.Realization.MemoryQueue
+
+private def front : Stack.Memory.Layout := ⟨⟨0, 1⟩, ⟨1, 2⟩⟩
+private def rear : Stack.Memory.Layout := ⟨⟨3, 1⟩, ⟨4, 2⟩⟩
+private def initial : Memory.State :=
+  ⟨fun a => if a = 0 then 0 else if a = 3 then 2 else if a = 4 then 7 else
+    if a = 5 then 15 else 9, 6⟩
+
+private def afterOne : Memory.State :=
+  ⟨Function.update (Function.update (Function.update initial.mem 3 1) 1 15) 0 1, 6⟩
+
+private theorem safe : iterationSafe transferBody transferSafe 4 (front, rear) 2 true initial := by
+  change transferSafe 4 ((front, rear), true) initial ∧
+    transferSafe 4 ((front, rear), true) afterOne ∧ True
+  refine ⟨?_, ?_, trivial⟩
+  all_goals
+    change rear.Valid 4 2 ∧ Stack.Memory.Inv rear _ ∧ front.Valid 4 2 ∧
+      Stack.Memory.Inv front _ ∧ _ < 2 ∧ Fits 4 1
+    refine ⟨⟨rfl, ?_, rfl, ?_⟩, ⟨?_, ?_, ?_⟩,
+      ⟨rfl, ?_, rfl, ?_⟩, ⟨?_, ?_, ?_⟩, ?_, ?_⟩ <;>
+      norm_num [front, rear, initial, afterOne, Block.Allocated, Block.Owns, Fits] <;> decide
+
+private theorem valid : (Memory.spec 4).ValidHistory initial
+    ((Memory.spec 4).clientHistory initial
+      (link (Stack.Memory.pairMethods front rear 4 2) (Queue.transfer 2))) := by decide
+
+private theorem encoded_fits : ∀ i,
+    Fits 4 (transferWords layoutWords ((front, rear), 2) i) := by
+  intro i
+  fin_cases i <;> decide
+
+private theorem mem_fits (a : ℕ) : Fits 4 (initial.mem a) := by
+  simp only [initial]
+  split_ifs <;> norm_num [Fits]
+
+private theorem realization :
+    Realizes .exact
+      (fun d => link (Stack.Memory.pairMethods d.1.1 d.1.2 4 2) (Queue.transfer d.2))
+      (transferWords layoutWords) (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+      (fun w d s => iterationSafe transferBody transferSafe w d.1 d.2 true s)
+      (fun d _ => 40 * d.2 + 1) := realizes_source_transfer 4 2
+private noncomputable def registers : ℕ := realization.scratchSize + 13
+private noncomputable def src (i : Fin 11) : Fin registers :=
+  ⟨i.val, by have := i.isLt; unfold registers; omega⟩
+private noncomputable def frontier : Fin registers := ⟨11, by unfold registers; omega⟩
+private noncomputable def scratch (i : Fin (0 + realization.scratchSize + 1)) : Fin registers :=
+  ⟨12 + i.val, by have := i.isLt; unfold registers; omega⟩
+
+private noncomputable def data : Data registers where
+  regs i := if h : i.val < 11 then transferWords layoutWords ((front, rear), 2) ⟨i.val, h⟩
+    else if i.val = 11 then 6 else 0
+  mem := initial.mem
+
+private theorem execution (x : Data registers) (hb : x.Bounded 4)
+    (hin : x.regs ∘ src = transferWords layoutWords ((front, rear), 2))
+    (hsafe : iterationSafe transferBody transferSafe 4 (front, rear) 2 true
+      (memoryState frontier x))
+    (hvalid : (Memory.spec 4).ValidHistory (memoryState frontier x)
+      ((Memory.spec 4).clientHistory (memoryState frontier x)
+        (link (Stack.Memory.pairMethods front rear 4 2) (Queue.transfer 2)))) :
+    ∃ y, ExecWithin 4 (realization.code frontier src scratch) x y
+        (realization.factor * (memoryCost
+          (link (Stack.Memory.pairMethods front rear 4 2) (Queue.transfer 2))
+            (memoryState frontier x) + 82)) ∧
+      memoryState frontier y = (Memory.spec 4).clientState (memoryState frontier x)
+        (link (Stack.Memory.pairMethods front rear 4 2) (Queue.transfer 2)) := by
+  have hi : Function.Injective scratch := by
+    intro i j h
+    apply Fin.ext
+    have := congrArg Fin.val h
+    change 12 + i.val = 12 + j.val at this
+    omega
+  have hd (i : Fin 11) (j) : src i ≠ scratch j := by
+    intro h
+    have := congrArg Fin.val h
+    change i.val = 12 + j.val at this
+    have := i.isLt
+    omega
+  have hf (j) : scratch j ≠ frontier := by
+    intro h
+    have := congrArg Fin.val h
+    change 12 + j.val = 11 at this
+    omega
+  have hs (i : Fin 11) : src i ≠ frontier := by
+    intro h
+    have := congrArg Fin.val h
+    change i.val = 11 at this
+    have := i.isLt
+    omega
+  obtain ⟨y, he, hm, _, _⟩ := (realization.code_spec frontier src scratch hi hd hf hs).2
+    4 ((front, rear), 2) x hb hin hsafe hvalid
+  exact ⟨y, he, hm⟩
+
+-- A genuine compiled transfer reverses the rear into the front, with all memory framed globally.
+example : ∃ y, ExecWithin 4 (realization.code frontier src scratch) data y
+    (94 * realization.factor) ∧ y.mem 0 = 2 ∧ y.mem 1 = 15 ∧ y.mem 2 = 7 ∧
+      y.mem 3 = 0 ∧ y.mem 100 = 9 ∧ y.regs frontier = 6 := by
+  have hb : data.Bounded 4 := by
+    refine ⟨fun i => ?_, mem_fits⟩
+    change Fits 4 (if h : i.val < 11 then
+      transferWords layoutWords ((front, rear), 2) ⟨i.val, h⟩ else
+      if i.val = 11 then 6 else 0)
+    split
+    · exact encoded_fits _
+    · split <;> norm_num [Fits]
+  have hin : data.regs ∘ src = transferWords layoutWords ((front, rear), 2) := by
+    funext i
+    simp [data, src]
+  have hm : memoryState frontier data = initial := by
+    apply Memory.State.ext
+    · rfl
+    · simp [memoryState, data, frontier, initial]
+  obtain ⟨y, he, hmem⟩ := execution data hb hin (hm ▸ safe) (hm ▸ valid)
+  rw [hm] at he hmem
+  change ExecWithin 4 (realization.code frontier src scratch) data y
+    (realization.factor * (12 + (40 * 2 + 1) + 1)) at he
+  refine ⟨y, he.mono (by omega), ?_, ?_, ?_, ?_, ?_, ?_⟩
+  all_goals
+    first
+    | exact congrArg (fun s : Memory.State => s.mem 0) hmem
+    | exact congrArg (fun s : Memory.State => s.mem 1) hmem
+    | exact congrArg (fun s : Memory.State => s.mem 2) hmem
+    | exact congrArg (fun s : Memory.State => s.mem 3) hmem
+    | exact congrArg (fun s : Memory.State => s.mem 100) hmem
+    | exact congrArg Memory.State.frontier hmem
+
+private def empty : Memory.State := ⟨fun a => if a = 0 ∨ a = 3 then 0 else 9, 6⟩
+private noncomputable def emptyData : Data registers := ⟨data.regs, empty.mem⟩
+
+-- The SAME fixed emitter pays its inactive tail: the source stops after one empty rear pop,
+-- while the runtime fuel is two. No further memory query is introduced by the inactive loop.
+example : ∃ y, ExecWithin 4 (realization.code frontier src scratch) emptyData y
+    (83 * realization.factor) ∧ y.mem = empty.mem ∧ y.regs frontier = 6 := by
+  have hb : emptyData.Bounded 4 := by
+    constructor
+    · intro i
+      change Fits 4 (if h : i.val < 11 then
+        transferWords layoutWords ((front, rear), 2) ⟨i.val, h⟩ else
+        if i.val = 11 then 6 else 0)
+      split
+      · exact encoded_fits _
+      · split <;> norm_num [Fits]
+    · intro a
+      change Fits 4 (if a = 0 ∨ a = 3 then 0 else 9)
+      split <;> norm_num [Fits]
+  have hin : emptyData.regs ∘ src = transferWords layoutWords ((front, rear), 2) := by
+    funext i
+    simp [emptyData, data, src]
+  have hm : memoryState frontier emptyData = empty := by
+    apply Memory.State.ext
+    · rfl
+    · simp [memoryState, emptyData, data, frontier, empty]
+  have hsafe : iterationSafe transferBody transferSafe 4 (front, rear) 2 true empty := by
+    change (rear.Valid 4 2 ∧ Stack.Memory.Inv rear empty ∧ True) ∧ True ∧ True
+    refine ⟨⟨⟨rfl, ?_, rfl, ?_⟩, ⟨?_, ?_, ?_⟩, trivial⟩, trivial, trivial⟩ <;>
+      norm_num [rear, empty, Block.Allocated, Block.Owns, Fits]
+  have hvalid : (Memory.spec 4).ValidHistory empty ((Memory.spec 4).clientHistory empty
+      (link (Stack.Memory.pairMethods front rear 4 2) (Queue.transfer 2))) := by decide
+  obtain ⟨y, he, hmem⟩ := execution emptyData hb hin (hm ▸ hsafe) (hm ▸ hvalid)
+  rw [hm] at he hmem
+  change ExecWithin 4 (realization.code frontier src scratch) emptyData y
+    (realization.factor * (1 + 82)) at he
+  refine ⟨y, he.mono (by omega), ?_, ?_⟩
+  · exact congrArg Memory.State.mem hmem
+  · exact congrArg Memory.State.frontier hmem
+
+end ComplexityTests.WordRAMRealizationQueue
diff --git a/ROADMAP.md b/ROADMAP.md
index 0db31f5c09..c8a085d8a0 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -642,8 +642,10 @@ reusing graph and matroid foundations and the shared data-structure interfaces.
   Word-RAM certificates can be derived from semantic modules after discharging their local
   initialization, footprint and ABI conditions; a one-cell ADT checks that boundary. Multiword
   glue preserves full-word Option payloads, and the actual memory-stack size/push/pop methods
-  have uniform native certificates over runtime layouts, with local work 0/10/19. Remaining:
-  the representative framed queue and its faithful whole-memory allocation/native-client path.
+  have uniform native certificates over runtime layouts, with local work 0/10/19. The exact
+  queue transfer and dequeue dispatch also have native certificates; bounded transfer charges
+  inactive iterations after early stop, and valid transfer fuel has memory cost 6*n and local
+  work 40*n+1. Remaining: the complete framed queue and faithful allocation/native-client path.
   The full C2/M1b objective remains open; arbitrary host continuations do not acquire runtime bounds.
 - **Stateful algorithms and data structures:** Word-RAM controllers for larger adaptive and
   iterative clients, including the two-stack queue and timeline-editing controllers; reusable
diff --git a/UPSTREAM.md b/UPSTREAM.md
index c7761ca654..c28385753e 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -527,6 +527,10 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   values use a tag and unshifted payload, including maximal fitting words. The actual
   `Stack.Memory` size/push/pop clients reuse those rules over faithfully encoded runtime layouts,
   with visible layout/representation/spare-capacity conditions and local work 0/10/19.
+  The exact source queue transfer is realized by an active-flag bounded loop, with inactive
+  tails still charged. Dequeue stages its test zero and full runtime transfer arguments; its
+  local work is 28 on the direct path or 40*rearCount+69 on fallback. Static reindexing rewires
+  existing input words without free computation or new continuation assertions.
   The full framed queue/faithful allocation client remains separate. No abstract headline is added.
   `DataStructure/OrderedSet` and `DataStructure/OrderedSet/*` provide neutral
   optional-minimum contracts, a typed finite-set interface including deletion, and adaptive