From 66650221c9a2d10c7891c3df3e6aead2d323cc1f Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sun, 1 Nov 2026 20:15:42 -0500
Subject: [PATCH 1/2] feat(WordRAM): realize source queue transfer and dispatch

Reuse the unchanged two-stack queue memory programs. A bounded active-flag
loop matches transfer's early stop exactly and charges inactive query-free
iterations. Static reindexing supplies runtime layouts and replies without
new intermediate assertions or hidden computation.

Dequeue stages its zero and complete transfer inputs. Its local work is28 on
the direct path or40*rearCount+69 on fallback; valid exact transfer has memory
cost6*n and local work40*n+1. Same fixed code is checked on maximum payloads,
immediate/fallback/empty paths and whole-memory frames.

This #2213/#2205 milestone leaves the final framed wrapper and faithful
allocated whole-client acceptance open. No abstract headline changes.

AI-assisted authoring: transfer by c2-mem-primitives-1730-20261101; dispatch
by learning-queue-dispatch-2213-20261101; reindex/integration by
codex-ram-realization-c2-20261101. Exact M1a412ad source and credit unchanged.
Outside-authoring-fleet review remains required.
---
 Complexity.lean                               |   3 +
 .../Realization/Client/MemoryQueue.lean       | 546 ++++++++++++++++++
 .../Client/MemoryQueueDispatch.lean           | 265 +++++++++
 .../WordRAM/Realization/Reindex.lean          |  54 ++
 .../WordRAMMemoryQueueDispatch.lean           | 186 ++++++
 ComplexityTests/WordRAMRealizationQueue.lean  | 185 ++++++
 ROADMAP.md                                    |   6 +-
 UPSTREAM.md                                   |   4 +
 8 files changed, 1247 insertions(+), 2 deletions(-)
 create mode 100644 Complexity/Computability/WordRAM/Realization/Client/MemoryQueue.lean
 create mode 100644 Complexity/Computability/WordRAM/Realization/Client/MemoryQueueDispatch.lean
 create mode 100644 Complexity/Computability/WordRAM/Realization/Reindex.lean
 create mode 100644 ComplexityTests/WordRAMMemoryQueueDispatch.lean
 create mode 100644 ComplexityTests/WordRAMRealizationQueue.lean

diff --git a/Complexity.lean b/Complexity.lean
index cb9df7d950..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
@@ -2568,6 +2570,7 @@ public import Complexity.Computability.WordRAM.Realization.MemoryBackend
 public import Complexity.Computability.WordRAM.Realization.Module
 public import Complexity.Computability.WordRAM.Realization.Primitive
 public import Complexity.Computability.WordRAM.Realization.Program
+public import Complexity.Computability.WordRAM.Realization.Reindex
 public import Complexity.Computability.WordRAM.Realization.Result
 public import Complexity.Computability.WordRAM.Realization.Witness
 public import Complexity.Computability.WordRAM.RegisterFrame
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..9b1ea70f1a
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueDispatch.lean
@@ -0,0 +1,265 @@
+/-
+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
+
+private def append {δ α : Type} {k l : ℕ} (input : δ ↪ (Fin k → ℕ))
+    (answer : α ↪ (Fin l → ℕ)) : δ × α ↪ (Fin (k + l) → ℕ) :=
+  (input.prodMap answer).trans (Fin.appendEquiv k l).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 := append MemoryQueue.layoutWords optionWords
+private def zeroInput := append replyInput word
+private def fuelInput := append zeroInput word
+private def stagedInput := append fuelInput (MemoryQueue.transferWords MemoryQueue.layoutWords)
+private def lastInput := append 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/Complexity/Computability/WordRAM/Realization/Reindex.lean b/Complexity/Computability/WordRAM/Realization/Reindex.lean
new file mode 100644
index 0000000000..18aea578f3
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Reindex.lean
@@ -0,0 +1,54 @@
+/-
+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.Basic
+
+/-!
+# Static live-register wiring
+
+A realization may consume selected words of a larger faithful environment without executing
+any computation. The equality of encoded inputs is explicit, and the register selection is
+fixed before runtime. This supplies layout arguments and query replies to existing method
+certificates while keeping other live words framed.
+
+## Main results
+
+* `Realizes.reindex`: pull a certificate back along a fixed register-index map.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization.Realizes
+
+open Cslib.DataStructure
+
+variable {B : Basis} {ε δ α : Type} {k m l : ℕ}
+
+/-- A fixed input-index map merely rewires registers. The semantic map must agree with that
+wiring on every encoded input; no host computation or runtime choice of code is granted. -/
+theorem reindex {p : δ → Memory.Prog α} {input : δ ↪ (Fin k → ℕ)}
+    {output : α ↪ (Fin l → ℕ)} {safe : ℕ → δ → Memory.State → Prop}
+    {work : δ → Memory.State → ℕ} (h : Realizes B p input output safe work)
+    (f : ε → δ) (env : ε ↪ (Fin m → ℕ)) (ix : Fin k → Fin m)
+    (hw : ∀ e i, input (f e) i = env e (ix i)) :
+    Realizes B (fun e => p (f e)) env output
+      (fun w e s => safe w (f e) s) (fun e s => work (f e) s) := by
+  obtain ⟨n, C, emit, he⟩ := h
+  refine ⟨n, C, fun frontier src tmp => emit frontier (src ∘ ix) tmp, ?_⟩
+  intro r frontier src tmp hi hd hf hs
+  obtain ⟨hnw, hrun⟩ := he frontier (src ∘ ix) tmp hi
+    (fun i j => hd (ix i) j) hf (fun i => hs (ix i))
+  refine ⟨hnw, ?_⟩
+  intro w e x hx hin hsafe hv
+  have hin' : x.regs ∘ (src ∘ ix) = input (f e) := by
+    funext i
+    exact (congrFun hin (ix i)).trans (hw e i).symm
+  exact hrun w (f e) x hx hin' hsafe hv
+
+end Cslib.WordRAM.Realization.Realizes
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

From a153124438bca43a9145dbdf80448885978f274c Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sun, 1 Nov 2026 21:33:45 -0500
Subject: [PATCH 2/2] refactor(WordRAM): reuse the canonical queue continuation
 encoding

Replace only the private Dispatch append encoding with existing appendWords. Source meaning, domains, work, native emitter and tests are unchanged. Codex authoring by roadmap_crypto; integration by roadmap_algorithms. Full integrated child validation follows before publication; worker focused checks pass. No selected abstract impact.
---
 .../Realization/Client/MemoryQueueDispatch.lean    | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

diff --git a/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueDispatch.lean b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueDispatch.lean
index 9b1ea70f1a..ef6bdebd3d 100644
--- a/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueDispatch.lean
+++ b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueDispatch.lean
@@ -42,10 +42,6 @@ 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
 
-private def append {δ α : Type} {k l : ℕ} (input : δ ↪ (Fin k → ℕ))
-    (answer : α ↪ (Fin l → ℕ)) : δ × α ↪ (Fin (k + l) → ℕ) :=
-  (input.prodMap answer).trans (Fin.appendEquiv k l).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
@@ -97,11 +93,11 @@ theorem realizes_enqueue (w C : ℕ) :
     (by intro d i; fin_cases i <;> rfl)
   simpa only [MemoryQueue.memMethods_enqueue] using h
 
-private def replyInput := append MemoryQueue.layoutWords optionWords
-private def zeroInput := append replyInput word
-private def fuelInput := append zeroInput word
-private def stagedInput := append fuelInput (MemoryQueue.transferWords MemoryQueue.layoutWords)
-private def lastInput := append stagedInput unitWords
+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