diff --git a/Complexity.lean b/Complexity.lean
index 9faed210d5..8dc48f686b 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -3016,10 +3016,16 @@ public import Complexity.DataStructure.PriorityQueue.WordRAM.FibonacciHeap.Model
 public import Complexity.DataStructure.PriorityQueue.WordRAM.FibonacciHeap.Program
 public import Complexity.DataStructure.PriorityQueue.WordRAM.FibonacciHeap.Trees
 public import Complexity.DataStructure.Queue.Memory
+public import Complexity.DataStructure.Queue.Memory.Transfer
 public import Complexity.DataStructure.Queue.Spec
-public import Complexity.DataStructure.Queue.WordRAM.Basic
-public import Complexity.DataStructure.Queue.WordRAM.Dynamic
 public import Complexity.DataStructure.Queue.WordRAM.Model
+public import Complexity.DataStructure.Queue.WordRAM.RegisterCorrectness
+public import Complexity.DataStructure.Queue.WordRAM.RegisterDynamic
+public import Complexity.DataStructure.Queue.WordRAM.RegisterExecution
+public import Complexity.DataStructure.Queue.WordRAM.RegisterMetadata
+public import Complexity.DataStructure.Queue.WordRAM.RegisterMethods
+public import Complexity.DataStructure.Queue.WordRAM.RegisterProgram
+public import Complexity.DataStructure.Queue.WordRAM.RegisterTransfer
 public import Complexity.DataStructure.Retroactive.Basic
 public import Complexity.DataStructure.SearchTree.Basic
 public import Complexity.DataStructure.SearchTree.Cost
diff --git a/Complexity/DataStructure/Queue/Memory/Transfer.lean b/Complexity/DataStructure/Queue/Memory/Transfer.lean
new file mode 100644
index 0000000000..1e01f9a4c3
--- /dev/null
+++ b/Complexity/DataStructure/Queue/Memory/Transfer.lean
@@ -0,0 +1,154 @@
+/-
+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.While
+public import Complexity.DataStructure.Queue.Memory
+
+/-!
+# Early-exit transfer for the memory queue
+
+The remaining number of rear elements is explicit loop state. A rear pop returning `none`
+sets it to zero, so the shared bounded while loop stops immediately. The source equalities
+preserve the original linked queue program, including its operation history.
+
+## Main definitions
+
+* `transferBody`: one rear pop and, when successful, one front push.
+
+## Main results
+
+* `transfer_eq_boundedWhile`: the existing transfer program is the shared early-exit loop.
+* `run_eq_allocPair_bind`: allocation followed by the original linked queue client.
+* `transfer_invariant`: the existing framed product preserves both stacks and moves the rear.
+
+## References
+
+The queue and its algorithmic references are in `Cslib.DataStructure.Queue.Spec`.
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.Queue.Memory
+
+open Cslib.WordRAM Cslib.WordRAM.Realization Cslib.DataStructure.Memory
+
+/-- Pop one rear element. An empty rear stops the loop; a successful move decreases the
+explicit remaining count. The loop guard excludes a zero count from this body. -/
+def transferBody (d : (Stack.Memory.Layout × Stack.Memory.Layout) × ℕ) : Prog ℕ := do
+  let a ← Stack.Memory.pop d.1.2
+  match a with
+  | none => pure 0
+  | some v => do
+      Stack.Memory.push d.1.1 v
+      pure (d.2 - 1)
+
+/-- Forgetting the loop's remaining count leaves exactly one step of the original transfer. -/
+theorem transferBody_forget (L₁ L₂ : Stack.Memory.Layout) (w C r : ℕ) :
+    (transferBody ((L₁, L₂), r)).bind (fun _ => pure ()) =
+      link (Methods.prod (Stack.Memory.methods L₁ w C) (Stack.Memory.methods L₂ w C))
+        (Queue.transfer 1) := by
+  simp only [transferBody, Queue.transfer, link, Methods.prod, Stack.Memory.methods,
+    PFunctor.FreeM.liftM, PFunctor.FreeM.bind_eq_bind, bind_assoc]
+  congr 1
+  funext a
+  cases a <;> simp [PFunctor.FreeM.liftM, Methods.prod, Stack.Memory.methods]
+
+/-- The bounded while has exactly the original source program, with no inactive tail queries
+or extra memory operations after an early empty pop. The cutoff bounds the remaining count. -/
+theorem transfer_eq_boundedWhile (L₁ L₂ : Stack.Memory.Layout) (w C fuel n : ℕ)
+    (hn : n ≤ fuel) :
+    link (Methods.prod (Stack.Memory.methods L₁ w C) (Stack.Memory.methods L₂ w C))
+        (Queue.transfer n) =
+      (boundedWhile (fun _ r => 0 < r) transferBody (L₁, L₂) fuel n).bind
+        (fun _ => pure ()) := by
+  induction fuel generalizing n with
+  | zero =>
+    have : n = 0 := by omega
+    subst n
+    rfl
+  | succ fuel ih =>
+    cases n with
+    | zero => simp [Queue.transfer, boundedWhile, link]
+    | succ n =>
+      simp only [Queue.transfer, link, PFunctor.FreeM.liftM, Methods.prod,
+        Stack.Memory.methods, boundedWhile, Nat.zero_lt_succ, ↓reduceIte, transferBody,
+        Nat.add_sub_cancel, PFunctor.FreeM.bind_eq_bind, bind_assoc]
+      congr 1
+      funext a
+      cases a with
+      | none => simp [boundedWhile_of_not]
+      | some v =>
+        simp only [PFunctor.FreeM.liftM]
+        exact congrArg (fun p => (Stack.Memory.push L₁ v).bind (fun _ => p))
+          (ih n (by omega))
+
+/-- The current allocator allocates its two stack handles and then links the unchanged queue
+methods through their product. This is equality of programs, before selecting a memory state. -/
+theorem run_eq_allocPair_bind (w C : ℕ) {α : Type}
+    (p : (Queue.WordRAM.spec w C).Client α) :
+    run w C p = (Allocator.allocPair (Stack.Memory.allocator w C)
+      (Stack.Memory.allocator w C)).bind (fun L => link ((allocator w C).methods L) p) := rfl
+
+/-- The source transfer preserves the two existing storage invariants and reverses the rear
+into the front. The generic framed product supplies noninterference; no replacement invariant
+or instruction-level proof is needed. -/
+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 : State} (hw : 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 := link (Methods.prod (Stack.Memory.methods L₁ w C)
+      (Stack.Memory.methods L₂ w C)) (Queue.transfer n)
+    let s' := (spec w).clientState s p
+    (spec w).ValidHistory s ((spec w).clientHistory s p) ∧
+      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 ∧
+      Stack.Memory.abs L₁ s' = (Stack.Memory.abs L₂ s).reverse ++ Stack.Memory.abs L₁ s := by
+  let M := (Stack.Memory.framed h₁).prod (Stack.Memory.framed h₂)
+  have hi : M.inv s := ⟨hs₁, hs₂, hd, by
+    change Cslib.WordRAM.Fits w (s.frontier + (0 + 0))
+    simpa only [Nat.add_zero] using hw.frontier_fits⟩
+  have hn' : n = (Stack.Memory.abs L₂ s).length := by
+    rw [Stack.Memory.length_abs, hn]
+  have hv : (boundedStacks w C).ValidHistory (M.abs s)
+      ((boundedStacks w C).clientHistory (M.abs s) (Queue.transfer n)) := by
+    rw [clientHistory_boundedStacks, hn']
+    change (boundedStacks w C).ValidHistory (Stack.Memory.abs L₁ s, Stack.Memory.abs L₂ s)
+      ((stackPair ℕ).runClient (Stack.Memory.abs L₁ s, Stack.Memory.abs L₂ s)
+        (Queue.transfer (Stack.Memory.abs L₂ s).length)).2.2
+    rw [Queue.transfer_run]
+    apply validHistory_transferTrace
+    · simpa only [Stack.Memory.length_abs] using hlen
+    · intro v hv
+      simp only [Stack.Memory.abs, List.mem_reverse, Cslib.WordRAM.Block.entries,
+        List.mem_map] at hv
+      obtain ⟨i, _, rfl⟩ := hv
+      exact hw.mem_fits _
+  obtain ⟨hvE, _, habs, hsE⟩ := M.toRefinement.simulates_client (Queue.transfer n) hi hv
+  have habs' : M.abs ((spec w).clientState s (link M.methods (Queue.transfer n))) =
+      ((Stack.Memory.abs L₂ s).reverse ++ Stack.Memory.abs L₁ s, []) := by
+    rw [habs, clientState_boundedStacks, hn']
+    exact congrArg (fun t => t.2.1) (Queue.transfer_run (Stack.Memory.abs L₁ s)
+      (Stack.Memory.abs L₂ s))
+  let s' := (spec w).clientState s (link (Methods.prod (Stack.Memory.methods L₁ w C)
+    (Stack.Memory.methods L₂ w C)) (Queue.transfer n))
+  have hfront : Stack.Memory.abs L₁ s' =
+      (Stack.Memory.abs L₂ s).reverse ++ Stack.Memory.abs L₁ s := congrArg Prod.fst habs'
+  have hrear : Stack.Memory.abs L₂ s' = [] := congrArg Prod.snd habs'
+  have hfrontLength := congrArg List.length hfront
+  have hrearLength := congrArg List.length hrear
+  simp only [Stack.Memory.length_abs, List.length_append, List.length_reverse,
+    List.length_nil, hn] at hfrontLength hrearLength
+  refine ⟨hvE, ?_, hsE.1, hsE.2.1, hrearLength, ?_, hfront⟩
+  · rw [← (spec w).run_runClient]
+    exact hw.run hvE
+  · simpa only [Nat.add_comm] using hfrontLength
+
+end Cslib.DataStructure.Queue.Memory
diff --git a/Complexity/DataStructure/Queue/WordRAM/Basic.lean b/Complexity/DataStructure/Queue/WordRAM/Basic.lean
deleted file mode 100644
index b573762272..0000000000
--- a/Complexity/DataStructure/Queue/WordRAM/Basic.lean
+++ /dev/null
@@ -1,395 +0,0 @@
-/-
-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.DataStructure.Queue.WordRAM.Model
-public import Complexity.Computability.WordRAM.Dynamic
-
-/-!
-# Two stacks implementing a queue in shared RAM
-
-Two disjoint reserved blocks hold bottom-first stack arrays. Enqueue pushes onto the rear;
-dequeue transfers the rear into an empty front before popping. All address arithmetic, memory
-accesses, loop tests and operation dispatch are machine instructions. Empty live prefixes do
-not require clearing the reserved memory.
-
-## Main definitions
-
-* `tag`, `arg`, `frontLen`, `frontBase`, `backLen`, `backBase`, `addr`, `out`, `present`, `zero`,
-  `one`: register allocation for the two-stack queue.
-* `Rep`, `footprint`: the bounded shared-memory representation of the two top-first lists and its
-  reserved memory footprint.
-* `enqueue`, `move`, `transfer`, `pop`, `dequeue`, `program`, `bodyCost`: structured queue
-  operations, the fixed operation dispatcher, and its per-operation instruction count.
-* `implementation`: its argument and result conventions.
-* `initializeCode`: six charged writes installing an empty representation.
-
-## Main results
-
-* `execute`: exact instruction execution, observations, representation and memory frame.
-* `initialize_exec`: initialization from arbitrary bounded machine data without clearing memory.
-
-## References
-
-* [Cormen, Leiserson, Rivest and Stein, *Introduction to Algorithms*][CLRS2009].
--/
-
-@[expose] public section
-
-namespace Cslib.DataStructure.Queue.WordRAM
-
-open Cslib.WordRAM Cslib.DataStructure.Queue
-
-/-- Operation tag: enqueue zero, dequeue one. -/
-abbrev tag : Fin 11 := 0
-/-- Enqueued word. -/
-abbrev arg : Fin 11 := 1
-/-- Front stack length. -/
-abbrev frontLen : Fin 11 := 2
-/-- Front block base. -/
-abbrev frontBase : Fin 11 := 3
-/-- Rear stack length. -/
-abbrev backLen : Fin 11 := 4
-/-- Rear block base. -/
-abbrev backBase : Fin 11 := 5
-/-- Temporary address. -/
-abbrev addr : Fin 11 := 6
-/-- Returned word. -/
-abbrev out : Fin 11 := 7
-/-- Returned presence flag. -/
-abbrev present : Fin 11 := 8
-/-- Constant zero. -/
-abbrev zero : Fin 11 := 9
-/-- Constant one. -/
-abbrev one : Fin 11 := 10
-
-/-- Both stack arrays live in one bounded memory, with one common capacity bound. -/
-structure Rep (w base capacity : ℕ) (front back : List ℕ) (x : Data 11) : Prop where
-  bounded : x.Bounded w
-  frontBase_eq : x.regs frontBase = base
-  backBase_eq : x.regs backBase = base + capacity
-  frontLen_eq : x.regs frontLen = front.length
-  backLen_eq : x.regs backLen = back.length
-  zero_eq : x.regs zero = 0
-  one_eq : x.regs one = 1
-  size_le : front.length + back.length ≤ capacity
-  front_contents : ∀ i : Fin front.length, x.mem (base + i.val) = front.reverse[i.val]
-  back_contents : ∀ i : Fin back.length,
-    x.mem (base + capacity + i.val) = back.reverse[i.val]
-
-/-- The fixed reserved region, including currently unused cells. -/
-def footprint (base capacity : ℕ) : Finset ℕ :=
-  (Block.mk base (2 * capacity)).footprint
-
-/-- Enqueue writes the next rear cell and advances the rear length. -/
-def enqueue : Code .standard 11 := ram[
-  addr ← backBase + backLen; *addr ← arg; backLen ← backLen + one; out ← zero ]
-
-/-- Move the top rear word onto the front stack. -/
-def move : Code .standard 11 := ram[
-  backLen ← backLen - one; addr ← backBase + backLen; out ← *addr;
-  addr ← frontBase + frontLen; *addr ← out; frontLen ← frontLen + one ]
-
-/-- Reverse the rear stack onto the front, testing each iteration on machine registers. -/
-def transfer : Code .standard 11 := ram[while zero < backLen do [ ⟪move⟫ ]]
-
-/-- Pop the front, distinguishing the empty queue from a returned zero. -/
-def pop : Code .standard 11 := ram[
-  if frontLen = zero then [ out ← zero; present ← zero ] else [
-    frontLen ← frontLen - one; addr ← frontBase + frontLen; out ← *addr; present ← one ] ]
-
-/-- Transfer only when the front is empty. -/
-def dequeue : Code .standard 11 := ram[
-  if frontLen = zero then [ ⟪transfer⟫; ⟪pop⟫ ] else [ ⟪pop⟫ ] ]
-
-/-- One fixed dispatcher, independent of queue contents, capacity, and operation arguments. -/
-def program : Code .standard 11 := ram[
-  if tag = zero then [ ⟪enqueue⟫ ] else [ ⟪dequeue⟫ ] ]
-
-/-- Register calling convention for the fixed queue dispatcher. -/
-def implementation (w capacity : ℕ) : DynamicProgram (spec w capacity) 11 where
-  code := program
-  output := out
-  input i := i == tag || i == arg
-  encode o i := if i = tag then
-    match o with | .enqueue _ => 0 | .dequeue => 1
-    else match o with | .enqueue v => v | .dequeue => 0
-  decode o regs := match o with
-    | .enqueue _ => some ()
-    | .dequeue => some (if regs present = 0 then none else some (regs out))
-
-/-- Enqueue body correctness with an exact four-instruction execution. -/
-private theorem enqueue_exec {w base capacity v : ℕ} {front back : List ℕ} {x : Data 11}
-    (hc : Fits w (base + 2 * capacity)) (hr : Rep w base capacity front back x)
-    (hs : front.length + back.length < capacity) (hv : x.regs arg = v) :
-    ∃ y, Exec w enqueue x y 4 ∧ Rep w base capacity front (v :: back) y ∧
-      Modifies (footprint base capacity) x.mem y.mem := by
-  have ha : Fits w (base + capacity + back.length) := hc.of_le (by omega)
-  have hl : Fits w (back.length + 1) := hc.of_le (by omega)
-  let y := ((x.set addr (base + capacity + back.length)).write
-    (base + capacity + back.length) v).set backLen (back.length + 1) |>.set out 0
-  have he : Exec w enqueue x y 4 := by
-    ram_eval [enqueue, y, hr.backBase_eq, hr.backLen_eq, hr.one_eq, hr.zero_eq, hv, ha, hl]
-  refine ⟨y, he, ⟨he.bounded hr.bounded, ?_, ?_, ?_, ?_, ?_, ?_,
-    by simp only [List.length_cons]; omega, ?_, ?_⟩, ?_⟩
-  · simpa +decide [y, Data.set, Data.write] using hr.frontBase_eq
-  · simpa +decide [y, Data.set, Data.write] using hr.backBase_eq
-  · simpa +decide [y, Data.set, Data.write] using hr.frontLen_eq
-  · simp +decide [y, Data.set, Data.write]
-  · simpa +decide [y, Data.set, Data.write] using hr.zero_eq
-  · simpa +decide [y, Data.set, Data.write] using hr.one_eq
-  · intro i
-    have hne : base + i.val ≠ base + capacity + back.length := by have := i.isLt; omega
-    simpa [y, Data.set, Data.write, Function.update_of_ne hne] using hr.front_contents i
-  · intro i
-    by_cases hi : i.val < back.length
-    · have hne : base + capacity + i.val ≠ base + capacity + back.length := by omega
-      simpa [y, Data.set, Data.write, List.reverse_cons, List.getElem_append, hi,
-        Function.update_of_ne hne] using hr.back_contents ⟨i.val, hi⟩
-    · have hi' : i.val = back.length := by
-        have := i.isLt
-        simp only [List.length_cons] at this
-        omega
-      simp [y, Data.set, Data.write, List.reverse_cons, hi']
-  · exact Modifies.write_of_owns ⟨by omega, by omega⟩ v
-
-/-- A rear-to-front move performs six instructions and preserves the reserved-region frame. -/
-private theorem move_exec {w base capacity v : ℕ} {front back : List ℕ} {x : Data 11}
-    (hc : Fits w (base + 2 * capacity)) (hr : Rep w base capacity front (v :: back) x) :
-    ∃ y, Exec w move x y 6 ∧ Rep w base capacity (v :: front) back y ∧
-      Modifies (footprint base capacity) x.mem y.mem := by
-  have hs := hr.size_le
-  simp only [List.length_cons] at hs
-  have hl : x.regs backLen = back.length + 1 := hr.backLen_eq
-  have hb : Fits w back.length := hc.of_le (by omega)
-  have ha : Fits w (base + capacity + back.length) := hc.of_le (by omega)
-  have hf : Fits w (base + front.length) := hc.of_le (by omega)
-  have hi : Fits w (front.length + 1) := hc.of_le (by omega)
-  have hread : x.mem (base + capacity + back.length) = v := by
-    simpa [List.reverse_cons] using hr.back_contents ⟨back.length, by simp⟩
-  let y := (((((x.set backLen back.length).set addr (base + capacity + back.length)).set
-    out v).set addr (base + front.length)).write (base + front.length) v).set
-    frontLen (front.length + 1)
-  have he : Exec w move x y 6 := by
-    ram_eval [move, y, hr.frontBase_eq, hr.backBase_eq, hr.frontLen_eq, hl, hr.one_eq,
-      Nat.add_sub_cancel, hb, ha, hf, hi, hread]
-  refine ⟨y, he, ⟨he.bounded hr.bounded, ?_, ?_, ?_, ?_, ?_, ?_,
-    by simp only [List.length_cons]; omega, ?_, ?_⟩, ?_⟩
-  · simpa +decide [y, Data.set, Data.write] using hr.frontBase_eq
-  · simpa +decide [y, Data.set, Data.write] using hr.backBase_eq
-  · simp +decide [y, Data.set, Data.write]
-  · simp +decide [y, Data.set, Data.write]
-  · simpa +decide [y, Data.set, Data.write] using hr.zero_eq
-  · simpa +decide [y, Data.set, Data.write] using hr.one_eq
-  · intro i
-    by_cases hij : i.val < front.length
-    · have hne : base + i.val ≠ base + front.length := by omega
-      simpa [y, Data.set, Data.write, List.reverse_cons, List.getElem_append, hij,
-        Function.update_of_ne hne] using hr.front_contents ⟨i.val, hij⟩
-    · have hi' : i.val = front.length := by
-        have := i.isLt
-        simp only [List.length_cons] at this
-        omega
-      simp [y, Data.set, Data.write, List.reverse_cons, hi']
-  · intro i
-    have hne : base + capacity + i.val ≠ base + front.length := by omega
-    have hr' := hr.back_contents ⟨i.val, by simp⟩
-    simpa [y, Data.set, Data.write, List.reverse_cons, List.getElem_append, i.isLt,
-      Function.update_of_ne hne] using hr'
-  · exact Modifies.write_of_owns ⟨by omega, by omega⟩ v
-
-/-- Transfer costs eight instructions per moved word and two instructions to exit the loop. -/
-private theorem transfer_exec {w base capacity : ℕ} {front back : List ℕ} {x : Data 11}
-    (hc : Fits w (base + 2 * capacity)) (hr : Rep w base capacity front back x) :
-    ∃ y, Exec w transfer x y (8 * back.length + 2) ∧
-      Rep w base capacity (back.reverse ++ front) [] y ∧
-      Modifies (footprint base capacity) x.mem y.mem := by
-  induction back generalizing front x with
-  | nil =>
-    refine ⟨x, ?_, hr, Modifies.refl _ _⟩
-    apply Exec.loop_exit
-    change ¬x.regs zero < x.regs backLen
-    rw [hr.zero_eq, hr.backLen_eq]
-    simp
-  | cons v back ih =>
-    obtain ⟨y, he, hy, hf⟩ := move_exec hc hr
-    obtain ⟨z, hz, hrz, hfz⟩ := ih hy
-    refine ⟨z, ?_, ?_, ?_⟩
-    · have he' := Exec.loop_iter (c := Cond.lt zero backLen) (by
-        change x.regs zero < x.regs backLen
-        rw [hr.zero_eq, hr.backLen_eq]
-        simp) he hz
-      convert he' using 1
-      · rfl
-      · simp only [List.length_cons]
-        omega
-    · simpa only [List.reverse_cons, List.append_assoc, List.singleton_append] using hrz
-    · exact fun a ha => (hfz a ha).trans (hf a ha)
-
-/-- Front-pop execution counts include the empty/nonempty branch and distinguish returned zero. -/
-private theorem pop_exec {w base capacity : ℕ} {front back : List ℕ} {x : Data 11}
-    (hc : Fits w (base + 2 * capacity)) (hr : Rep w base capacity front back x) :
-    ∃ y, Exec w pop x y (if front = [] then 3 else 6) ∧
-      Rep w base capacity front.tail back y ∧
-      (if y.regs present = 0 then none else some (y.regs out)) = front.head? ∧
-      y.mem = x.mem := by
-  cases front with
-  | nil =>
-    let y := (x.set out 0).set present 0
-    have he : Exec w pop x y 3 := by
-      ram_eval [pop, y, hr.frontLen_eq, hr.zero_eq]
-    refine ⟨y, he, ⟨he.bounded hr.bounded, ?_, ?_, ?_, ?_, ?_, ?_, hr.size_le,
-      fun i => Fin.elim0 i, hr.back_contents⟩, ?_, rfl⟩
-    · simpa +decide [y, Data.set] using hr.frontBase_eq
-    · simpa +decide [y, Data.set] using hr.backBase_eq
-    · simpa +decide [y, Data.set] using hr.frontLen_eq
-    · simpa +decide [y, Data.set] using hr.backLen_eq
-    · simpa +decide [y, Data.set] using hr.zero_eq
-    · simpa +decide [y, Data.set] using hr.one_eq
-    · simp [y, Data.set]
-  | cons v front =>
-    have hs := hr.size_le
-    simp only [List.length_cons] at hs
-    have hl : x.regs frontLen = front.length + 1 := hr.frontLen_eq
-    have hf : Fits w front.length := hc.of_le (by omega)
-    have ha : Fits w (base + front.length) := hc.of_le (by omega)
-    have hread : x.mem (base + front.length) = v := by
-      simpa [List.reverse_cons] using hr.front_contents ⟨front.length, by simp⟩
-    let y := (((x.set frontLen front.length).set addr (base + front.length)).set out v).set
-      present 1
-    have he : Exec w pop x y 6 := by
-      ram_eval [pop, y, hl, hr.zero_eq, hr.one_eq, hr.frontBase_eq, hread, hf, ha,
-        Nat.add_sub_cancel, Nat.add_eq_zero_iff, and_false]
-    refine ⟨y, he, ⟨he.bounded hr.bounded, ?_, ?_, ?_, ?_, ?_, ?_,
-      by change front.length + back.length ≤ capacity; omega,
-      ?_, hr.back_contents⟩, ?_, rfl⟩
-    · simpa +decide [y, Data.set] using hr.frontBase_eq
-    · simpa +decide [y, Data.set] using hr.backBase_eq
-    · simp +decide [y, Data.set]
-    · simpa +decide [y, Data.set] using hr.backLen_eq
-    · simpa +decide [y, Data.set] using hr.zero_eq
-    · simpa +decide [y, Data.set] using hr.one_eq
-    · intro i
-      have hij : i.val < front.length := i.isLt
-      have hr' := hr.front_contents ⟨i.val, by simp only [List.length_cons]; omega⟩
-      simpa [y, Data.set, List.reverse_cons, List.getElem_append, hij] using hr'
-    · simp +decide [y, Data.set]
-
-/-- Exact instruction count of a dispatched operation, excluding the final halt. -/
-def bodyCost (front back : List ℕ) : QueueOp ℕ → ℕ
-  | .enqueue _ => 5
-  | .dequeue => if front = [] then 8 * back.length + (if back = [] then 8 else 11) else 10
-
-/-- Encoded operation arguments for any valid queue operation fit in a `w`-bit word. -/
-theorem arguments_fit {w capacity : ℕ} (h1 : Fits w 1) {q : List ℕ} (o : QueueOp ℕ)
-    (hv : (spec w capacity).valid q o) (i : Fin 11) :
-    Fits w ((implementation w capacity).encode o i) := by
-  cases o with
-  | enqueue v =>
-    change Fits w (if i = tag then 0 else v)
-    split
-    · exact fits_zero w
-    · exact hv.2
-  | dequeue =>
-    change Fits w (if i = tag then 1 else 0)
-    split
-    · exact h1
-    · exact fits_zero w
-
-private theorem prepare_rep {w base capacity : ℕ} {front back : List ℕ} {x : Data 11}
-    (hr : Rep w base capacity front back x) (o : QueueOp ℕ)
-    (hv : (spec w capacity).valid (contents (front, back)) o) :
-    Rep w base capacity front back ((implementation w capacity).prepare o x) := by
-  have hb : ((implementation w capacity).prepare o x).Bounded w :=
-    (implementation w capacity).prepare_bounded hr.bounded
-      (fun i _ => arguments_fit (hr.one_eq ▸ hr.bounded.1 one) o hv i)
-  refine ⟨hb, ?_, ?_, ?_, ?_, ?_, ?_, hr.size_le, hr.front_contents, hr.back_contents⟩
-  all_goals first
-    | simpa +decide [implementation, DynamicProgram.prepare] using hr.frontBase_eq
-    | simpa +decide [implementation, DynamicProgram.prepare] using hr.backBase_eq
-    | simpa +decide [implementation, DynamicProgram.prepare] using hr.frontLen_eq
-    | simpa +decide [implementation, DynamicProgram.prepare] using hr.backLen_eq
-    | simpa +decide [implementation, DynamicProgram.prepare] using hr.zero_eq
-    | simpa +decide [implementation, DynamicProgram.prepare] using hr.one_eq
-
-/-- Every valid operation executes the fixed dispatcher with its exact instruction count,
-implements the two-stack transition, and preserves every cell outside the reserved region. -/
-theorem execute {w base capacity : ℕ} {front back : List ℕ} {x : Data 11}
-    (hc : Fits w (base + 2 * capacity)) (hr : Rep w base capacity front back x)
-    (o : QueueOp ℕ) (hv : (spec w capacity).valid (contents (front, back)) o) :
-    ∃ y, Exec w program ((implementation w capacity).prepare o x) y (bodyCost front back o) ∧
-      (implementation w capacity).decode o y.regs = some (pairStep (front, back) o).2 ∧
-      Rep w base capacity (pairStep (front, back) o).1.1 (pairStep (front, back) o).1.2 y ∧
-      Modifies (footprint base capacity) x.mem y.mem := by
-  have hp := prepare_rep hr o hv
-  cases o with
-  | enqueue v =>
-    have hs : front.length + back.length < capacity := by
-      simpa only [contents_length] using hv.1
-    have ha : ((implementation w capacity).prepare (.enqueue v) x).regs arg = v := by
-      simp +decide [implementation, DynamicProgram.prepare]
-    obtain ⟨y, he, hy, hf⟩ := enqueue_exec hc hp hs ha
-    refine ⟨y, ?_, rfl, hy, hf⟩
-    exact Exec.branch_pos (by
-      change _ = _
-      simp +decide [implementation, DynamicProgram.prepare, hr.zero_eq]) he
-  | dequeue =>
-    have ht : ¬(Cond.eq tag zero).Holds ((implementation w capacity).prepare .dequeue x) := by
-      change ¬_ = _
-      simp +decide [implementation, DynamicProgram.prepare, hr.zero_eq]
-    cases front with
-    | nil =>
-      obtain ⟨y, he, hy, hf⟩ := transfer_exec hc hp
-      have hy' : Rep w base capacity back.reverse [] y := by simpa using hy
-      obtain ⟨z, hz, hrz, ha, hm⟩ := pop_exec hc hy'
-      refine ⟨z, ?_, ?_, hrz, ?_⟩
-      · have hbranch := Exec.branch_neg (pos := enqueue) ht
-          (Exec.branch_pos (c := Cond.eq frontLen zero) (neg := pop) (by
-            change _ = _
-            rw [hp.frontLen_eq, hp.zero_eq]
-            rfl) (Exec.seq he hz))
-        convert hbranch using 1
-        · rfl
-        · simp only [bodyCost, ↓reduceIte, List.reverse_eq_nil_iff]
-          split <;> omega
-      · exact congrArg some ha
-      · intro a hab
-        rw [hm]
-        exact hf a hab
-    | cons v front =>
-      obtain ⟨y, he, hy, ha, hm⟩ := pop_exec hc hp
-      refine ⟨y, ?_, congrArg some ha, hy, ?_⟩
-      · exact Exec.branch_neg ht (Exec.branch_neg (by
-          change ¬_ = _
-          rw [hp.frontLen_eq, hp.zero_eq]
-          simp) he)
-      · intro a _
-        exact congrFun hm a
-
-/-- Install an empty queue using six register instructions, with no writes to reserved memory. -/
-def initializeCode (base capacity : ℕ) : Code .standard 11 := ram[
-  frontBase ← #base; backBase ← #(base + capacity); frontLen ← #0; backLen ← #0;
-  zero ← #0; one ← #1 ]
-
-/-- Initialization accepts arbitrary bounded registers and memory. Only the six representation
-registers change; both reserved live prefixes are empty, so memory remains untouched. -/
-theorem initialize_exec {w base capacity : ℕ} {x : Data 11} (hx : x.Bounded w)
-    (h1 : Fits w 1) (hc : Fits w (base + 2 * capacity)) :
-    ∃ y, Exec w (initializeCode base capacity) x y 6 ∧ Rep w base capacity [] [] y ∧
-      y.mem = x.mem := by
-  let y := (((((x.set frontBase base).set backBase (base + capacity)).set frontLen 0).set
-    backLen 0).set zero 0).set one 1
-  have hf : Fits w base := hc.of_le (by omega)
-  have hb : Fits w (base + capacity) := hc.of_le (by omega)
-  have he : Exec w (initializeCode base capacity) x y 6 := by
-    ram_eval [initializeCode, y, hf, hb, h1]
-  refine ⟨y, he, ⟨he.bounded hx, ?_, ?_, ?_, ?_, ?_, ?_, Nat.zero_le _,
-    fun i => Fin.elim0 i, fun i => Fin.elim0 i⟩, rfl⟩
-  all_goals simp +decide [y, Data.set]
-
-end Cslib.DataStructure.Queue.WordRAM
diff --git a/Complexity/DataStructure/Queue/WordRAM/Dynamic.lean b/Complexity/DataStructure/Queue/WordRAM/Dynamic.lean
deleted file mode 100644
index e37644998e..0000000000
--- a/Complexity/DataStructure/Queue/WordRAM/Dynamic.lean
+++ /dev/null
@@ -1,165 +0,0 @@
-/-
-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.DataStructure.Queue.WordRAM.Basic
-public import Complexity.DataStructure.StateTransition.Amortized
-
-/-!
-# Correctness and amortized instruction cost of a RAM queue
-
-The mathematical client sees only a FIFO list. The realization hides how that list is split
-between the two arrays. A dequeue can move every rear element, but each enqueue deposits eight
-credits: six instructions move an element and two instructions control that loop iteration.
-Consequently every admissible history costs at most fourteen instructions per operation,
-plus the initial rear credit. The final unused credit is retained in the inequality.
-
-These are actual RAM operation instructions, including each call's halt. The operation interface
-still uses externally delivered argument registers; arbitrary pure computation in a client's
-Lean continuation is not included in this bound. Initialization is a separate six-instruction
-program. The arrays reserve twice the queue capacity, while at most one capacity's worth of
-values are live. No allocator or dynamically growing capacity is assumed.
-
-## Main definitions
-
-* `QueueRep`: the FIFO representation hiding the split into two stacks.
-* `certificate`: a semantic realization of the bounded queue interface.
-* `potential`: rear-stack credit read from the persistent length register.
-* `amortized`: the separate instruction-cost certificate with rear-stack potential.
-
-## Main results
-
-* `run_client`: correct adaptive execution and the amortized native instruction bound.
-* `frame`: every operation preserves any disjoint heap assertion.
-
-## References
-
-* [Cormen, Leiserson, Rivest and Stein, *Introduction to Algorithms*, Chapters 10 and 17][CLRS2009].
--/
-
-@[expose] public section
-
-namespace Cslib.DataStructure.Queue.WordRAM
-
-open Cslib.WordRAM Cslib.DataStructure.Queue
-
-/-- The two reserved blocks contain exactly twice the queue capacity in word cells. -/
-theorem footprint_card (base capacity : ℕ) : (footprint base capacity).card = 2 * capacity :=
-  Block.card_footprint _
-
-/-- A client observes a FIFO list, while the machine retains a hidden split between two stacks. -/
-def QueueRep (w base capacity : ℕ) (q : List ℕ) (x : Data 11) : Prop :=
-  ∃ front back, q = contents (front, back) ∧ Rep w base capacity front back x
-
-/-- The fixed dispatcher implements the bounded FIFO specification. -/
-def certificate {w base capacity : ℕ} (h1 : Fits w 1)
-    (hc : Fits w (base + 2 * capacity)) :
-    DynamicCertificate (implementation w capacity) w :=
-  DynamicCertificate.ofFn
-    (rep := QueueRep w base capacity)
-    (bounded := fun h => by obtain ⟨_, _, _, hr⟩ := h; exact hr.bounded)
-    (arguments_fit := fun o hv i _ => arguments_fit h1 o hv i)
-    (execute := fun o hr hv => by
-      obtain ⟨front, back, rfl, hr⟩ := hr
-      obtain ⟨y, he, ha, hy, _⟩ := execute hc hr o hv
-      have hs := pairStep_correct (front, back) o
-      refine ⟨y, _, he, ?_, ?_⟩
-      · exact ha.trans (congrArg some (congrArg Prod.snd hs))
-      · exact ⟨_, _, (congrArg Prod.fst hs).symm, hy⟩)
-
-/-- The expensive transfer consumes eight credits per rear element, including loop control.
-The final halt contributes the extra one in the left side. -/
-private theorem bodyCost_potential (front back : List ℕ) (o : QueueOp ℕ) :
-    bodyCost front back o + 1 + 8 * (pairStep (front, back) o).1.2.length ≤
-      14 + 8 * back.length := by
-  cases o with
-  | enqueue v => simp only [bodyCost, pairStep, List.length_cons]; omega
-  | dequeue => cases front <;> cases back <;>
-      simp only [bodyCost, pairStep, List.cons_ne_nil, ↓reduceIte,
-        List.length_nil, List.length_cons] <;> omega
-
-/-- Every native operation has the exact charged body cost plus its final halt. -/
-theorem instructions_eq {w base capacity : ℕ} (hc : Fits w (base + 2 * capacity))
-    {front back : List ℕ} {x y : Data 11} {o : QueueOp ℕ}
-    {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace}
-    (hr : Rep w base capacity front back x)
-    (hv : (spec w capacity).valid (contents (front, back)) o)
-    (he : (implementation w capacity).ExecOp w x o a y trace) :
-    trace.instructions = bodyCost front back o + 1 := by
-  obtain ⟨z, hz, _, _, _⟩ := execute hc hr o hv
-  exact (he.eq_of_exec hz).2
-
-/-- Rear-stack credit is read from the concrete persistent length register. -/
-def potential (x : Data 11) : ℕ := 8 * x.regs backLen
-
-/-- Amortized constant instruction cost is certified separately from FIFO correctness. -/
-theorem amortized {w base capacity : ℕ} (h1 : Fits w 1)
-    (hc : Fits w (base + 2 * capacity)) :
-    DataStructure.Amortized (certificate h1 hc).impl
-      DynamicProgram.OperationTrace.instructions (fun _ x => potential x) (fun _ _ => 14) :=
-  DataStructure.Amortized.ofFn fun hr hv he => by
-    obtain ⟨front, back, rfl, hr⟩ := hr
-    obtain ⟨z, hz, _, hrz, _⟩ := execute hc hr _ hv
-    obtain ⟨rfl, hn⟩ := he.eq_of_exec hz
-    rw [hn]
-    simpa only [potential, hr.backLen_eq, hrz.backLen_eq] using
-      bodyCost_potential front back _
-
-/-- Every admissible adaptive client has a correct native execution with a telescoping bound.
-This sums operation calls; the externally supplied client controller is not machine code. -/
-theorem run_client {w base capacity : ℕ} (h1 : Fits w 1)
-    (hc : Fits w (base + 2 * capacity)) {α : Type} (p : (spec w capacity).Client α)
-    {q : List ℕ} {x : Data 11} (hr : QueueRep w base capacity q x)
-    (hv : (spec w capacity).ValidHistory q ((spec w capacity).runClient q p).2.2) :
-    ∃ y traces, DataStructure.Executes ((implementation w capacity).ExecOp w) p x
-        ((spec w capacity).runClient q p).1 y traces ∧
-      QueueRep w base capacity ((spec w capacity).runClient q p).2.1 y ∧
-      DataStructure.total DynamicProgram.OperationTrace.instructions traces + potential y ≤
-        ((spec w capacity).runClient q p).2.2.length * 14 + potential x :=
-  (amortized h1 hc).exists_executes_const p hr hv
-
-/-- Starting with arbitrary bounded data, charge the six initialization instructions before
-summing the actual queue calls. Empty regions need no zeroing; controller computation and
-external argument delivery retain the boundary stated in `run_client`. -/
-theorem run_initialized {w base capacity : ℕ} (h1 : Fits w 1)
-    (hc : Fits w (base + 2 * capacity)) {α : Type} (p : (spec w capacity).Client α)
-    {x : Data 11} (hx : x.Bounded w)
-    (hv : (spec w capacity).ValidHistory [] ((spec w capacity).runClient [] p).2.2) :
-    ∃ ready y traces, Exec w (initializeCode base capacity) x ready 6 ∧
-      DataStructure.Executes ((implementation w capacity).ExecOp w) p ready
-        ((spec w capacity).runClient [] p).1 y traces ∧
-      QueueRep w base capacity ((spec w capacity).runClient [] p).2.1 y ∧
-      6 + DataStructure.total DynamicProgram.OperationTrace.instructions traces + potential y ≤
-        6 + ((spec w capacity).runClient [] p).2.2.length * 14 := by
-  obtain ⟨ready, hi, hr, _⟩ := initialize_exec hx h1 hc
-  have hp : potential ready = 0 := by simp [potential, hr.backLen_eq]
-  obtain ⟨y, traces, he, hy, hb⟩ := run_client (q := []) h1 hc p ⟨[], [], rfl, hr⟩ hv
-  exact ⟨ready, y, traces, hi, he, hy, by omega⟩
-
-/-- Actual queue calls modify only the two reserved array regions. -/
-theorem modifies {w base capacity : ℕ}
-    (hc : Fits w (base + 2 * capacity)) {q : List ℕ} {x y : Data 11} {o : QueueOp ℕ}
-    {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace}
-    (hr : QueueRep w base capacity q x) (hv : (spec w capacity).valid q o)
-    (he : (implementation w capacity).ExecOp w x o a y trace) :
-    Modifies (footprint base capacity) x.mem y.mem := by
-  obtain ⟨front, back, rfl, hr⟩ := hr
-  obtain ⟨z, hz, _, _, hf⟩ := execute hc hr o hv
-  exact (he.eq_of_exec hz).1 ▸ hf
-
-/-- Disjoint heap representations survive every queue call, including a full rear transfer. -/
-theorem frame {w base capacity : ℕ}
-    (hc : Fits w (base + 2 * capacity)) {q : List ℕ} {x y : Data 11} {o : QueueOp ℕ}
-    {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace}
-    (hr : QueueRep w base capacity q x) (hv : (spec w capacity).valid q o)
-    (he : (implementation w capacity).ExecOp w x o a y trace)
-    {Q : HeapAssertion} (hQ : Q.holds x.mem)
-    (hd : Disjoint Q.footprint (footprint base capacity)) : Q.holds y.mem :=
-  HeapAssertion.frame hQ hd (modifies hc hr hv he)
-
-end Cslib.DataStructure.Queue.WordRAM
diff --git a/Complexity/DataStructure/Queue/WordRAM/RegisterCorrectness.lean b/Complexity/DataStructure/Queue/WordRAM/RegisterCorrectness.lean
new file mode 100644
index 0000000000..914d9d6ad8
--- /dev/null
+++ b/Complexity/DataStructure/Queue/WordRAM/RegisterCorrectness.lean
@@ -0,0 +1,141 @@
+/-
+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.DataStructure.Queue.WordRAM.RegisterMethods
+
+/-!
+# FIFO correctness of the physical-array memory programs
+
+The count inputs and results are ordinary values; the physical memory assertions reuse
+`Block.HoldsList`. The conclusions identify the existing `pairStep` on the front and rear
+lists, including empty dequeue and a returned zero. No count cell or stronger room premise is
+introduced. The native register representation and paid dispatcher are separate consumers.
+
+## Main results
+
+* `enqueue_contents`: the rear write implements a logical stack push and frames the front.
+* `popFront_contents`: the top read implements a logical stack pop without clearing memory.
+* `dequeue_contents`: transfer and pop implement the existing FIFO transition `pairStep`.
+
+## References
+
+The queue and its algorithmic references are in `Cslib.DataStructure.Queue.Spec`.
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
+
+open Cslib.WordRAM Cslib.WordRAM.Realization
+
+/-- Enqueue appends one physical rear word while retaining the entire represented front. -/
+theorem enqueue_contents {d : Input} (front back : List ℕ) (s : Memory.State)
+    (hF : d 0 = front.length) (hB : d 1 = back.length)
+    (hc : front.length + back.length < d 3)
+    (hfront : Block.HoldsList (d 2) front.reverse s.mem)
+    (hback : Block.HoldsList (d 2 + d 3) back.reverse s.mem) :
+    let t := (Memory.spec 0).clientState s (enqueue d)
+    (Memory.spec 0).clientResult s (enqueue d) = (front.length, (d 4 :: back).length) ∧
+      Block.HoldsList (d 2) front.reverse t.mem ∧
+      Block.HoldsList (d 2 + d 3) (d 4 :: back).reverse t.mem := by
+  refine ⟨?_, ?_, ?_⟩
+  · change (d 0, d 1 + 1) = _
+    rw [hF, hB]
+    rfl
+  · change Block.HoldsList (d 2) front.reverse
+      (Function.update s.mem (d 2 + d 3 + d 1) (d 4))
+    apply hfront.frame
+    intro a ha hb
+    rw [Function.update_of_ne]
+    simp only [List.length_reverse] at hb
+    omega
+  · change Block.HoldsList (d 2 + d 3) (d 4 :: back).reverse
+      (Function.update s.mem (d 2 + d 3 + d 1) (d 4))
+    simpa only [hB, List.reverse_cons, List.length_reverse] using hback.append_one (d 4)
+
+/-- Pop observes the top represented value and retains the unused dirty cell. No memory
+clearing, capacity fit or nonzero-value hypothesis is needed for this source equation. -/
+theorem popFront_contents {d : Input} (front back : List ℕ) (s : Memory.State)
+    (hF : d 0 = front.length) (hB : d 1 = back.length)
+    (hfront : Block.HoldsList (d 2) front.reverse s.mem)
+    (hback : Block.HoldsList (d 2 + d 3) back.reverse s.mem) :
+    (Memory.spec 0).clientResult s (popFront d) =
+        ((front.tail.length, back.length), front.head?) ∧
+      Block.HoldsList (d 2) front.tail.reverse s.mem ∧
+      Block.HoldsList (d 2 + d 3) back.reverse s.mem := by
+  cases front with
+  | nil =>
+    refine ⟨?_, Block.holdsList_nil _ _, hback⟩
+    have hz : d 0 = 0 := hF
+    rw [clientResult_popFront, ite_eq_left hz, hF, hB]
+    rfl
+  | cons a front =>
+    have hn : d 0 ≠ 0 := by rw [hF]; exact Nat.succ_ne_zero _
+    have hlen : d 0 - 1 = front.length := by rw [hF]; rfl
+    have hp : Block.HoldsList (d 2) (front.reverse ++ [a]) s.mem := by
+      simpa only [List.reverse_cons] using hfront
+    have hv : s.mem (d 2 + front.length) = a := by
+      have hv : s.mem (d 2 + front.reverse.length) = a :=
+        (hp.get front.reverse.length (by simp)).trans (List.getElem_concat_length rfl _)
+      simpa only [List.length_reverse] using hv
+    refine ⟨?_, ?_, hback⟩
+    · rw [clientResult_popFront, ite_eq_right hn, hlen, hB, hv]
+      rfl
+    · simpa only [List.tail_cons, List.take_left] using
+        hp.take front.reverse.length
+
+/-- The interpreter's actual counts, option answer and physical arrays implement the
+existing two-stack transition. The only capacity premise is the original sum bound. -/
+theorem dequeue_contents {w : ℕ} {d : Input} (front back : List ℕ) (s : Memory.State)
+    (hw : Memory.WellFormed w s) (hF : d 0 = front.length) (hB : d 1 = back.length)
+    (hc : front.length + back.length ≤ d 3) (hf : d 2 + 2 * d 3 ≤ s.frontier)
+    (hfront : Block.HoldsList (d 2) front.reverse s.mem)
+    (hback : Block.HoldsList (d 2 + d 3) back.reverse s.mem) :
+    let p := pairStep (front, back) .dequeue
+    let t := (Memory.spec 0).clientState s (dequeue d)
+    (Memory.spec 0).clientResult s (dequeue d) = ((p.1.1.length, p.1.2.length), p.2) ∧
+      Block.HoldsList (d 2) p.1.1.reverse t.mem ∧
+      Block.HoldsList (d 2 + d 3) p.1.2.reverse t.mem := by
+  cases front with
+  | nil =>
+    have hz : d 0 = 0 := hF
+    have hdom : transferDomain w d s := by
+      exact ⟨by rw [hF, hB]; exact hc, hf⟩
+    have hi := transfer_invariant hw hdom
+    have hr : (Memory.spec 0).clientResult s (transfer d) = (back.length, 0) := by
+      simpa only [hF, hB, List.length_nil, Nat.zero_add] using hi.2.2.1
+    let t := (Memory.spec 0).clientState s (transfer d)
+    have ht : Block.HoldsList (d 2) back.reverse.reverse t.mem := by
+      simpa only [List.append_nil] using transfer_contents back [] s hF hB hc hfront hback
+    have hp := popFront_contents (d := ![back.length, 0, d 2, d 3, d 4])
+      back.reverse [] t (by simp) rfl ht (Block.holdsList_nil _ _)
+    have hs : (Memory.spec 0).clientState s (dequeue d) = t := by
+      rw [dequeue, ite_eq_left hz, StateTransitionSpec.clientState_bind, hr]
+      exact clientState_popFront _ _ _
+    refine ⟨?_, ?_, ?_⟩
+    · rw [dequeue, ite_eq_left hz, StateTransitionSpec.clientResult_bind, hr]
+      exact hp.1
+    · rw [hs]
+      exact hp.2.1
+    · rw [hs]
+      exact hp.2.2
+  | cons a front =>
+    have hn : d 0 ≠ 0 := by rw [hF]; exact Nat.succ_ne_zero _
+    have hp := popFront_contents (a :: front) back s hF hB hfront hback
+    have hs : (Memory.spec 0).clientState s (dequeue d) = s := by
+      rw [dequeue, ite_eq_right hn, clientState_popFront]
+    refine ⟨?_, ?_, ?_⟩
+    · rw [dequeue, ite_eq_right hn]
+      exact hp.1
+    · rw [hs]
+      exact hp.2.1
+    · rw [hs]
+      exact hp.2.2
+
+end Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
diff --git a/Complexity/DataStructure/Queue/WordRAM/RegisterDynamic.lean b/Complexity/DataStructure/Queue/WordRAM/RegisterDynamic.lean
new file mode 100644
index 0000000000..e798a9055d
--- /dev/null
+++ b/Complexity/DataStructure/Queue/WordRAM/RegisterDynamic.lean
@@ -0,0 +1,112 @@
+/-
+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.DataStructure.Queue.WordRAM.RegisterExecution
+
+/-!
+# Adaptive clients of the realized resident queue
+
+The existing dynamic certificate supplies correctness and the generic resource theorem
+telescopes the actual native instruction counts with the terminal rear potential. The operation
+program, register file and exchange factor precede widths, layouts, dirty memory and adaptive
+clients. Initialization is a literal base/capacity code family, fixed before width and entry data;
+its six instructions change no physical memory cell. The client controller and external
+tag/payload delivery keep the original calling boundary.
+
+## Main results
+
+* `amortized`, `run_client`, `run_initialized`: native adaptive execution and resource bounds.
+* `modifies`, `frame`: the original two-array footprint and disjoint heap assertions.
+
+## References
+
+The queue and its algorithmic references are in `Cslib.DataStructure.Queue.Spec`.
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.Queue.WordRAM
+
+open Cslib.WordRAM Cslib.WordRAM.Realization
+open RegisterMetadata
+
+/-- Both reserved arrays together contain exactly twice the capacity in cells. -/
+theorem footprint_card (base capacity : ℕ) : (footprint base capacity).card = 2 * capacity :=
+  Block.card_footprint _
+
+/-- The expensive native transfer consumes the scaled rear credit. Both branches include
+their control, count commits and final halt in this globally constant per-call charge. -/
+theorem amortized {w base capacity : ℕ} (h1 : Fits w 1) :
+    DataStructure.Amortized (certificate (base := base) (capacity := capacity) h1).impl
+      DynamicProgram.OperationTrace.instructions (fun _ x => potential x)
+      (fun _ _ => 4 * Backend.factor family + 6) :=
+  DataStructure.Amortized.ofFn fun hr hv he => by
+    obtain ⟨front, back, rfl, hr⟩ := hr
+    obtain ⟨z, n, hz, _, _, _, hp⟩ := execute h1 hr _ hv
+    obtain ⟨rfl, hn⟩ := he.eq_of_exec hz
+    rw [hn]
+    exact hp
+
+/-- Every admissible adaptive client has a correct native execution with terminal potential
+retained. This sums calls of the fixed program, without charging a host controller as RAM. -/
+theorem run_client {w base capacity : ℕ} (h1 : Fits w 1) {α : Type}
+    (p : (spec w capacity).Client α) {q : List ℕ} {x : Data registers}
+    (hr : QueueRep w base capacity q x)
+    (hv : (spec w capacity).ValidHistory q ((spec w capacity).runClient q p).2.2) :
+    ∃ y traces, DataStructure.Executes ((implementation w capacity).ExecOp w) p x
+        ((spec w capacity).runClient q p).1 y traces ∧
+      QueueRep w base capacity ((spec w capacity).runClient q p).2.1 y ∧
+      DataStructure.total DynamicProgram.OperationTrace.instructions traces + potential y ≤
+        ((spec w capacity).runClient q p).2.2.length * (4 * Backend.factor family + 6) +
+          potential x :=
+  (amortized h1).exists_executes_const p hr hv
+
+/-- Starting from arbitrary bounded dirty data, the actual six initializer instructions
+establish zero rear credit. The physical end-fit domain is exactly the original `base+2*C`.
+No clearing, installed frontier or zero-memory premise is needed. -/
+theorem run_initialized {w base capacity : ℕ} (h1 : Fits w 1)
+    (hc : Fits w (base + 2 * capacity)) {α : Type} (p : (spec w capacity).Client α)
+    {x : Data registers} (hx : x.Bounded w)
+    (hv : (spec w capacity).ValidHistory [] ((spec w capacity).runClient [] p).2.2) :
+    ∃ ready y traces, Exec w (initializeCode base capacity) x ready 6 ∧
+      DataStructure.Executes ((implementation w capacity).ExecOp w) p ready
+        ((spec w capacity).runClient [] p).1 y traces ∧
+      QueueRep w base capacity ((spec w capacity).runClient [] p).2.1 y ∧
+      6 + DataStructure.total DynamicProgram.OperationTrace.instructions traces + potential y ≤
+        6 + ((spec w capacity).runClient [] p).2.2.length * (4 * Backend.factor family + 6) := by
+  have hr := initialized_rep hx hc
+  have hp : potential (initialized base capacity x) = 0 := by
+    simp only [potential, hr.backLen_eq, List.length_nil, Nat.mul_zero]
+  obtain ⟨y, traces, he, hy, hb⟩ := run_client (q := []) h1 p ⟨[], [], rfl, hr⟩ hv
+  exact ⟨initialized base capacity x, y, traces, (initialize_exec hx hc).1,
+    he, hy, by omega⟩
+
+/-- Actual native queue calls modify only the original two reserved array regions. -/
+theorem modifies {w base capacity : ℕ} (h1 : Fits w 1)
+    {q : List ℕ} {x y : Data registers} {o : Queue.QueueOp ℕ}
+    {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace}
+    (hr : QueueRep w base capacity q x) (hv : (spec w capacity).valid q o)
+    (he : (implementation w capacity).ExecOp w x o a y trace) :
+    Modifies (footprint base capacity) x.mem y.mem := by
+  obtain ⟨front, back, rfl, hr⟩ := hr
+  obtain ⟨z, n, hz, _, _, hf, _⟩ := execute h1 hr o hv
+  exact (he.eq_of_exec hz).1 ▸ hf
+
+/-- Disjoint heap assertions survive every call, including the native reversal. This is
+the original physical-memory frame, not a claim about another structure's frontier invariant. -/
+theorem frame {w base capacity : ℕ} (h1 : Fits w 1)
+    {q : List ℕ} {x y : Data registers} {o : Queue.QueueOp ℕ}
+    {a : (spec w capacity).Result o} {trace : DynamicProgram.OperationTrace}
+    (hr : QueueRep w base capacity q x) (hv : (spec w capacity).valid q o)
+    (he : (implementation w capacity).ExecOp w x o a y trace)
+    {Q : HeapAssertion} (hQ : Q.holds x.mem)
+    (hd : Disjoint Q.footprint (footprint base capacity)) : Q.holds y.mem :=
+  HeapAssertion.frame hQ hd (modifies h1 hr hv he)
+
+end Cslib.DataStructure.Queue.WordRAM
diff --git a/Complexity/DataStructure/Queue/WordRAM/RegisterExecution.lean b/Complexity/DataStructure/Queue/WordRAM/RegisterExecution.lean
new file mode 100644
index 0000000000..f2d4159b46
--- /dev/null
+++ b/Complexity/DataStructure/Queue/WordRAM/RegisterExecution.lean
@@ -0,0 +1,448 @@
+/-
+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.DataStructure.Queue.WordRAM.RegisterProgram
+
+/-!
+# Paid initialization and execution of the resident queue
+
+The proof uses the shared Backend's public packing and live-execution facts. In particular,
+the maintained count words are already present in native source registers, rather than being
+reinstalled by the external controller. Operation code and packing are the globally fixed family
+from `RegisterProgram`; the initializer remains parameterized by literal base and capacity.
+
+## Main results
+
+* `initialized_rep`: the six register writes establish the empty two-array representation.
+* `initialize_queue`: arbitrary dirty bounded data admits paid constant-time initialization.
+* `execute_enqueue`, `execute_dequeue`: the same native dispatcher implements both methods.
+* `execute`, `certificate`: scaled native payment and the existing dynamic certificate.
+
+## References
+
+The queue and its algorithmic references are in `Cslib.DataStructure.Queue.Spec`.
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.Queue.WordRAM
+
+open Cslib.WordRAM Cslib.WordRAM.Realization
+open RegisterMetadata
+
+private theorem src_injective : Function.Injective src := Backend.src_injective family false
+
+private theorem result_injective : Function.Injective result := by
+  intro i j h
+  have he := Backend.tmp_injective family true h
+  have hv := congrArg Fin.val he
+  exact Fin.ext hv
+
+private theorem src_ne_result (i : Fin 5) (j : Fin 4) : src i ≠ result j :=
+  Backend.src_ne_tmp family false true i _
+
+private theorem src_ne_frontier (i : Fin 5) : src i ≠ Backend.frontier family :=
+  Backend.src_ne_frontier family false i
+
+private theorem result_ne_frontier (i : Fin 4) : result i ≠ Backend.frontier family :=
+  Backend.tmp_ne_frontier family true _
+
+private theorem tag_ne_zero : tag ≠ zero := by
+  intro h
+  have hv := congrArg Fin.val (result_injective h)
+  change (0 : ℕ) = 1 at hv
+  omega
+
+private theorem prepare_frame (w capacity : ℕ) (o : Queue.QueueOp ℕ) (x : Data registers)
+    (i : Fin registers) (ht : i ≠ tag) (ha : i ≠ src 4) :
+    ((implementation w capacity).prepare o x).regs i = x.regs i := by
+  apply DynamicProgram.prepare_regs_of_not_input
+  simp [implementation, ht, ha]
+
+private theorem prepare_src (w capacity : ℕ) (o : Queue.QueueOp ℕ) (x : Data registers)
+    (i : Fin 5) :
+    ((implementation w capacity).prepare o x).regs (src i) =
+      if i = 4 then (match o with | .enqueue v => v | .dequeue => 0) else x.regs (src i) := by
+  have ht : src i ≠ tag := src_ne_result i 0
+  have hs : src i = src 4 ↔ i = 4 := src_injective.eq_iff
+  cases o <;> simp [DynamicProgram.prepare, implementation, ht, hs]
+
+private theorem prepare_tag (w capacity : ℕ) (o : Queue.QueueOp ℕ) (x : Data registers) :
+    ((implementation w capacity).prepare o x).regs tag =
+      match o with | .enqueue _ => 0 | .dequeue => 1 := by
+  cases o <;> simp [DynamicProgram.prepare, implementation]
+
+private theorem prepare_frontier (w capacity : ℕ) (o : Queue.QueueOp ℕ)
+    (x : Data registers) :
+    ((implementation w capacity).prepare o x).regs (Backend.frontier family) =
+      x.regs (Backend.frontier family) :=
+  prepare_frame _ _ _ _ _ (result_ne_frontier 0).symm (src_ne_frontier 4).symm
+
+private theorem encoded_fits {w capacity : ℕ} (h1 : Fits w 1) (o : Queue.QueueOp ℕ)
+    (hv : match o with | .enqueue v => Fits w v | .dequeue => True)
+    (i : Fin registers) : Fits w ((implementation w capacity).encode o i) := by
+  cases o <;> dsimp only [implementation] <;> split
+  · exact fits_zero w
+  · exact hv
+  · exact h1
+  · exact fits_zero w
+
+private theorem prepare_bounded {w capacity : ℕ} (o : Queue.QueueOp ℕ)
+    {x : Data registers} (hx : x.Bounded w) (h1 : Fits w 1)
+    (hv : match o with | .enqueue v => Fits w v | .dequeue => True) :
+    ((implementation w capacity).prepare o x).Bounded w :=
+  DynamicProgram.prepare_bounded _ hx (fun i _ => encoded_fits h1 o hv i)
+
+private noncomputable def staged (w capacity : ℕ) (o : Queue.QueueOp ℕ)
+    (x : Data registers) : Data registers :=
+  ((implementation w capacity).prepare o x).set zero 0
+
+private theorem stage_exec (w capacity : ℕ) (o : Queue.QueueOp ℕ) (x : Data registers) :
+    Exec (B := .standard) w (.op (.const zero 0)) ((implementation w capacity).prepare o x)
+      (staged w capacity o x) 1 := Exec.const (fits_zero w)
+
+private theorem staged_bounded {w capacity : ℕ} (o : Queue.QueueOp ℕ)
+    {x : Data registers} (hx : x.Bounded w) (h1 : Fits w 1)
+    (hv : match o with | .enqueue v => Fits w v | .dequeue => True) :
+    (staged w capacity o x).Bounded w :=
+  (stage_exec w capacity o x).bounded (prepare_bounded o hx h1 hv)
+
+private theorem staged_input {w base capacity : ℕ} {front back : List ℕ} {x : Data registers}
+    (hr : Rep w base capacity front back x) (o : Queue.QueueOp ℕ) :
+    (staged w capacity o x).regs ∘ src =
+      ![front.length, back.length, base, capacity,
+        match o with | .enqueue v => v | .dequeue => 0] := by
+  funext i
+  change Function.update _ zero 0 (src i) = _
+  rw [Function.update_of_ne (src_ne_result i 1), prepare_src]
+  fin_cases i <;> simp [hr.frontLen_eq, hr.backLen_eq, hr.base_eq, hr.capacity_eq]
+
+private theorem staged_memory (w capacity : ℕ) (o : Queue.QueueOp ℕ) (x : Data registers) :
+    memoryState (Backend.frontier family) (staged w capacity o x) =
+      memoryState (Backend.frontier family) x := by
+  refine Memory.State.ext ?_ ?_
+  · change ((implementation w capacity).prepare o x).mem = x.mem
+    exact DynamicProgram.prepare_mem _ _ _
+  · change Function.update _ zero 0 (Backend.frontier family) = _
+    rw [Function.update_of_ne (result_ne_frontier 1).symm]
+    exact prepare_frontier _ _ _ _
+
+private theorem staged_tag (w capacity : ℕ) (o : Queue.QueueOp ℕ) (x : Data registers) :
+    (staged w capacity o x).regs tag =
+      match o with | .enqueue _ => 0 | .dequeue => 1 := by
+  change Function.update _ zero 0 tag = _
+  rw [Function.update_of_ne tag_ne_zero]
+  exact prepare_tag _ _ _ _
+
+private noncomputable def committed (m : ℕ × ℕ) (x : Data registers) : Data registers :=
+  (x.set (src 0) m.1).set (src 1) m.2
+
+private theorem commit_exec {w : ℕ} {x : Data registers} {m : ℕ × ℕ}
+    (h0 : x.regs (result 0) = m.1) (h1 : x.regs (result 1) = m.2) :
+    Exec w commit x (committed m x) 2 := by
+  have h0' : Exec (B := .standard) w (.op (.copy (src 0) (result 0))) x
+      (x.set (src 0) m.1) 1 := by
+    simpa only [h0] using (Exec.copy (B := .standard) (w := w)
+      (x := x) (d := src 0) (s := result 0))
+  have hr : (x.set (src 0) m.1).regs (result 1) = m.2 := by
+    simpa only [Data.set_regs, Function.update_of_ne (src_ne_result 0 1).symm] using h1
+  exact h0'.seq (by
+    simpa only [hr] using (Exec.copy (B := .standard) (w := w)
+      (x := x.set (src 0) m.1) (d := src 1) (s := result 1)))
+
+private theorem committed_other (m : ℕ × ℕ) (x : Data registers) (i : Fin registers)
+    (h0 : i ≠ src 0) (h1 : i ≠ src 1) : (committed m x).regs i = x.regs i := by
+  simp only [committed, Data.set_regs, Function.update_of_ne h1, Function.update_of_ne h0]
+
+private theorem committed_counts (m : ℕ × ℕ) (x : Data registers) :
+    (committed m x).regs (src 0) = m.1 ∧ (committed m x).regs (src 1) = m.2 := by
+  have hn : src 0 ≠ src 1 := src_injective.ne (by decide)
+  simp [committed, Data.set, hn]
+
+private theorem enqueue_result_eq (i : Fin 2) :
+    Backend.tmp family false (Fin.castAdd ((family false).realizes.scratchSize + 1) i) =
+      result (Fin.castAdd 2 i) := Backend.tmp_eq_of_val_eq family false true rfl
+
+private theorem initialized_input (base capacity : ℕ) (x : Data registers) :
+    (initialized base capacity x).regs ∘ src = ![0, 0, base, capacity, x.regs (src 4)] := by
+  have hz (i : Fin 5) : src i ≠ zero := src_ne_result i 1
+  have hf (i : Fin 5) : src i ≠ Backend.frontier family := src_ne_frontier i
+  have hs (i j : Fin 5) : src i = src j ↔ i = j := src_injective.eq_iff
+  funext i
+  fin_cases i <;> simp [initialized, Data.set, hz, hf, hs]
+
+private theorem initialized_frontier (base capacity : ℕ) (x : Data registers) :
+    (initialized base capacity x).regs (Backend.frontier family) = base + 2 * capacity := by
+  have hz : Backend.frontier family ≠ zero := (result_ne_frontier 1).symm
+  have hs (i : Fin 5) : Backend.frontier family ≠ src i := (src_ne_frontier i).symm
+  simp [initialized, Data.set, hz, hs]
+
+/-- The actual six writes establish the empty representation under precisely the original
+end-fit condition, with no assumption on initial registers or dirty memory. -/
+theorem initialized_rep {w base capacity : ℕ} {x : Data registers} (hx : x.Bounded w)
+    (hc : Fits w (base + 2 * capacity)) : Rep w base capacity [] []
+      (initialized base capacity x) := by
+  have hin := initialized_input base capacity x
+  exact ⟨(initialize_exec hx hc).2.1, congrFun hin 2, congrFun hin 3,
+    initialized_frontier base capacity x, congrFun hin 0, congrFun hin 1,
+    Nat.zero_le _, Block.holdsList_nil _ _, Block.holdsList_nil _ _⟩
+
+/-- Paid raw initialization establishes the existing FIFO meaning and preserves all memory.
+The original small-width and capacity-zero cases are included; tag delivery later retains its
+separate `Fits w 1` requirement. -/
+theorem initialize_queue {w base capacity : ℕ} {x : Data registers} (hx : x.Bounded w)
+    (hc : Fits w (base + 2 * capacity)) :
+    ∃ ready, Exec w (initializeCode base capacity) x ready 6 ∧
+      QueueRep w base capacity [] ready ∧ ready.mem = x.mem := by
+  exact ⟨initialized base capacity x, (initialize_exec hx hc).1,
+    ⟨[], [], rfl, initialized_rep hx hc⟩, rfl⟩
+
+/-- The fixed dispatcher executes enqueue from resident metadata, pays the zero test and
+two count copies, and includes the final call halt in its bound. The original two arrays are
+the complete memory footprint. -/
+theorem execute_enqueue {w base capacity v : ℕ} {front back : List ℕ} {x : Data registers}
+    (h1 : Fits w 1) (hr : Rep w base capacity front back x)
+    (hs : front.length + back.length < capacity) (hv : Fits w v) :
+    ∃ y n, Exec w program ((implementation w capacity).prepare (.enqueue v) x) y n ∧
+      n + 1 ≤ 2 * Backend.factor family + 5 ∧ Rep w base capacity front (v :: back) y ∧
+      Modifies (footprint base capacity) x.mem y.mem := by
+  let d : Input := ![front.length, back.length, base, capacity, v]
+  let z := staged w capacity (.enqueue v) x
+  have hdom : enqueueDomain w d (memoryState (Backend.frontier family) x) := by
+    change front.length + back.length < capacity ∧
+      base + 2 * capacity ≤ x.regs (Backend.frontier family) ∧ Fits w v
+    exact ⟨hs, hr.frontier_eq.ge, hv⟩
+  have hz : z.Bounded w := staged_bounded (.enqueue v) hr.bounded h1 hv
+  have hin : z.regs ∘ Backend.src family false = (family false).input d :=
+    staged_input hr (.enqueue v)
+  have hdomz : enqueueDomain w d (memoryState (Backend.frontier family) z) := by
+    rw [staged_memory]
+    exact hdom
+  obtain ⟨b, n, hb, hn, hm, ho, hbb, hframe⟩ := Backend.exists_exec_live family false d hz hin
+    hdomz (valid_enqueue hdomz)
+  rw [staged_memory] at hm
+  have hn' : n ≤ 2 * Backend.factor family := by
+    change n ≤ Backend.factor family * (memoryCost (enqueue d)
+      (memoryState (Backend.frontier family) z) + 0 + 1) at hn
+    simpa only [memoryCost_enqueue, Nat.add_zero, Nat.mul_comm] using hn
+  have h0 : b.regs (result 0) = front.length :=
+    (congrArg b.regs (enqueue_result_eq 0)).symm.trans (ho 0)
+  have hB : b.regs (result 1) = back.length + 1 :=
+    (congrArg b.regs (enqueue_result_eq 1)).symm.trans (ho 1)
+  let m := (front.length, back.length + 1)
+  have hcommit : Exec w commit b (committed m b) 2 := commit_exec h0 hB
+  have hcond : (Cond.eq tag zero).Holds z := by
+    change z.regs tag = z.regs zero
+    have hz0 : z.regs zero = 0 := by
+      simp only [z, staged, Data.set_regs, Function.update_self]
+    rw [hz0]
+    exact staged_tag w capacity (.enqueue v) x
+  have he : Exec w program ((implementation w capacity).prepare (.enqueue v) x)
+      (committed m b) (1 + (n + 1 + 2)) :=
+    (stage_exec w capacity (.enqueue v) x).seq ((Exec.branch_pos hcond hb).seq hcommit)
+  have hsrc (i : Fin 5) : b.regs (src i) = d i := by
+    rw [hframe _ (src_ne_frontier i) (fun a => (Backend.src_ne_tmp family false false i a).symm)]
+    exact congrFun hin i
+  have hfrontier : b.regs (Backend.frontier family) = x.regs (Backend.frontier family) :=
+    congrArg Memory.State.frontier hm
+  have hmemw : (committed m b).mem =
+      ((Memory.spec w).clientState (memoryState (Backend.frontier family) x) (enqueue d)).mem :=
+    congrArg Memory.State.mem hm
+  have hmem : (committed m b).mem =
+      ((Memory.spec 0).clientState (memoryState (Backend.frontier family) x) (enqueue d)).mem := by
+    simpa only [clientState_width w] using hmemw
+  have hcontents := enqueue_contents (d := d) front back
+    (memoryState (Backend.frontier family) x) rfl rfl hs hr.front_contents hr.back_contents
+  refine ⟨committed m b, 1 + (n + 1 + 2), he, by omega, ?_, ?_⟩
+  · refine ⟨hcommit.bounded hbb, ?_, ?_, ?_, (committed_counts m b).1,
+      (committed_counts m b).2, ?_, ?_, ?_⟩
+    · rw [committed_other m b (src 2) (src_injective.ne (by decide))
+        (src_injective.ne (by decide)), hsrc]
+      rfl
+    · rw [committed_other m b (src 3) (src_injective.ne (by decide))
+        (src_injective.ne (by decide)), hsrc]
+      rfl
+    · rw [committed_other m b _ (src_ne_frontier 0).symm (src_ne_frontier 1).symm,
+        hfrontier, hr.frontier_eq]
+    · simp only [List.length_cons]
+      omega
+    · rw [hmem]
+      exact hcontents.2.1
+    · rw [hmem]
+      exact hcontents.2.2
+  · rw [hmemw]
+    exact enqueue_modifies hdom
+
+/-- The negative native branch performs the source transfer/pop, commits both returned
+counts, and decodes its faithful option result. The bound includes the negative branch's
+two instructions and the call halt, without charging any hidden metadata installation. -/
+theorem execute_dequeue {w base capacity : ℕ} {front back : List ℕ} {x : Data registers}
+    (h1 : Fits w 1) (hr : Rep w base capacity front back x) :
+    let p := pairStep (front, back) .dequeue
+    ∃ y n, Exec w program ((implementation w capacity).prepare .dequeue x) y n ∧
+      n + 1 ≤ Backend.factor family *
+        (memoryCost (dequeue ![front.length, back.length, base, capacity, 0])
+          (memoryState (Backend.frontier family) x) + 1) + 6 ∧
+      Rep w base capacity p.1.1 p.1.2 y ∧
+      (implementation w capacity).decode .dequeue y.regs = some p.2 ∧
+      Modifies (footprint base capacity) x.mem y.mem := by
+  let d : Input := ![front.length, back.length, base, capacity, 0]
+  let p := pairStep (front, back) .dequeue
+  let z := staged w capacity .dequeue x
+  have hdom : transferDomain w d (memoryState (Backend.frontier family) x) := by
+    change front.length + back.length ≤ capacity ∧
+      base + 2 * capacity ≤ x.regs (Backend.frontier family)
+    exact ⟨hr.size_le, hr.frontier_eq.ge⟩
+  have hw : Memory.WellFormed w (memoryState (Backend.frontier family) x) :=
+    wellFormed_memoryState hr.bounded
+  have hi := dequeue_invariant hw hdom
+  have hcontents := dequeue_contents (d := d) front back
+    (memoryState (Backend.frontier family) x) hw rfl rfl hr.size_le hr.frontier_eq.ge
+    hr.front_contents hr.back_contents
+  have hz : z.Bounded w := staged_bounded .dequeue hr.bounded h1 trivial
+  have hin : z.regs ∘ Backend.src family true = (family true).input d := by
+    funext i
+    change z.regs (Backend.src family true i) = d i
+    rw [Backend.src_eq_of_val_eq family true false (a := i) (b := i) rfl]
+    exact congrFun (staged_input hr .dequeue) i
+  have hdomz : transferDomain w d (memoryState (Backend.frontier family) z) := by
+    rw [staged_memory]
+    exact hdom
+  obtain ⟨b, n, hb, hn, hm, ho, hbb, hframe⟩ := Backend.exists_exec_live family true d hz hin
+    hdomz (by rw [staged_memory]; exact hi.1)
+  rw [staged_memory] at hm hn ho
+  rw [clientResult_width w, hcontents.1] at ho
+  have hn' : n ≤ Backend.factor family *
+      (memoryCost (dequeue d) (memoryState (Backend.frontier family) x) + 1) := by
+    simpa only [Nat.add_zero] using hn
+  let m := (p.1.1.length, p.1.2.length)
+  have h0 : b.regs (result 0) = m.1 := ho 0
+  have hB : b.regs (result 1) = m.2 := ho 1
+  have hcommit : Exec w commit b (committed m b) 2 := commit_exec h0 hB
+  have hcond : ¬(Cond.eq tag zero).Holds z := by
+    change ¬z.regs tag = z.regs zero
+    have ht : z.regs tag = 1 := staged_tag w capacity .dequeue x
+    have hz0 : z.regs zero = 0 := by
+      simp only [z, staged, Data.set_regs, Function.update_self]
+    rw [ht, hz0]
+    decide
+  have he : Exec w program ((implementation w capacity).prepare .dequeue x)
+      (committed m b) (1 + (n + 2 + 2)) :=
+    (stage_exec w capacity .dequeue x).seq ((Exec.branch_neg hcond hb).seq hcommit)
+  have hsrc (i : Fin 5) : b.regs (src i) = d i := by
+    rw [hframe _ (src_ne_frontier i) (fun a => (Backend.src_ne_tmp family false true i a).symm)]
+    exact congrFun (staged_input hr .dequeue) i
+  have hfrontier : b.regs (Backend.frontier family) = x.regs (Backend.frontier family) := by
+    have hf := congrArg Memory.State.frontier hm
+    rw [clientState_width w] at hf
+    exact hf.trans hi.2.2.2.1
+  have hmem : (committed m b).mem =
+      ((Memory.spec 0).clientState (memoryState (Backend.frontier family) x) (dequeue d)).mem := by
+    have hmemw : (committed m b).mem =
+        ((Memory.spec w).clientState (memoryState (Backend.frontier family) x) (dequeue d)).mem :=
+      congrArg Memory.State.mem hm
+    rw [clientState_width w] at hmemw
+    exact hmemw
+  have hclock : 1 + (n + 2 + 2) + 1 ≤ Backend.factor family *
+      (memoryCost (dequeue d) (memoryState (Backend.frontier family) x) + 1) + 6 := by omega
+  refine ⟨committed m b, 1 + (n + 2 + 2), he, hclock, ?_, ?_, ?_⟩
+  · refine ⟨hcommit.bounded hbb, ?_, ?_, ?_, (committed_counts m b).1,
+      (committed_counts m b).2, ?_, ?_, ?_⟩
+    · rw [committed_other m b (src 2) (src_injective.ne (by decide))
+        (src_injective.ne (by decide)), hsrc]
+      rfl
+    · rw [committed_other m b (src 3) (src_injective.ne (by decide))
+        (src_injective.ne (by decide)), hsrc]
+      rfl
+    · rw [committed_other m b _ (src_ne_frontier 0).symm (src_ne_frontier 1).symm,
+        hfrontier, hr.frontier_eq]
+    · have hs := pairStep_length_le (w := w) (capacity := capacity) (s := (front, back))
+        (by simpa only [contents_length] using hr.size_le) .dequeue trivial
+      simpa only [contents_length] using hs
+    · rw [hmem]
+      exact hcontents.2.1
+    · rw [hmem]
+      exact hcontents.2.2
+  · have ht : (committed m b).regs (result 2) = optionWords p.2 0 := by
+      rw [committed_other m b _ (src_ne_result 0 2).symm (src_ne_result 1 2).symm]
+      exact ho 2
+    have hv : (committed m b).regs (result 3) = optionWords p.2 1 := by
+      rw [committed_other m b _ (src_ne_result 0 3).symm (src_ne_result 1 3).symm]
+      exact ho 3
+    change some (if (committed m b).regs (result 2) = 0 then none
+      else some ((committed m b).regs (result 3))) = some p.2
+    rw [ht, hv]
+    cases p.2 <;> rfl
+  · rw [hmem]
+    exact hi.2.2.2.2.2
+
+/-- One admissible call of the fixed native queue. The terminal rear potential is retained;
+the globally chosen exchange factor, control, metadata copies and halt are all charged.
+The external controller and tag/payload delivery remain the original dynamic-call boundary. -/
+theorem execute {w base capacity : ℕ} {front back : List ℕ} {x : Data registers}
+    (h1 : Fits w 1) (hr : Rep w base capacity front back x) (o : Queue.QueueOp ℕ)
+    (hv : (spec w capacity).valid (contents (front, back)) o) :
+    let p := pairStep (front, back) o
+    ∃ y n, Exec w program ((implementation w capacity).prepare o x) y n ∧
+      (implementation w capacity).decode o y.regs = some p.2 ∧
+      Rep w base capacity p.1.1 p.1.2 y ∧
+      Modifies (footprint base capacity) x.mem y.mem ∧
+      n + 1 + potential y ≤ 4 * Backend.factor family + 6 + potential x := by
+  cases o with
+  | enqueue v =>
+    change (contents (front, back)).length < capacity ∧ Fits w v at hv
+    rw [contents_length] at hv
+    obtain ⟨y, n, he, hn, hry, hm⟩ := execute_enqueue h1 hr hv.1 hv.2
+    refine ⟨y, n, he, rfl, hry, hm, ?_⟩
+    simp only [potential, hry.backLen_eq, hr.backLen_eq, List.length_cons,
+      Nat.mul_add, Nat.mul_one]
+    omega
+  | dequeue =>
+    obtain ⟨y, n, he, hn, hry, ha, hm⟩ := execute_dequeue h1 hr
+    let d : Input := ![front.length, back.length, base, capacity, 0]
+    have hw : Memory.WellFormed w (memoryState (Backend.frontier family) x) :=
+      wellFormed_memoryState hr.bounded
+    have hdom : transferDomain w d (memoryState (Backend.frontier family) x) :=
+      ⟨hr.size_le, hr.frontier_eq.ge⟩
+    have hcontents := dequeue_contents (d := d) front back
+      (memoryState (Backend.frontier family) x) hw rfl rfl hr.size_le hr.frontier_eq.ge
+      hr.front_contents hr.back_contents
+    have hpay := dequeue_memory_amortized hw hdom
+    rw [hcontents.1] at hpay
+    change memoryCost (dequeue d) (memoryState (Backend.frontier family) x) +
+      2 * (pairStep (front, back) .dequeue).1.2.length ≤ 3 + 2 * back.length at hpay
+    change n + 1 ≤ Backend.factor family *
+      (memoryCost (dequeue d) (memoryState (Backend.frontier family) x) + 1) + 6 at hn
+    refine ⟨y, n, he, ha, hry, hm, ?_⟩
+    simp only [potential, hry.backLen_eq, hr.backLen_eq]
+    nlinarith [Nat.mul_le_mul_left (Backend.factor family) hpay]
+
+/-- The fixed realized dispatcher implements the original bounded FIFO specification via
+the existing dynamic certificate. Its representation retains resident count words; no
+memory-only Backend implementation is asserted. The bounded resident frontier equals the physical
+end, so its fit already follows from `Rep`; raw initialization keeps its explicit end-fit
+premise. -/
+noncomputable def certificate {w base capacity : ℕ} (h1 : Fits w 1) :
+    DynamicCertificate (implementation w capacity) w :=
+  DynamicCertificate.ofFn
+    (rep := QueueRep w base capacity)
+    (bounded := fun h => by obtain ⟨_, _, _, hr⟩ := h; exact hr.bounded)
+    (arguments_fit := fun o hv i _ => by
+      exact encoded_fits h1 o (by
+        cases o with
+        | enqueue v => exact hv.2
+        | dequeue => trivial) i)
+    (execute := fun o hr hv => by
+      obtain ⟨front, back, rfl, hr⟩ := hr
+      obtain ⟨y, n, he, ha, hy, _, _⟩ := execute h1 hr o hv
+      have hs := pairStep_correct (front, back) o
+      exact ⟨y, n, he, ha.trans (congrArg some (congrArg Prod.snd hs)),
+        ⟨_, _, (congrArg Prod.fst hs).symm, hy⟩⟩)
+
+end Cslib.DataStructure.Queue.WordRAM
diff --git a/Complexity/DataStructure/Queue/WordRAM/RegisterMetadata.lean b/Complexity/DataStructure/Queue/WordRAM/RegisterMetadata.lean
new file mode 100644
index 0000000000..4060cd91a7
--- /dev/null
+++ b/Complexity/DataStructure/Queue/WordRAM/RegisterMetadata.lean
@@ -0,0 +1,95 @@
+/-
+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
+public import Complexity.DataStructure.Queue.WordRAM.Model
+import Complexity.Tactic.Realize
+
+/-!
+# A physical transfer step with explicit queue count words
+
+The input words are front count, rear count, base, capacity and payload. The source step reads
+one rear-array cell, writes the next front cell, and returns updated counts as values. No count
+is stored in physical memory. The shared realization judgment certifies every native arithmetic
+and staging instruction while retaining literal whole-memory semantics.
+
+## Main definitions
+
+* `Input`, `counts`: five input words and two faithfully encoded returned counts.
+* `move`, `domain`: one physical step and the original two-array capacity/room domain.
+
+## Main results
+
+* `realizes_move`: one uniform emitter before runtime values and register layouts.
+* `runClient_move`, `valid_move`, `move_modifies`: exact history, validity and physical frame.
+
+## References
+
+The queue and its algorithmic references are in `Cslib.DataStructure.Queue.Spec`.
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
+
+open Cslib.WordRAM Cslib.WordRAM.Realization
+
+/-- Five live input words: front count, rear count, base, capacity, reserved payload. -/
+abbrev Input := Fin 5 → ℕ
+
+/-- One exact source transfer step; the counts are values, not cells. -/
+def move (d : Input) : Memory.Prog (ℕ × ℕ) := do
+  let v ← Memory.read (d 2 + d 3 + (d 1 - 1))
+  Memory.write (d 2 + d 0) v
+  pure (d 0 + 1, d 1 - 1)
+
+/-- The old capacity and allocation envelope, without extra count cells or zero memory. -/
+def domain (_w : ℕ) (d : Input) (s : Memory.State) : Prop :=
+  0 < d 1 ∧ d 0 + d 1 ≤ d 3 ∧ d 2 + 2 * d 3 ≤ s.frontier
+
+/-- The two returned count words. -/
+def counts : ℕ × ℕ ↪ (Fin 2 → ℕ) :=
+  appendWords (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+    (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+
+/-- One emitter precedes every count, layout, width and initial memory. All native arithmetic
+and vector staging are charged by the memory-query budget; the body performs two queries. -/
+theorem realizes_move : Realizes .exact move (.refl Input) counts
+    domain (fun _ _ => 0) := by
+  change Realizes .exact move (.refl (Fin 5 → ℕ)) counts _ _
+  realize
+  · exact h.1
+  · exact hmem.fits_of_lt_frontier (by rcases h with ⟨hb, hc, hf⟩; omega)
+  · exact hmem.fits_of_lt_frontier (by rcases h with ⟨hb, hc, hf⟩; omega)
+  · exact (show Fits w (d 3) from hwords 3).of_le (by rcases h with ⟨hb, hc, hf⟩; omega)
+
+/-- The exact source history, including the physical read and write. -/
+theorem runClient_move (w : ℕ) (d : Input) (s : Memory.State) :
+    (Memory.spec w).runClient s (move d) =
+      ((d 0 + 1, d 1 - 1),
+        ⟨Function.update s.mem (d 2 + d 0) (s.mem (d 2 + d 3 + (d 1 - 1))), s.frontier⟩,
+        [.read (d 2 + d 3 + (d 1 - 1)),
+          .write (d 2 + d 0) (s.mem (d 2 + d 3 + (d 1 - 1)))]) := rfl
+
+/-- Every access is within the original two arrays, including the written value's fit. -/
+theorem valid_move {w : ℕ} {d : Input} {s : Memory.State}
+    (hw : Memory.WellFormed w s) (h : domain w d s) :
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (move d)) := by
+  change (d 2 + d 3 + (d 1 - 1) < s.frontier) ∧
+    (d 2 + d 0 < s.frontier ∧ Fits w (s.mem (d 2 + d 3 + (d 1 - 1)))) ∧ True
+  exact ⟨by rcases h with ⟨hb, hc, hf⟩; omega,
+    ⟨by rcases h with ⟨hb, hc, hf⟩; omega, hw.mem_fits _⟩, trivial⟩
+
+/-- The literal physical-memory frame remains the old `2*C` block. -/
+theorem move_modifies {w : ℕ} {d : Input} {s : Memory.State} (h : domain w d s) :
+    Modifies (Block.mk (d 2) (2 * d 3)).footprint s.mem
+      ((Memory.spec w).clientState s (move d)).mem := by
+  exact Modifies.write_of_owns ⟨by omega, by rcases h with ⟨hb, hc, hf⟩; omega⟩ _
+
+end Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
diff --git a/Complexity/DataStructure/Queue/WordRAM/RegisterMethods.lean b/Complexity/DataStructure/Queue/WordRAM/RegisterMethods.lean
new file mode 100644
index 0000000000..ff57b2d130
--- /dev/null
+++ b/Complexity/DataStructure/Queue/WordRAM/RegisterMethods.lean
@@ -0,0 +1,289 @@
+/-
+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.DataStructure.Queue.WordRAM.RegisterTransfer
+import Complexity.Tactic.Realize
+
+/-!
+# Queue methods with resident register metadata
+
+Both methods consume the same five live words: the two stack counts, base, capacity and the
+delivered payload. Their returned vectors begin with the two updated counts. Enqueue has no
+logical answer word; dequeue appends the faithful option encoding, including a distinct tag for
+`some 0`. The memory programs write only the original two physical arrays.
+
+## Main definitions
+
+* `enqueue`, `popFront`, `dequeue`: memory programs with explicit count inputs and results.
+* `enqueueDomain`: spare capacity, physical room and a word-sized delivered value.
+
+## Main results
+
+* `realizes_enqueue`, `realizes_popFront`, `realizes_dequeue`: uniform native method bodies.
+
+## References
+
+The queue and its algorithmic references are in `Cslib.DataStructure.Queue.Spec`.
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
+
+open Cslib.WordRAM Cslib.WordRAM.Realization
+
+/-- Write the rear's next physical cell and return the two new count words. There is no echo
+of the delivered payload in the result. -/
+def enqueue (d : Input) : Memory.Prog (ℕ × ℕ) := do
+  Memory.write (d 2 + d 3 + d 1) (d 4)
+  pure (d 0, d 1 + 1)
+
+/-- The original queue enqueue domain, with the physical room unchanged. -/
+def enqueueDomain (w : ℕ) (d : Input) (s : Memory.State) : Prop :=
+  d 0 + d 1 < d 3 ∧ d 2 + 2 * d 3 ≤ s.frontier ∧ Fits w (d 4)
+
+/-- An empty front returns none without a memory query. A nonempty front reads its top and
+returns a decremented count; the unused physical cell is retained. -/
+def popFront (d : Input) : Memory.Prog ((ℕ × ℕ) × Option ℕ) :=
+  if d 0 = 0 then pure ((d 0, d 1), none) else do
+    let v ← Memory.read (d 2 + (d 0 - 1))
+    pure ((d 0 - 1, d 1), some v)
+
+/-- The front-empty path transfers the rear before performing the original front pop. -/
+def dequeue (d : Input) : Memory.Prog ((ℕ × ℕ) × Option ℕ) :=
+  if d 0 = 0 then do
+    let m ← transfer d
+    popFront ![m.1, m.2, d 2, d 3, d 4]
+  else popFront d
+
+/-- One uniform enqueue body, with all address arithmetic, result copies and control charged. -/
+theorem realizes_enqueue : Realizes .exact enqueue (.refl Input) counts
+    enqueueDomain (fun _ _ => 0) := by
+  change Realizes .exact enqueue (.refl (Fin 5 → ℕ)) counts _ _
+  realize
+  · exact hmem.fits_of_lt_frontier (by have := h.1; have := h.2.1; omega)
+  · exact (show Fits w (d 3) from hwords 3).of_le (by have := h.1; omega)
+
+/-- A uniform typed pop body; the option tag is separate from its full-range word payload. -/
+theorem realizes_popFront : Realizes .exact popFront (.refl Input)
+    (appendWords counts optionWords) transferDomain (fun _ _ => 0) := by
+  change Realizes .exact popFront (.refl (Fin 5 → ℕ)) _ _ _
+  realize
+  · omega
+  · exact hmem.fits_of_lt_frontier (by have := h.1; have := h.2; omega)
+  · exact (show Fits w (d 0) from hwords 0).of_le (by omega)
+
+/-- Dequeue reuses the shared remaining-count transfer and preserves the exact old room. -/
+theorem realizes_dequeue : Realizes .exact dequeue (.refl Input)
+    (appendWords counts optionWords) transferDomain (fun _ _ => 0) := by
+  change Realizes .exact dequeue (.refl (Fin 5 → ℕ)) _ _ _
+  realize
+  all_goals try omega
+  case hsafe.isTrue.left =>
+    intro hv
+    refine whileSafe_of_measure _ _ _ w d
+      (fun m t => Memory.WellFormed w t ∧ m.1 + m.2 ≤ d 3 ∧ d 2 + 2 * d 3 ≤ t.frontier)
+      (fun m _ => m.2) (fun m _ _ hz hg => by omega) ?_ ⟨hmem, h.1, h.2⟩ le_rfl hv
+    rintro m t ⟨hwt, hcap, hfrontier⟩ hg hb
+    refine ⟨?_, ?_, ?_⟩
+    · change (1 ≤ m.2 ∧ Fits w (d 2 + d 3 + (m.2 - 1))) ∧
+        Fits w (d 2 + m.1) ∧ 1 ≤ m.2 ∧ Fits w (m.1 + 1)
+      exact ⟨⟨by omega, hwt.fits_of_lt_frontier (by omega)⟩,
+        hwt.fits_of_lt_frontier (by omega), by omega,
+        (show Fits w (d 3) from hwords 3).of_le (by omega)⟩
+    · have hw' : Memory.WellFormed w
+          ((Memory.spec 0).clientState t (move ![m.1, m.2, d 2, d 3, d 4])) := by
+        rw [← clientState_width w, ← (Memory.spec w).run_runClient]
+        exact hwt.run hb
+      refine ⟨hw', ?_, ?_⟩
+      · change (m.1 + 1) + (m.2 - 1) ≤ d 3
+        omega
+      · exact hfrontier
+    · change m.2 - 1 < m.2
+      omega
+  case hsafe.isTrue.right.isFalse.left.right =>
+    have hr := (transfer_invariant hmem h).2.2.1
+    rw [hr] at hc ⊢
+    change d 0 + d 1 ≠ 0 at hc
+    change Fits w (d 2 + (d 0 + d 1 - 1))
+    exact hmem.fits_of_lt_frontier (by have := h.1; have := h.2; omega)
+  case hsafe.isTrue.right.isFalse.right.right =>
+    have hr := (transfer_invariant hmem h).2.2.1
+    rw [hr] at hc
+    change d 0 + d 1 ≠ 0 at hc
+    exact (show Fits w (d 3) from hwords 3).of_le (by have := h.1; omega)
+  case hsafe.isFalse.isFalse.left.right =>
+    exact hmem.fits_of_lt_frontier (by have := h.1; have := h.2; omega)
+  case hsafe.isFalse.isFalse.right.right =>
+    exact (show Fits w (d 0) from hwords 0).of_le (by omega)
+
+/-- The original standard word-RAM basis has the same checked method behavior. -/
+theorem realizes_enqueue_standard : Realizes .standard enqueue (.refl Input) counts
+    enqueueDomain (fun _ _ => 0) :=
+  realizes_enqueue.mapSimulates Basis.Simulates.exactStandard
+
+/-- Standard-basis dequeue keeps both counts and the faithful option result. -/
+theorem realizes_dequeue_standard : Realizes .standard dequeue (.refl Input)
+    (appendWords counts optionWords) transferDomain (fun _ _ => 0) :=
+  realizes_dequeue.mapSimulates Basis.Simulates.exactStandard
+
+/-- Enqueue issues exactly the physical rear write, retaining the frontier. -/
+theorem runClient_enqueue (w : ℕ) (d : Input) (s : Memory.State) :
+    (Memory.spec w).runClient s (enqueue d) =
+      ((d 0, d 1 + 1), ⟨Function.update s.mem (d 2 + d 3 + d 1) (d 4), s.frontier⟩,
+        [.write (d 2 + d 3 + d 1) (d 4)]) := rfl
+
+/-- The spare-capacity domain admits the one physical write, including the delivered value. -/
+theorem valid_enqueue {w : ℕ} {d : Input} {s : Memory.State}
+    (h : enqueueDomain w d s) :
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (enqueue d)) := by
+  change (d 2 + d 3 + d 1 < s.frontier ∧ Fits w (d 4)) ∧ True
+  exact ⟨⟨by have := h.1; have := h.2.1; omega, h.2.2⟩, trivial⟩
+
+/-- Enqueue uses one memory query, independently of the capacity and existing contents. -/
+theorem memoryCost_enqueue (d : Input) (s : Memory.State) :
+    memoryCost (enqueue d) s = 1 := rfl
+
+/-- The rear write remains inside the original two-array footprint. -/
+theorem enqueue_modifies {w : ℕ} {d : Input} {s : Memory.State}
+    (h : enqueueDomain w d s) :
+    Modifies (Block.mk (d 2) (2 * d 3)).footprint s.mem
+      ((Memory.spec w).clientState s (enqueue d)).mem := by
+  exact Modifies.write_of_owns ⟨by omega, by have := h.1; omega⟩ _
+
+/-- Pop never changes any memory cell or the frontier, including its empty path. -/
+theorem clientState_popFront (w : ℕ) (d : Input) (s : Memory.State) :
+    (Memory.spec w).clientState s (popFront d) = s := by
+  by_cases hz : d 0 = 0
+  · rw [popFront, ite_eq_left hz]
+    rfl
+  · rw [popFront, ite_eq_right hz]
+    rfl
+
+/-- Both returned counts are exact even when the unused physical top cell remains dirty. -/
+theorem clientResult_popFront (w : ℕ) (d : Input) (s : Memory.State) :
+    (Memory.spec w).clientResult s (popFront d) =
+      if d 0 = 0 then ((d 0, d 1), none)
+      else ((d 0 - 1, d 1), some (s.mem (d 2 + (d 0 - 1)))) := by
+  by_cases hz : d 0 = 0
+  · rw [popFront, ite_eq_left hz, ite_eq_left hz]
+    rfl
+  · rw [popFront, ite_eq_right hz, ite_eq_right hz]
+    rfl
+
+/-- A nonempty front performs one read; an empty front performs no memory operation. -/
+theorem memoryCost_popFront (d : Input) (s : Memory.State) :
+    memoryCost (popFront d) s = if d 0 = 0 then 0 else 1 := by
+  by_cases hz : d 0 = 0
+  · rw [popFront, ite_eq_left hz, ite_eq_left hz]
+    rfl
+  · rw [popFront, ite_eq_right hz, ite_eq_right hz]
+    rfl
+
+/-- Every nonempty front read lies in the old physical region. -/
+theorem valid_popFront {w : ℕ} {d : Input} {s : Memory.State}
+    (h : transferDomain w d s) :
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (popFront d)) := by
+  by_cases hz : d 0 = 0
+  · rw [popFront, ite_eq_left hz]
+    trivial
+  · rw [popFront, ite_eq_right hz]
+    change (Memory.spec w).ValidHistory s
+      ((Memory.spec w).clientHistory s (do
+        let v ← Memory.read (d 2 + (d 0 - 1))
+        pure ((d 0 - 1, d 1), some v)))
+    change (d 2 + (d 0 - 1) < s.frontier) ∧ True
+    exact ⟨by have := h.1; have := h.2; omega, trivial⟩
+
+/-- Dequeue's source summary retains the actual final counts, valid physical history and
+frontier. The fallback performs exactly two queries per transferred element and one final
+read when the queue was nonempty. -/
+theorem dequeue_invariant {w : ℕ} {d : Input} {s : Memory.State}
+    (hw : Memory.WellFormed w s) (h : transferDomain w d s) :
+    let t := (Memory.spec 0).clientState s (dequeue d)
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (dequeue d)) ∧
+      Memory.WellFormed w t ∧
+      ((Memory.spec 0).clientResult s (dequeue d)).1 =
+        (if d 0 = 0 then (d 1 - 1, 0) else (d 0 - 1, d 1)) ∧
+      t.frontier = s.frontier ∧
+      memoryCost (dequeue d) s =
+        (if d 0 = 0 then 2 * d 1 + (if d 1 = 0 then 0 else 1) else 1) ∧
+      Modifies (Block.mk (d 2) (2 * d 3)).footprint s.mem t.mem := by
+  by_cases hz : d 0 = 0
+  · obtain ⟨hv, hwt, hr, hf, hc, hm⟩ := transfer_invariant hw h
+    have hr' : (Memory.spec 0).clientResult s (transfer d) = (d 1, 0) := by
+      simpa only [hz, Nat.zero_add] using hr
+    let t := (Memory.spec 0).clientState s (transfer d)
+    let e : Input := ![d 1, 0, d 2, d 3, d 4]
+    have he : transferDomain w e t := by
+      refine ⟨?_, ?_⟩
+      · change d 1 + 0 ≤ d 3
+        have := h.1
+        omega
+      · change d 2 + 2 * d 3 ≤ t.frontier
+        rw [hf]
+        exact h.2
+    have hs : (Memory.spec 0).clientState s (dequeue d) = t := by
+      rw [dequeue, ite_eq_left hz, StateTransitionSpec.clientState_bind, hr']
+      exact clientState_popFront 0 e t
+    refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
+    · rw [dequeue, ite_eq_left hz]
+      change (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s
+        ((transfer d).bind (fun m => popFront ![m.1, m.2, d 2, d 3, d 4])))
+      rw [validHistory_bind]
+      refine ⟨hv, ?_⟩
+      rw [clientState_width w, clientResult_width w, hr']
+      exact valid_popFront he
+    · rw [hs]
+      exact hwt
+    · rw [dequeue, ite_eq_left hz, StateTransitionSpec.clientResult_bind, hr',
+        clientResult_popFront, ite_eq_left hz]
+      change (if d 1 = 0 then ((d 1, 0), none)
+        else ((d 1 - 1, 0), some (t.mem (d 2 + (d 1 - 1))))).1 = (d 1 - 1, 0)
+      split <;> simp_all
+    · rw [hs]
+      exact hf
+    · rw [dequeue, ite_eq_left hz]
+      change memoryCost ((transfer d).bind (fun m => popFront ![m.1, m.2, d 2, d 3, d 4])) s = _
+      rw [memoryCost_bind, hr', hc, memoryCost_popFront, ite_eq_left hz]
+      rfl
+    · rw [hs]
+      exact hm
+  · have hs : (Memory.spec 0).clientState s (dequeue d) = s := by
+      rw [dequeue, ite_eq_right hz, clientState_popFront]
+    refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
+    · rw [dequeue, ite_eq_right hz]
+      exact valid_popFront h
+    · rw [hs]
+      exact hw
+    · rw [dequeue, ite_eq_right hz, clientResult_popFront, ite_eq_right hz, ite_eq_right hz]
+    · rw [hs]
+    · rw [dequeue, ite_eq_right hz, memoryCost_popFront, ite_eq_right hz, ite_eq_right hz]
+    · rw [hs]
+      exact fun _ _ => rfl
+
+/-- At the source-memory boundary, one enqueue pays for its write and the added rear credit.
+Native glue and the final halt are accounted for separately by the realized dispatcher. -/
+theorem enqueue_memory_amortized (d : Input) (s : Memory.State) :
+    memoryCost (enqueue d) s + 2 * ((Memory.spec 0).clientResult s (enqueue d)).2 =
+      3 + 2 * d 1 := by
+  change 1 + 2 * (d 1 + 1) = _
+  omega
+
+/-- The actual transfer queries are paid by the initial rear credit, including a final
+nonempty pop. This is a source-memory bound, not a claim that native glue is free. -/
+theorem dequeue_memory_amortized {w : ℕ} {d : Input} {s : Memory.State}
+    (hw : Memory.WellFormed w s) (h : transferDomain w d s) :
+    memoryCost (dequeue d) s + 2 * ((Memory.spec 0).clientResult s (dequeue d)).1.2 ≤
+      3 + 2 * d 1 := by
+  have hi := dequeue_invariant hw h
+  rw [hi.2.2.1, hi.2.2.2.2.1]
+  split <;> (try split) <;> simp_all
+
+end Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
diff --git a/Complexity/DataStructure/Queue/WordRAM/RegisterProgram.lean b/Complexity/DataStructure/Queue/WordRAM/RegisterProgram.lean
new file mode 100644
index 0000000000..aa3c7a9f71
--- /dev/null
+++ b/Complexity/DataStructure/Queue/WordRAM/RegisterProgram.lean
@@ -0,0 +1,152 @@
+/-
+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.DataStructure.Queue.WordRAM.RegisterCorrectness
+public import Complexity.Computability.WordRAM.Realization.Backend
+
+/-!
+# One fixed queue dispatcher over realized physical-array methods
+
+The finite method family chooses all code and register packing before any runtime count,
+base, capacity, width, memory or operation. Only the tag and payload are delivered by the
+external dynamic calling convention. The count words, base, capacity and frontier remain
+resident. A native branch selects a body, and two actual copies commit its returned counts.
+
+The initializer is a literal-parameterized code family, as in the original queue: base and
+capacity are fixed before the arbitrary dirty entry data. It writes registers only, performs
+six instructions, and reserves exactly `2*capacity` physical cells. It is not a memory-clearing
+initializer or an uncharged use of `Backend.install`.
+
+## Main definitions
+
+* `family`, `program`: the finite body family and its fixed native dispatcher.
+* `implementation`: the existing dynamic-program calling convention and typed observation.
+* `Rep`, `QueueRep`, `footprint`: the original two physical arrays with resident count words.
+* `initializeCode`, `initialized`: six register writes and their exact state.
+
+## References
+
+The queue and its algorithmic references are in `Cslib.DataStructure.Queue.Spec`.
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.Queue.WordRAM
+
+open Cslib.WordRAM Cslib.WordRAM.Realization
+open RegisterMetadata
+open Cslib.DataStructure.Queue
+
+/-- One fixed family contains both method bodies. Runtime arguments select no new code. -/
+noncomputable abbrev family : Bool → Certificate .standard
+  | false => ⟨realizes_enqueue_standard⟩
+  | true => ⟨realizes_dequeue_standard⟩
+
+/-- One finite register file for both bodies and the dispatcher. -/
+noncomputable abbrev registers := Backend.registers family
+
+/-- The complete physical reservation, including unused array cells. -/
+def footprint (base capacity : ℕ) : Finset ℕ := (Block.mk base (2 * capacity)).footprint
+
+/-- Persistent count, layout and payload bank. Both tags have the same five-word input. -/
+noncomputable def src (i : Fin 5) : Fin registers := Backend.src family false i
+
+/-- The two counts occupy the first two words of this common result prefix. -/
+noncomputable def result (i : Fin 4) : Fin registers :=
+  Backend.tmp family true (Fin.castAdd ((family true).realizes.scratchSize + 1) i)
+
+/-- Tag delivery reuses scratch word zero, which the selected body may overwrite. -/
+noncomputable abbrev tag : Fin registers := result 0
+
+/-- A paid zero constant for the native tag test, also in the shared scratch bank. -/
+noncomputable abbrev zero : Fin registers := result 1
+
+/-- Two paid copies update the resident count bank. -/
+noncomputable def commit : Code .standard registers :=
+  .seq (.op (.copy (src 0) (result 0))) (.op (.copy (src 1) (result 1)))
+
+/-- The same native program executes every operation. No host-selected body is substituted. -/
+noncomputable def program : Code .standard registers :=
+  .seq (.op (.const zero 0))
+    (.seq (.branch (.eq tag zero) (Backend.code family false) (Backend.code family true)) commit)
+
+/-- Only the tag and payload are external inputs. The result decoder observes Unit for
+enqueue and the faithful option tag/value for dequeue; enqueue need not echo its argument. -/
+noncomputable def implementation (w capacity : ℕ) :
+    DynamicProgram (spec w capacity) registers where
+  code := program
+  output := result 3
+  input i := i == tag || i == src 4
+  encode o i := if i = tag then
+    match o with | .enqueue _ => 0 | .dequeue => 1
+    else match o with | .enqueue v => v | .dequeue => 0
+  decode o regs := match o with
+    | .enqueue _ => some ()
+    | .dequeue => some (if regs (result 2) = 0 then none else some (regs (result 3)))
+
+/-- The existing two-array representation, with counts and layout in the shared input bank.
+Unused cells and the delivered tag/payload impose no extra memory or register premise. -/
+structure Rep (w base capacity : ℕ) (front back : List ℕ) (x : Data registers) : Prop where
+  bounded : x.Bounded w
+  base_eq : x.regs (src 2) = base
+  capacity_eq : x.regs (src 3) = capacity
+  frontier_eq : x.regs (Backend.frontier family) = base + 2 * capacity
+  frontLen_eq : x.regs (src 0) = front.length
+  backLen_eq : x.regs (src 1) = back.length
+  size_le : front.length + back.length ≤ capacity
+  front_contents : Block.HoldsList base front.reverse x.mem
+  back_contents : Block.HoldsList (base + capacity) back.reverse x.mem
+
+/-- The same logical FIFO projection as the original queue. -/
+def QueueRep (w base capacity : ℕ) (q : List ℕ) (x : Data registers) : Prop :=
+  ∃ front back, q = contents (front, back) ∧ Rep w base capacity front back x
+
+/-- The actual resident input words, without installing the maintained metadata again. -/
+theorem Rep.input_eq {w base capacity : ℕ} {front back : List ℕ} {x : Data registers}
+    (hr : Rep w base capacity front back x) :
+    x.regs ∘ src = ![front.length, back.length, base, capacity, x.regs (src 4)] := by
+  funext i
+  fin_cases i
+  · exact hr.frontLen_eq
+  · exact hr.backLen_eq
+  · exact hr.base_eq
+  · exact hr.capacity_eq
+  · rfl
+
+/-- Rear credit is scaled by the single native exchange factor. This definition does not
+assert the still separate dispatcher clock or the final per-call amortized inequality. -/
+noncomputable def potential (x : Data registers) : ℕ :=
+  2 * Backend.factor family * x.regs (src 1)
+
+/-- Exact initialized data: only the frontier, counts, layout and zero scratch word change. -/
+noncomputable def initialized (base capacity : ℕ) (x : Data registers) : Data registers :=
+  (((((x.set (Backend.frontier family) (base + 2 * capacity)).set (src 0) 0).set
+    (src 1) 0).set (src 2) base).set (src 3) capacity).set zero 0
+
+/-- A literal base/capacity initializer with the original uniform six-instruction cost. -/
+noncomputable def initializeCode (base capacity : ℕ) : Code .standard registers :=
+  .seq (.op (.const (Backend.frontier family) (base + 2 * capacity)))
+    (.seq (.op (.const (src 0) 0)) (.seq (.op (.const (src 1) 0))
+      (.seq (.op (.const (src 2) base))
+        (.seq (.op (.const (src 3) capacity)) (.op (.const zero 0))))))
+
+/-- Initialization starts from arbitrary bounded dirty data and keeps every memory cell.
+The original `Fits w 1` premise is needed by operation tag delivery, not these zero writes. -/
+theorem initialize_exec {w base capacity : ℕ} {x : Data registers} (hx : x.Bounded w)
+    (hc : Fits w (base + 2 * capacity)) :
+    Exec w (initializeCode base capacity) x (initialized base capacity x) 6 ∧
+      (initialized base capacity x).Bounded w ∧ (initialized base capacity x).mem = x.mem := by
+  have hb : Fits w base := hc.of_le (by omega)
+  have hcap : Fits w capacity := hc.of_le (by omega)
+  have he : Exec w (initializeCode base capacity) x (initialized base capacity x) 6 :=
+    (Exec.const hc).seq ((Exec.const (fits_zero w)).seq ((Exec.const (fits_zero w)).seq
+      ((Exec.const hb).seq ((Exec.const hcap).seq (Exec.const (fits_zero w))))))
+  exact ⟨he, he.bounded hx, rfl⟩
+
+end Cslib.DataStructure.Queue.WordRAM
diff --git a/Complexity/DataStructure/Queue/WordRAM/RegisterTransfer.lean b/Complexity/DataStructure/Queue/WordRAM/RegisterTransfer.lean
new file mode 100644
index 0000000000..5a8decf4cb
--- /dev/null
+++ b/Complexity/DataStructure/Queue/WordRAM/RegisterTransfer.lean
@@ -0,0 +1,221 @@
+/-
+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.DataStructure.Queue.WordRAM.RegisterMetadata
+public import Complexity.Computability.WordRAM.Realization.WhileAbsorb
+public import Complexity.Computability.WordRAM.ListArray
+import Complexity.Tactic.Realize
+
+/-!
+# Queue transfer with explicit register metadata
+
+Both stack counts are explicit input and result words. The source uses the existing memory
+programs and bounded while, writes only the original two physical arrays, and neither allocates
+count cells nor changes unallocated memory. The remaining rear count is the loop rank.
+
+## Main definitions
+
+* `transfer`: the remaining-count loop over the shared physical transfer step.
+* `transferDomain`: the old combined-capacity and physical frontier envelope.
+
+## Main results
+
+* `realizes_transfer`: one native emitter before every count, layout, width and memory.
+* `realizes_transfer_standard`: the same semantics on the original standard word-RAM basis.
+* `transfer_invariant`: valid histories, exact two-query-per-item cost, count and memory frame.
+* `transfer_contents`: the physical arrays have exactly the original reversal semantics.
+
+## References
+
+The queue and its algorithmic references are in `Cslib.DataStructure.Queue.Spec`.
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
+
+open Cslib.WordRAM Cslib.WordRAM.Realization
+
+/-- Reuse the shared physical step with the current two count words. -/
+def transferBody (d : Input × (ℕ × ℕ)) : Memory.Prog (ℕ × ℕ) :=
+  move ![d.2.1, d.2.2, d.1 2, d.1 3, d.1 4]
+
+/-- Move the whole rear, using the explicit rear count as a sufficient ghost cutoff. -/
+def transfer (d : Input) : Memory.Prog (ℕ × ℕ) :=
+  boundedWhile (fun _ m => 0 < m.2) transferBody d (d 1) (d 0, d 1)
+
+/-- Both arrays use the old `2*C` physical room; the two counts occupy registers. -/
+def transferDomain (_w : ℕ) (d : Input) (s : Memory.State) : Prop :=
+  d 0 + d 1 ≤ d 3 ∧ d 2 + 2 * d 3 ≤ s.frontier
+
+/-- The canonical tactic certifies the actual memory-query loop. Every guard and count-copy
+instruction is paid through the existing realization factor. -/
+theorem realizes_transfer : Realizes .exact transfer (.refl Input) counts
+    transferDomain (fun _ _ => 0) := by
+  change Realizes .exact transfer (.refl (Fin 5 → ℕ)) counts _ _
+  realize
+  intro hv
+  refine whileSafe_of_measure _ _ _ w d
+    (fun m t => Memory.WellFormed w t ∧ m.1 + m.2 ≤ d 3 ∧ d 2 + 2 * d 3 ≤ t.frontier)
+    (fun m _ => m.2) (fun m _ _ hz hg => by omega) ?_ ⟨hmem, h.1, h.2⟩ le_rfl hv
+  rintro m t ⟨hwt, hcap, hfrontier⟩ hg hb
+  refine ⟨?_, ?_, ?_⟩
+  · change (1 ≤ m.2 ∧ Fits w (d 2 + d 3 + (m.2 - 1))) ∧
+      Fits w (d 2 + m.1) ∧ 1 ≤ m.2 ∧ Fits w (m.1 + 1)
+    exact ⟨⟨by omega, hwt.fits_of_lt_frontier (by omega)⟩,
+      hwt.fits_of_lt_frontier (by omega), by omega,
+      (show Fits w (d 3) from hwords 3).of_le (by omega)⟩
+  · have hw' : Memory.WellFormed w
+        ((Memory.spec 0).clientState t (move ![m.1, m.2, d 2, d 3, d 4])) := by
+      rw [← clientState_width w, ← (Memory.spec w).run_runClient]
+      exact hwt.run hb
+    refine ⟨hw', ?_, ?_⟩
+    · change (m.1 + 1) + (m.2 - 1) ≤ d 3
+      omega
+    · exact hfrontier
+  · change m.2 - 1 < m.2
+    omega
+
+/-- The existing defined-evaluation simulation gives the same literal memory semantics on the
+standard word-RAM basis used by the original queue. No overflow/underflow behavior is weakened. -/
+theorem realizes_transfer_standard : Realizes .standard transfer (.refl Input) counts
+    transferDomain (fun _ _ => 0) :=
+  realizes_transfer.mapSimulates Basis.Simulates.exactStandard
+
+private theorem transfer_summary (d : Input) (F n : ℕ) {w : ℕ} {s : Memory.State}
+    (hw : Memory.WellFormed w s) (hc : F + n ≤ d 3)
+    (hf : d 2 + 2 * d 3 ≤ s.frontier) :
+    let p := boundedWhile (fun _ m => 0 < m.2) transferBody d n (F, n)
+    let t := (Memory.spec 0).clientState s p
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s p) ∧
+      Memory.WellFormed w t ∧ (Memory.spec 0).clientResult s p = (F + n, 0) ∧
+      t.frontier = s.frontier ∧ memoryCost p s = 2 * n ∧
+      Modifies (Block.mk (d 2) (2 * d 3)).footprint s.mem t.mem := by
+  induction n generalizing F s with
+  | zero => exact ⟨trivial, hw, rfl, rfl, rfl, fun _ _ => rfl⟩
+  | succ n ih =>
+    let b := transferBody (d, (F, n + 1))
+    let t₁ := (Memory.spec 0).clientState s b
+    have hdom : domain w ![F, n + 1, d 2, d 3, d 4] s :=
+      ⟨Nat.zero_lt_succ n, hc, hf⟩
+    have hvb : (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s b) :=
+      valid_move hw hdom
+    have hw₁ : Memory.WellFormed w t₁ := by
+      change Memory.WellFormed w ((Memory.spec 0).clientState s b)
+      rw [← clientState_width w, ← (Memory.spec w).run_runClient]
+      exact hw.run hvb
+    have hresult : (Memory.spec 0).clientResult s b = (F + 1, n) := rfl
+    have hfrontier : t₁.frontier = s.frontier := rfl
+    obtain ⟨hvt, hwt, hrt, hft, hct, hmt⟩ := ih (F + 1) hw₁ (by omega) (by
+      rw [hfrontier]
+      exact hf)
+    let rest := boundedWhile (fun _ m => 0 < m.2) transferBody d n
+    have hstate : (Memory.spec 0).clientState s
+        (boundedWhile (fun _ m => 0 < m.2) transferBody d (n + 1) (F, n + 1)) =
+        (Memory.spec 0).clientState t₁ (rest (F + 1, n)) := by
+      change (Memory.spec 0).clientState s (b.bind rest) = _
+      simp only [StateTransitionSpec.clientState, StateTransitionSpec.runClient_bind]
+      change (Memory.spec 0).clientState t₁ (rest ((Memory.spec 0).clientResult s b)) = _
+      rw [hresult]
+    refine ⟨?_, hstate ▸ hwt, ?_, hstate ▸ hft.trans hfrontier, ?_, ?_⟩
+    · change (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (b.bind rest))
+      apply (validHistory_bind w b rest s).mpr
+      refine ⟨hvb, ?_⟩
+      rw [clientState_width w, clientResult_width w, hresult]
+      exact hvt
+    · change (Memory.spec 0).clientResult s (b.bind rest) = _
+      simp only [StateTransitionSpec.clientResult, StateTransitionSpec.runClient_bind]
+      change (Memory.spec 0).clientResult t₁ (rest ((Memory.spec 0).clientResult s b)) = _
+      rw [hresult, hrt]
+      congr 1
+      omega
+    · change memoryCost (b.bind rest) s = _
+      rw [memoryCost_bind, hresult, hct]
+      have hb : memoryCost b s = 2 := rfl
+      omega
+    · intro j hj
+      rw [hstate]
+      exact (hmt j hj).trans (move_modifies (w := 0) hdom j hj)
+
+/-- Transfer is valid on arbitrary well-formed physical memory under the original room
+envelope. It performs exactly two memory queries per moved element and preserves the entire
+memory outside the old `2*C` block. The two returned counts are the actual final counts. -/
+theorem transfer_invariant {w : ℕ} {d : Input} {s : Memory.State}
+    (hw : Memory.WellFormed w s) (h : transferDomain w d s) :
+    let t := (Memory.spec 0).clientState s (transfer d)
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (transfer d)) ∧
+      Memory.WellFormed w t ∧ (Memory.spec 0).clientResult s (transfer d) = (d 0 + d 1, 0) ∧
+      t.frontier = s.frontier ∧ memoryCost (transfer d) s = 2 * d 1 ∧
+      Modifies (Block.mk (d 2) (2 * d 3)).footprint s.mem t.mem :=
+  transfer_summary d (d 0) (d 1) hw h.1 h.2
+
+private theorem transfer_contents_aux (d : Input) (back front : List ℕ) (s : Memory.State)
+    (hc : front.length + back.length ≤ d 3)
+    (hfront : Block.HoldsList (d 2) front.reverse s.mem)
+    (hback : Block.HoldsList (d 2 + d 3) back.reverse s.mem) :
+    Block.HoldsList (d 2) (back.reverse ++ front).reverse
+      ((Memory.spec 0).clientState s
+        (boundedWhile (fun _ m => 0 < m.2) transferBody d back.length
+          (front.length, back.length))).mem := by
+  induction back generalizing front s with
+  | nil =>
+    simpa only [List.length_nil, boundedWhile, StateTransitionSpec.clientState,
+      StateTransitionSpec.runClient_pure', List.reverse_nil, List.nil_append] using hfront
+  | cons v back ih =>
+    have hread : s.mem (d 2 + d 3 + back.length) = v := by
+      simpa [List.reverse_cons] using hback.get back.length (by simp)
+    let t : Memory.State := ⟨Function.update s.mem (d 2 + front.length) v, s.frontier⟩
+    have hfront' : Block.HoldsList (d 2) (v :: front).reverse t.mem := by
+      simpa only [t, List.reverse_cons, List.length_reverse] using hfront.append_one v
+    have hback' : Block.HoldsList (d 2 + d 3) back.reverse t.mem := by
+      have hprefix : Block.HoldsList (d 2 + d 3) back.reverse s.mem := by
+        simpa [List.reverse_cons] using hback.take back.length
+      apply hprefix.frame
+      intro a ha _
+      exact Function.update_of_ne (by have := hc; simp only [List.length_cons] at this; omega) _ _
+    have hc' : (v :: front).length + back.length ≤ d 3 := by
+      simp only [List.length_cons] at hc ⊢
+      omega
+    have hi := ih (v :: front) t hc' hfront' hback'
+    let b := transferBody (d, (front.length, (v :: back).length))
+    have hrun : (Memory.spec 0).runClient s b =
+        ((front.length + 1, back.length), t,
+          [Memory.Op.read (d 2 + d 3 + back.length), Memory.Op.write (d 2 + front.length) v]) := by
+      change ((front.length + 1, back.length),
+        (⟨Function.update s.mem (d 2 + front.length)
+          (s.mem (d 2 + d 3 + back.length)), s.frontier⟩ : Memory.State),
+        [Memory.Op.read (d 2 + d 3 + back.length), Memory.Op.write (d 2 + front.length)
+          (s.mem (d 2 + d 3 + back.length))]) = _
+      rw [hread]
+    have hstate : (Memory.spec 0).clientState s
+        (boundedWhile (fun _ m => 0 < m.2) transferBody d (v :: back).length
+          (front.length, (v :: back).length)) =
+        (Memory.spec 0).clientState t
+          (boundedWhile (fun _ m => 0 < m.2) transferBody d back.length
+            ((v :: front).length, back.length)) := by
+      change (Memory.spec 0).clientState s
+        (b.bind (boundedWhile (fun _ m => 0 < m.2) transferBody d back.length)) = _
+      simp only [StateTransitionSpec.clientState, StateTransitionSpec.runClient_bind, hrun,
+        List.length_cons]
+    rw [hstate]
+    simpa only [List.reverse_cons, List.append_assoc, List.singleton_append] using hi
+
+/-- The physical arrays have exactly the original transfer semantics: the reversed rear is
+placed on top of the front. This proof reuses the generic list-array append, prefix and frame
+lemmas; no machine step table or count-cell representation is introduced. -/
+theorem transfer_contents {d : Input} (back front : List ℕ) (s : Memory.State)
+    (hF : d 0 = front.length) (hB : d 1 = back.length)
+    (hc : front.length + back.length ≤ d 3)
+    (hfront : Block.HoldsList (d 2) front.reverse s.mem)
+    (hback : Block.HoldsList (d 2 + d 3) back.reverse s.mem) :
+    Block.HoldsList (d 2) (back.reverse ++ front).reverse
+      ((Memory.spec 0).clientState s (transfer d)).mem := by
+  simpa only [transfer, hF, hB] using transfer_contents_aux d back front s hc hfront hback
+
+end Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
diff --git a/ComplexityTests/QueueMemoryTransfer.lean b/ComplexityTests/QueueMemoryTransfer.lean
new file mode 100644
index 0000000000..95c2c7f955
--- /dev/null
+++ b/ComplexityTests/QueueMemoryTransfer.lean
@@ -0,0 +1,69 @@
+/-
+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: local-only (tests of the memory queue migration)
+
+public import Complexity.DataStructure.Queue.Memory.Transfer
+
+@[expose] public section
+
+namespace ComplexityTests.QueueMemoryTransfer
+
+open Cslib Cslib.DataStructure Cslib.WordRAM Cslib.WordRAM.Realization
+
+def front : Stack.Memory.Layout := ⟨⟨0, 1⟩, ⟨1, 2⟩⟩
+def rear : Stack.Memory.Layout := ⟨⟨3, 1⟩, ⟨4, 2⟩⟩
+
+def memory : Memory.State :=
+  ⟨fun a => if a = 3 then 2 else if a = 4 then 3 else if a = 7 then 5 else 0, 6⟩
+
+def source : Memory.Prog ℕ :=
+  boundedWhile (fun _ r => 0 < r) Queue.Memory.transferBody (front, rear) 2 2
+
+example : (Memory.spec 3).clientResult memory source = 0 := rfl
+example : ((Memory.spec 3).clientState memory source).mem 0 = 2 := rfl
+example : ((Memory.spec 3).clientState memory source).mem 3 = 0 := rfl
+example : ((Memory.spec 3).clientState memory source).mem 7 = 5 := rfl
+example : Stack.Memory.abs front ((Memory.spec 3).clientState memory source) = [3, 0] := rfl
+
+-- The ghost cutoff may exceed the count without changing the linked source or its history.
+example :
+    link (Methods.prod (Stack.Memory.methods front 3 2) (Stack.Memory.methods rear 3 2))
+        (Queue.transfer 2) =
+      (boundedWhile (fun _ r => 0 < r) Queue.Memory.transferBody (front, rear) 9 2).bind
+        (fun _ => pure ()) :=
+  Queue.Memory.transfer_eq_boundedWhile front rear 3 2 9 2 (by omega)
+
+-- A positive remaining count on an empty rear performs just the terminating count read.
+example :
+    (Memory.spec 3).clientHistory (⟨fun _ => 0, 6⟩ : Memory.State)
+      (boundedWhile (fun _ r => 0 < r) Queue.Memory.transferBody (front, rear) 4 4) =
+        [.read 3] := rfl
+
+-- The existing invariants are satisfiable at the concrete nonempty transfer above.
+example :
+    let p := link (Methods.prod (Stack.Memory.methods front 3 2)
+      (Stack.Memory.methods rear 3 2)) (Queue.transfer 2)
+    let s' := (Memory.spec 3).clientState memory p
+    (Memory.spec 3).ValidHistory memory ((Memory.spec 3).clientHistory memory p) ∧
+      Memory.WellFormed 3 s' ∧ Stack.Memory.Inv front s' ∧ Stack.Memory.Inv rear s' ∧
+      s'.mem rear.count.base = 0 ∧ s'.mem front.count.base = memory.mem front.count.base + 2 ∧
+      Stack.Memory.abs front s' = (Stack.Memory.abs rear memory).reverse ++
+        Stack.Memory.abs front memory := by
+  apply Queue.Memory.transfer_invariant (w := 3) (C := 2)
+  · exact ⟨rfl, by change ¬(1 ≤ 0 ∧ 0 < 1 + 2); decide, rfl, by decide⟩
+  · exact ⟨rfl, by change ¬(4 ≤ 3 ∧ 3 < 4 + 2); decide, rfl, by decide⟩
+  · decide
+  · refine ⟨by decide, fun a => ?_⟩
+    dsimp only [memory]
+    split <;> (try split) <;> (try split) <;> decide
+  · exact ⟨by change 0 + 1 ≤ 6; decide, by change 1 + 2 ≤ 6; decide, by decide⟩
+  · exact ⟨by change 3 + 1 ≤ 6; decide, by change 4 + 2 ≤ 6; decide, by decide⟩
+  · rfl
+  · decide
+
+end ComplexityTests.QueueMemoryTransfer
diff --git a/ComplexityTests/QueueRegisterCorrectness.lean b/ComplexityTests/QueueRegisterCorrectness.lean
new file mode 100644
index 0000000000..cf990d0827
--- /dev/null
+++ b/ComplexityTests/QueueRegisterCorrectness.lean
@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: local-only (test driver)
+
+public import Complexity.DataStructure.Queue.WordRAM.RegisterCorrectness
+
+/-! Logical clients of the physical-array source proofs. Native prepared-body regressions
+are in `QueueRegisterMethods`; raw initialization and persistent dispatch are separate. -/
+
+@[expose] public section
+
+namespace ComplexityTests.QueueRegisterCorrectness
+
+open Cslib Cslib.WordRAM Cslib.WordRAM.Realization Cslib.DataStructure
+open Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
+
+/-- Two rear entries are stored in physical stack order in otherwise dirty memory. -/
+def rear : Memory.State := ⟨fun a => if a = 3 then 0 else if a = 4 then 7 else 5, 5⟩
+
+theorem rear_bounded : Memory.WellFormed 3 rear := by
+  refine ⟨by decide, fun a => ?_⟩
+  dsimp only [rear]
+  split <;> (try split) <;> decide
+
+-- Existing pairStep, not a separate FIFO specification, supplies the actual dequeue result.
+example :
+    (Memory.spec 0).clientResult rear (dequeue ![0, 2, 1, 2, 0]) = ((1, 0), some 0) ∧
+      Block.HoldsList 1 [7] ((Memory.spec 0).clientState rear
+        (dequeue ![0, 2, 1, 2, 0])).mem := by
+  have h := dequeue_contents (d := ![0, 2, 1, 2, 0]) [] [7, 0] rear
+    rear_bounded rfl rfl (by decide) (by decide) (Block.holdsList_nil _ _)
+    (by intro i; fin_cases i <;> rfl)
+  exact ⟨h.1, h.2.1⟩
+
+-- A nonempty front and a live rear are both retained correctly after the front pop.
+example :
+    (Memory.spec 0).clientResult rear (dequeue ![1, 1, 1, 2, 0]) = ((0, 1), some 5) ∧
+      Block.HoldsList 3 [0] ((Memory.spec 0).clientState rear
+        (dequeue ![1, 1, 1, 2, 0])).mem := by
+  have h := dequeue_contents (d := ![1, 1, 1, 2, 0]) [5] [0] rear
+    rear_bounded rfl rfl (by decide) (by decide)
+    (by intro i; fin_cases i; rfl) (by intro i; fin_cases i; rfl)
+  exact ⟨h.1, h.2.2⟩
+
+-- Enqueue preserves the existing front and extends the rear in physical stack order.
+example : Block.HoldsList 3 [0, 7]
+    ((Memory.spec 0).clientState ⟨fun _ => 0, 5⟩ (enqueue ![0, 1, 1, 2, 7])).mem := by
+  have h := enqueue_contents (d := ![0, 1, 1, 2, 7]) [] [0] ⟨fun _ => 0, 5⟩
+    rfl rfl (by decide) (Block.holdsList_nil _ _) (by intro i; fin_cases i; rfl)
+  exact h.2.2
+
+/-- A source client threads the returned count values, with no hidden memory count cells. -/
+def cycle (v : ℕ) : Memory.Prog (Option ℕ) := do
+  let m ← enqueue ![0, 0, 1, 1, v]
+  let r ← dequeue ![m.1, m.2, 1, 1, v]
+  pure r.2
+
+example : (Memory.spec 2).clientResult ⟨fun _ => 1, 3⟩ (cycle 3) = some 3 := rfl
+example : memoryCost (cycle 3) ⟨fun _ => 1, 3⟩ = 4 := rfl
+example : ((Memory.spec 2).clientState ⟨fun _ => 1, 3⟩ (cycle 3)).mem 4 = 1 := rfl
+
+-- Full and overflowing enqueues remain rejected; zero-capacity dequeue remains admitted.
+example : ¬ enqueueDomain 2 ![0, 1, 1, 1, 3] ⟨fun _ => 3, 3⟩ := by unfold enqueueDomain; decide
+example : ¬ enqueueDomain 2 ![0, 0, 1, 1, 4] ⟨fun _ => 3, 3⟩ := by unfold enqueueDomain; decide
+example : transferDomain 1 ![0, 0, 0, 0, 1] ⟨fun _ => 1, 0⟩ := by unfold transferDomain; decide
+
+end ComplexityTests.QueueRegisterCorrectness
diff --git a/ComplexityTests/QueueRegisterDynamic.lean b/ComplexityTests/QueueRegisterDynamic.lean
new file mode 100644
index 0000000000..8896b2b3dd
--- /dev/null
+++ b/ComplexityTests/QueueRegisterDynamic.lean
@@ -0,0 +1,83 @@
+/-
+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: local-only (test driver)
+
+public import Complexity.DataStructure.Queue.WordRAM.RegisterDynamic
+
+/-!
+The original adaptive FIFO client is consumed by the existing dynamic execution/resource
+interfaces. Raw dirty initialization, its six actual instructions, final potential and the
+free external-controller boundary are preserved. The native exchange factor is uniform;
+the old hand-written program's literal14/28 instruction claims are not reused.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.QueueRegisterDynamic
+
+open Cslib Cslib.WordRAM Cslib.WordRAM.Realization Cslib.DataStructure
+open Cslib.DataStructure.Queue.WordRAM
+
+/-- Enqueue two values, dequeue the first and reinsert that observed value before the final
+dequeue. The client never inspects either physical stack or its count words. -/
+def cycle {w capacity : ℕ} (a b : ℕ) :
+    (spec w capacity).Client (Option ℕ × Option ℕ) := do
+  let _ ← (spec w capacity).call (.enqueue a)
+  let _ ← (spec w capacity).call (.enqueue b)
+  let first ← (spec w capacity).call .dequeue
+  let _ ← (spec w capacity).call (.enqueue (first.getD 0))
+  let second ← (spec w capacity).call .dequeue
+  pure (first, second)
+
+theorem cycle_valid {w capacity a b : ℕ} (hc : 2 ≤ capacity)
+    (ha : Fits w a) (hb : Fits w b) :
+    (spec w capacity).ValidHistory [] ((spec w capacity).runClient [] (cycle a b)).2.2 := by
+  exact ⟨⟨by simpa using (show 0 < capacity by omega), ha⟩,
+    ⟨⟨by simpa using (show 1 < capacity by omega), hb⟩,
+    trivial, ⟨by simpa using (show 1 < capacity by omega), ha⟩, trivial, trivial⟩⟩
+
+example {w capacity a b : ℕ} : (spec w capacity).runClient [] (cycle a b) =
+    ((some a, some b), [a], [.enqueue a, .enqueue b, .dequeue, .enqueue a, .dequeue]) := rfl
+
+/-- All registers and all physical cells initially contain dirty maximum words. -/
+def stale : Data registers := ⟨fun _ => 15, fun _ => 15⟩
+
+theorem stale_bounded : stale.Bounded 4 :=
+  ⟨fun _ => (by decide : Fits 4 15), fun _ => (by decide : Fits 4 15)⟩
+
+/-- The five adaptive native calls retain the final queue and terminal rear credit. -/
+theorem adaptive_from_dirty : ∃ ready y traces,
+    Exec 4 (initializeCode 3 2) stale ready 6 ∧
+      DataStructure.Executes ((implementation 4 2).ExecOp 4)
+        (cycle 0 15) ready (some 0, some 15) y traces ∧
+      QueueRep 4 3 2 [0] y ∧
+      6 + DataStructure.total DynamicProgram.OperationTrace.instructions traces + potential y ≤
+        6 + 5 * (4 * Backend.factor family + 6) := by
+  exact run_initialized (w := 4) (base := 3) (capacity := 2)
+    (by decide) (by decide) (cycle 0 15) stale_bounded
+    (cycle_valid (by decide) (by decide) (by decide))
+
+-- No unused physical cell is cleared by the raw initializer.
+example : (initialized 3 2 stale).mem = stale.mem := rfl
+
+-- The original zero-capacity domain and dirty memory need no extra metadata cells.
+example {x : Data registers} (hx : x.Bounded 1) : ∃ ready y traces,
+    Exec 1 (initializeCode 0 0) x ready 6 ∧
+      DataStructure.Executes ((implementation 1 0).ExecOp 1)
+        ((spec 1 0).call .dequeue) ready none y traces ∧
+      QueueRep 1 0 0 [] y ∧
+      6 + DataStructure.total DynamicProgram.OperationTrace.instructions traces + potential y ≤
+        6 + (4 * Backend.factor family + 6) := by
+  have hrun : (spec 1 0).runClient [] ((spec 1 0).call .dequeue) =
+      (none, [], [Queue.QueueOp.dequeue]) := rfl
+  have h := run_initialized (w := 1) (base := 0) (capacity := 0)
+    (by decide) (by decide) ((spec 1 0).call .dequeue) hx ⟨trivial, trivial⟩
+  rw [hrun] at h
+  simpa only [List.length_singleton, Nat.one_mul] using h
+
+end ComplexityTests.QueueRegisterDynamic
diff --git a/ComplexityTests/QueueRegisterExecution.lean b/ComplexityTests/QueueRegisterExecution.lean
new file mode 100644
index 0000000000..88b7527614
--- /dev/null
+++ b/ComplexityTests/QueueRegisterExecution.lean
@@ -0,0 +1,106 @@
+/-
+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: local-only (test driver)
+
+public import Complexity.DataStructure.Queue.WordRAM.RegisterExecution
+
+/-!
+Actual fixed-dispatcher calls carry their count registers from one call to the next. External
+prepare delivers only tag/payload; no Backend.install or replacement metadata is used. The
+six-instruction initializer starts from dirty registers and preserves every memory cell.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.QueueRegisterExecution
+
+open Cslib.WordRAM Cslib.WordRAM.Realization
+open Cslib.DataStructure.Queue.WordRAM
+
+/-- Dirty entry registers, zero-valued physical and inaccessible memory. -/
+def rawTwo : Data registers := ⟨fun _ => 3, fun _ => 0⟩
+
+theorem rawTwo_bounded : rawTwo.Bounded 2 :=
+  ⟨fun _ => (by decide : Fits 2 3), fun _ => fits_zero 2⟩
+
+/-- At the old small-width boundary, one fixed program enqueues and dequeues every fitting
+value, with paid initialization, carried metadata, typed observation and an intact sentinel. -/
+theorem roundTrip_native (v : ℕ) (hv : Fits 2 v) :
+    ∃ ready y z n m, Exec 2 (initializeCode 1 1) rawTwo ready 6 ∧
+      Exec 2 program ((implementation 2 1).prepare (.enqueue v) ready) y n ∧
+      Exec 2 program ((implementation 2 1).prepare .dequeue y) z m ∧
+      (implementation 2 1).decode .dequeue z.regs = some (some v) ∧
+      QueueRep 2 1 1 [] z ∧ 6 + (n + 1) + (m + 1) ≤ 6 + (6 * Backend.factor family + 11) ∧
+      z.mem 4 = 0 := by
+  let ready := initialized 1 1 rawTwo
+  have hr : Rep 2 1 1 [] [] ready := initialized_rep rawTwo_bounded (by decide)
+  obtain ⟨y, n, he, hn, hry, hmy⟩ := execute_enqueue (by decide) hr (by decide) hv
+  obtain ⟨z, m, hd, hm, hrz, ha, hmz⟩ := execute_dequeue (by decide) hry
+  have hm' : m + 1 ≤ Backend.factor family * 4 + 6 := hm
+  have houtside : 4 ∉ (Block.mk 1 (2 * 1)).footprint := by decide
+  have hsentinel : z.mem 4 = 0 := (hmz 4 houtside).trans ((hmy 4 houtside).trans rfl)
+  refine ⟨ready, y, z, n, m, (initialize_exec rawTwo_bounded (by decide)).1,
+    he, hd, ha, ⟨[], [], rfl, hrz⟩, ?_, hsentinel⟩
+  omega
+
+-- Some-zero and the maximum word use the same program and persistent register file.
+example := roundTrip_native 0 (fits_zero 2)
+example := roundTrip_native 3 (by decide)
+
+/-- A larger old two-array region, with arbitrary dirty unused cells. -/
+def rawThree : Data registers := ⟨fun _ => 7, fun _ => 5⟩
+
+theorem rawThree_bounded : rawThree.Bounded 3 :=
+  ⟨fun _ => (by decide : Fits 3 7), fun _ => (by decide : Fits 3 5)⟩
+
+-- Five actual calls carry metadata through a two-iteration reversal, an immediate pop and
+-- the empty case. The values zero and maximum7 remain distinct from the empty observation.
+example : ∃ ready a b c d e n0 n1 n2 n3 n4,
+    Exec 3 (initializeCode 1 2) rawThree ready 6 ∧
+      Exec 3 program ((implementation 3 2).prepare (.enqueue 0) ready) a n0 ∧
+      Exec 3 program ((implementation 3 2).prepare (.enqueue 7) a) b n1 ∧
+      Exec 3 program ((implementation 3 2).prepare .dequeue b) c n2 ∧
+      Exec 3 program ((implementation 3 2).prepare .dequeue c) d n3 ∧
+      Exec 3 program ((implementation 3 2).prepare .dequeue d) e n4 ∧
+      (implementation 3 2).decode .dequeue c.regs = some (some 0) ∧
+      (implementation 3 2).decode .dequeue d.regs = some (some 7) ∧
+      (implementation 3 2).decode .dequeue e.regs = some none ∧ QueueRep 3 1 2 [] e := by
+  let ready := initialized 1 2 rawThree
+  have hr : Rep 3 1 2 [] [] ready := initialized_rep rawThree_bounded (by decide)
+  obtain ⟨a, n0, h0, _, hra, _⟩ := execute_enqueue (v := 0) (by decide) hr (by decide) (by decide)
+  obtain ⟨b, n1, h1, _, hrb, _⟩ := execute_enqueue (v := 7) (by decide) hra (by decide) (by decide)
+  obtain ⟨c, n2, h2, _, hrc, hc, _⟩ := execute_dequeue (by decide) hrb
+  obtain ⟨d, n3, h3, _, hrd, hd, _⟩ := execute_dequeue (by decide) hrc
+  obtain ⟨e, n4, h4, _, hre, he, _⟩ := execute_dequeue (by decide) hrd
+  exact ⟨ready, a, b, c, d, e, n0, n1, n2, n3, n4,
+    (initialize_exec rawThree_bounded (by decide)).1,
+    h0, h1, h2, h3, h4, hc, hd, he, ⟨[], [], rfl, hre⟩⟩
+
+/-- Capacity-zero entry is dirty in every register and every memory cell. -/
+def rawOne : Data registers := ⟨fun _ => 1, fun _ => 1⟩
+
+theorem rawOne_bounded : rawOne.Bounded 1 :=
+  ⟨fun _ => (by decide : Fits 1 1), fun _ => (by decide : Fits 1 1)⟩
+
+example : ∃ ready y n, Exec 1 (initializeCode 0 0) rawOne ready 6 ∧
+      Exec 1 program ((implementation 1 0).prepare .dequeue ready) y n ∧
+      n + 1 ≤ Backend.factor family + 6 ∧
+      (implementation 1 0).decode .dequeue y.regs = some none ∧
+      QueueRep 1 0 0 [] y ∧ y.mem = rawOne.mem := by
+  let ready := initialized 0 0 rawOne
+  have hr : Rep 1 0 0 [] [] ready := initialized_rep rawOne_bounded (by decide)
+  obtain ⟨y, n, he, hn, hry, ha, hm⟩ := execute_dequeue (by decide) hr
+  have hn' : n + 1 ≤ Backend.factor family + 6 := by
+    change n + 1 ≤ Backend.factor family * 1 + 6 at hn
+    simpa only [Nat.mul_one] using hn
+  refine ⟨ready, y, n, (initialize_exec rawOne_bounded (by decide)).1,
+    he, hn', ha, ⟨[], [], rfl, hry⟩, ?_⟩
+  funext a
+  exact hm a (by simp [footprint, Block.footprint])
+
+end ComplexityTests.QueueRegisterExecution
diff --git a/ComplexityTests/QueueRegisterMethods.lean b/ComplexityTests/QueueRegisterMethods.lean
new file mode 100644
index 0000000000..6101f17b43
--- /dev/null
+++ b/ComplexityTests/QueueRegisterMethods.lean
@@ -0,0 +1,129 @@
+/-
+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: local-only (test driver)
+
+public import Complexity.DataStructure.Queue.WordRAM.RegisterProgram
+
+/-!
+The production finite family is fixed before every runtime count, base, capacity, width and memory.
+These are prepared-body executions. A later fixed native dispatcher must pay for tag selection,
+metadata commit and the final halt; `Backend.install` is explicit here and is not a raw loader.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.QueueRegisterMethods
+
+open Cslib Cslib.WordRAM Cslib.WordRAM.Realization Cslib.DataStructure
+open Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
+open Cslib.DataStructure.Queue.WordRAM
+
+noncomputable def result (b : Bool) (i : Fin (family b).l) :
+    Fin (Backend.registers family) :=
+  Backend.tmp family b (Fin.castAdd ((family b).realizes.scratchSize + 1) i)
+
+/-- Enqueue's whole source memory and its two count words are realized by the fixed body. -/
+theorem native_enqueue {w : ℕ} {d : Input} {s : Memory.State}
+    (hw : Memory.WellFormed w s) (hwords : ∀ i, Fits w (d i))
+    (h : enqueueDomain w d s) :
+    ∃ y n, Exec w (Backend.code family false)
+        (Backend.install family false d (Backend.data family s)) y n ∧
+      n ≤ Backend.factor family * 2 ∧
+      y.mem = Function.update s.mem (d 2 + d 3 + d 1) (d 4) ∧
+      ∀ i, y.regs (result false i) = counts (d 0, d 1 + 1) i := by
+  obtain ⟨y, n, he, hn, hm, hout, _⟩ := Backend.exists_exec family false d
+    (Backend.bounded_data family hw) hwords
+    (by simpa only [Backend.memoryState_data] using h)
+    (by simpa only [Backend.memoryState_data] using valid_enqueue h)
+  rw [Backend.memoryState_data, memoryCost_enqueue] at hn
+  have hmem := congrArg Memory.State.mem hm
+  rw [Backend.memoryState_data, clientState_width w] at hmem
+  rw [Backend.memoryState_data, clientResult_width w] at hout
+  exact ⟨y, n, he, hn, hmem, hout⟩
+
+/-- The same dequeue body realizes empty, immediate and transferred option answers. -/
+theorem native_dequeue {w : ℕ} {d : Input} {s : Memory.State}
+    (hw : Memory.WellFormed w s) (hwords : ∀ i, Fits w (d i))
+    (h : transferDomain w d s) :
+    ∃ y n, Exec w (Backend.code family true)
+        (Backend.install family true d (Backend.data family s)) y n ∧
+      n ≤ Backend.factor family *
+        ((if d 0 = 0 then 2 * d 1 + (if d 1 = 0 then 0 else 1) else 1) + 1) ∧
+      y.mem = ((Memory.spec 0).clientState s (dequeue d)).mem ∧
+      ∀ i, y.regs (result true i) =
+        appendWords counts optionWords ((Memory.spec 0).clientResult s (dequeue d)) i := by
+  have hi := dequeue_invariant hw h
+  obtain ⟨y, n, he, hn, hm, hout, _⟩ := Backend.exists_exec family true d
+    (Backend.bounded_data family hw) hwords
+    (by simpa only [Backend.memoryState_data] using h)
+    (by simpa only [Backend.memoryState_data] using hi.1)
+  rw [Backend.memoryState_data, hi.2.2.2.2.1] at hn
+  have hmem := congrArg Memory.State.mem hm
+  rw [Backend.memoryState_data, clientState_width w] at hmem
+  rw [Backend.memoryState_data, clientResult_width w] at hout
+  exact ⟨y, n, he, hn, hmem, hout⟩
+
+-- The old decisive small-width domain admits a maximum-word enqueue with only two cells.
+example : ∃ y n, Exec 2 (Backend.code family false)
+      (Backend.install family false ![0, 0, 1, 1, 3]
+        (Backend.data family ⟨fun _ => 1, 3⟩)) y n ∧
+    n ≤ Backend.factor family * 2 ∧ y.mem 2 = 3 ∧ y.mem 4 = 1 ∧
+      y.regs (result false 0) = 0 ∧ y.regs (result false 1) = 1 := by
+  obtain ⟨y, n, he, hn, hm, ho⟩ := native_enqueue (w := 2)
+    (d := ![0, 0, 1, 1, 3]) (s := ⟨fun _ => 1, 3⟩)
+    ⟨by decide, fun _ => (by decide : Fits 2 1)⟩ (fun i => by fin_cases i <;> decide)
+    (by change 0 + 0 < 1 ∧ 1 + 2 * 1 ≤ 3 ∧ Fits 2 3; decide)
+  exact ⟨y, n, he, hn, hm ▸ rfl, hm ▸ rfl, ho 0, ho 1⟩
+
+/-- A dirty two-element rear contains zero and the maximum three-bit word. -/
+def dirty : Memory.State := ⟨fun a => if a = 3 then 0 else if a = 4 then 7 else 5, 5⟩
+
+theorem dirty_bounded : Memory.WellFormed 3 dirty := by
+  refine ⟨by decide, fun a => ?_⟩
+  dsimp only [dirty]
+  split <;> (try split) <;> decide
+
+-- The actual fallback returns the oldest value zero, with a separate present tag.
+example : ∃ y n, Exec 3 (Backend.code family true)
+      (Backend.install family true ![0, 2, 1, 2, 7]
+        (Backend.data family dirty)) y n ∧
+    n ≤ Backend.factor family * 6 ∧ y.mem 6 = 5 ∧
+      y.regs (result true 0) = 1 ∧ y.regs (result true 1) = 0 ∧
+      y.regs (result true 2) = 1 ∧ y.regs (result true 3) = 0 := by
+  obtain ⟨y, n, he, hn, hm, ho⟩ := native_dequeue (d := ![0, 2, 1, 2, 7])
+    dirty_bounded (fun i => by fin_cases i <;> decide)
+    (by change 0 + 2 ≤ 2 ∧ 1 + 2 * 2 ≤ 5; decide)
+  exact ⟨y, n, he, hn, hm ▸ rfl, ho 0, ho 1, ho 2, ho 3⟩
+
+-- A nonempty front returns a maximum word without touching any memory cell.
+example : ∃ y n, Exec 2 (Backend.code family true)
+      (Backend.install family true ![1, 0, 1, 1, 0]
+        (Backend.data family ⟨fun _ => 3, 3⟩)) y n ∧
+    n ≤ Backend.factor family * 2 ∧ y.mem = (fun _ => 3) ∧
+      y.regs (result true 0) = 0 ∧ y.regs (result true 1) = 0 ∧
+      y.regs (result true 2) = 1 ∧ y.regs (result true 3) = 3 := by
+  obtain ⟨y, n, he, hn, hm, ho⟩ := native_dequeue (w := 2)
+    (d := ![1, 0, 1, 1, 0]) (s := ⟨fun _ => 3, 3⟩)
+    ⟨by decide, fun _ => (by decide : Fits 2 3)⟩ (fun i => by fin_cases i <;> decide)
+    (by change 1 + 0 ≤ 1 ∧ 1 + 2 * 1 ≤ 3; decide)
+  exact ⟨y, n, he, hn, hm, ho 0, ho 1, ho 2, ho 3⟩
+
+-- The same dequeue body handles capacity zero on arbitrary dirty bounded memory.
+example : ∃ y n, Exec 1 (Backend.code family true)
+      (Backend.install family true ![0, 0, 0, 0, 1]
+        (Backend.data family ⟨fun _ => 1, 0⟩)) y n ∧
+    n ≤ Backend.factor family ∧ y.mem = (fun _ => 1) ∧
+      y.regs (result true 0) = 0 ∧ y.regs (result true 1) = 0 ∧
+      y.regs (result true 2) = 0 ∧ y.regs (result true 3) = 0 := by
+  obtain ⟨y, n, he, hn, hm, ho⟩ := native_dequeue (w := 1)
+    (d := ![0, 0, 0, 0, 1]) (s := ⟨fun _ => 1, 0⟩)
+    ⟨by decide, fun _ => (by decide : Fits 1 1)⟩ (fun i => by fin_cases i <;> decide)
+    (by change 0 + 0 ≤ 0 ∧ 0 + 2 * 0 ≤ 0; decide)
+  exact ⟨y, n, he, by simpa using hn, hm, ho 0, ho 1, ho 2, ho 3⟩
+
+end ComplexityTests.QueueRegisterMethods
diff --git a/ComplexityTests/QueueRegisterProgram.lean b/ComplexityTests/QueueRegisterProgram.lean
new file mode 100644
index 0000000000..adc30b493c
--- /dev/null
+++ b/ComplexityTests/QueueRegisterProgram.lean
@@ -0,0 +1,44 @@
+/-
+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: local-only (test driver)
+
+public import Complexity.DataStructure.Queue.WordRAM.RegisterProgram
+
+/-! Paid raw setup in the same globally chosen register file as both method bodies. These
+checks establish six actual writes and literal dirty-memory preservation; the full initialized
+representation and persistent dispatcher certificate remain separate proof obligations. -/
+
+@[expose] public section
+
+namespace ComplexityTests.QueueRegisterProgram
+
+open Cslib.WordRAM
+open Cslib.DataStructure.Queue.WordRAM
+
+/-- Every entry register and cell starts dirty, including the frontier and count words. -/
+def rawTwo : Data registers := ⟨fun _ => 3, fun _ => 3⟩
+
+theorem rawTwo_bounded : rawTwo.Bounded 2 :=
+  ⟨fun _ => (by decide : Fits 2 3), fun _ => (by decide : Fits 2 3)⟩
+
+-- The decisive old width2/base1/C1 domain, with no two extra count cells.
+example : ∃ y, Exec 2 (initializeCode 1 1) rawTwo y 6 ∧ y.Bounded 2 ∧
+    y.mem = rawTwo.mem := by
+  exact ⟨initialized 1 1 rawTwo, initialize_exec rawTwo_bounded (by decide)⟩
+
+/-- Capacity zero still starts from arbitrary dirty bounded memory. -/
+def rawOne : Data registers := ⟨fun _ => 1, fun _ => 1⟩
+
+theorem rawOne_bounded : rawOne.Bounded 1 :=
+  ⟨fun _ => (by decide : Fits 1 1), fun _ => (by decide : Fits 1 1)⟩
+
+example : ∃ y, Exec 1 (initializeCode 0 0) rawOne y 6 ∧ y.Bounded 1 ∧
+    y.mem = rawOne.mem := by
+  exact ⟨initialized 0 0 rawOne, initialize_exec rawOne_bounded (by decide)⟩
+
+end ComplexityTests.QueueRegisterProgram
diff --git a/ComplexityTests/QueueRegisterTransfer.lean b/ComplexityTests/QueueRegisterTransfer.lean
new file mode 100644
index 0000000000..cf2a3c86a2
--- /dev/null
+++ b/ComplexityTests/QueueRegisterTransfer.lean
@@ -0,0 +1,112 @@
+/-
+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: local-only (test driver)
+
+public import Complexity.DataStructure.Queue.WordRAM.RegisterTransfer
+public import Complexity.Computability.WordRAM.Realization.Backend
+
+/-!
+One standard-basis body serves all prepared transfer inputs below. Argument installation is
+explicit in the entry state; these are body executions, not an uncharged raw initializer or a
+stateful `Backend.implementation`. The separate metadata feasibility test pays its initializer.
+-/
+
+@[expose] public section
+
+namespace ComplexityTests.QueueRegisterTransfer
+
+open Cslib Cslib.WordRAM Cslib.WordRAM.Realization Cslib.DataStructure
+
+open Cslib.DataStructure.Queue.WordRAM.RegisterMetadata
+
+/-- The same globally fixed certificate family is used by every width/layout/value case. -/
+noncomputable abbrev certificates (_ : Unit) : Certificate .standard := ⟨realizes_transfer_standard⟩
+
+noncomputable def result (i : Fin 2) : Fin (Backend.registers certificates) :=
+  Backend.tmp certificates () (Fin.castAdd ((certificates ()).realizes.scratchSize + 1) i)
+
+theorem native_body {w : ℕ} {d : Input} {s : Memory.State}
+    (hw : Memory.WellFormed w s) (hwords : ∀ i, Fits w (d i))
+    (h : transferDomain w d s) :
+    ∃ y n, Exec w (Backend.code certificates ())
+        (Backend.install certificates () d (Backend.data certificates s)) y n ∧
+      n ≤ Backend.factor certificates * (2 * d 1 + 1) ∧
+      y.mem = ((Memory.spec w).clientState s (transfer d)).mem ∧
+      y.regs (result 0) = d 0 + d 1 ∧ y.regs (result 1) = 0 := by
+  have hi := transfer_invariant hw h
+  obtain ⟨y, n, he, hn, hm, hout, _⟩ := Backend.exists_exec certificates () d
+    (Backend.bounded_data certificates hw) hwords
+    (by simpa only [Backend.memoryState_data] using h)
+    (by simpa only [Backend.memoryState_data] using hi.1)
+  have hcost := hi.2.2.2.2.1
+  change memoryCost (transfer d) s = 2 * d 1 at hcost
+  have hresult : (Memory.spec w).clientResult s (transfer d) = (d 0 + d 1, 0) :=
+    (clientResult_width w _ _).trans hi.2.2.1
+  have h0 := hout (0 : Fin 2)
+  have h1 := hout (1 : Fin 2)
+  rw [Backend.memoryState_data, hresult] at h0 h1
+  rw [Backend.memoryState_data, hcost] at hn
+  have hmem := congrArg Memory.State.mem hm
+  rw [Backend.memoryState_data] at hmem
+  exact ⟨y, n, he, hn, hmem, h0, h1⟩
+
+/-- Two iterations move a zero and the largest three-bit word through dirty physical arrays. -/
+def two : Input := ![0, 2, 1, 2, 7]
+
+def dirty : Memory.State := ⟨fun a => if a = 3 then 7 else if a = 4 then 0 else 5, 5⟩
+
+theorem dirty_bounded : Memory.WellFormed 3 dirty := by
+  refine ⟨by decide, fun a => ?_⟩
+  dsimp only [dirty]
+  split <;> (try split) <;> decide
+
+example : (Memory.spec 3).clientResult dirty (transfer two) = (2, 0) := rfl
+example : memoryCost (transfer two) dirty = 4 := rfl
+example : let t := (Memory.spec 3).clientState dirty (transfer two)
+    t.mem 1 = 0 ∧ t.mem 2 = 7 ∧ t.mem 3 = 7 ∧ t.mem 4 = 0 ∧ t.mem 6 = 5 :=
+  ⟨rfl, rfl, rfl, rfl, rfl⟩
+
+example : Block.HoldsList 1 [0, 7]
+    ((Memory.spec 3).clientState dirty (transfer two)).mem := by
+  rw [clientState_width 3]
+  exact transfer_contents (d := two) [0, 7] [] dirty rfl rfl (by decide)
+    (fun i => Fin.elim0 i) (by intro i; fin_cases i <;> rfl)
+
+example : ∃ y n, Exec 3 (Backend.code certificates ())
+      (Backend.install certificates () two (Backend.data certificates dirty)) y n ∧
+    n ≤ Backend.factor certificates * 5 ∧ y.mem 1 = 0 ∧ y.mem 2 = 7 ∧
+      y.mem 6 = 5 ∧ y.regs (result 0) = 2 ∧ y.regs (result 1) = 0 := by
+  obtain ⟨y, n, he, hn, hm, h0, h1⟩ := native_body (d := two) dirty_bounded
+    (fun i => by fin_cases i <;> decide) (by change 0 + 2 ≤ 2 ∧ 1 + 2 * 2 ≤ 5; decide)
+  refine ⟨y, n, he, hn, ?_, ?_, ?_, h0, h1⟩ <;> rw [hm] <;> rfl
+
+-- The original small-width domain: base1/C1 fits without two extra count cells.
+example : ∃ y n, Exec 2 (Backend.code certificates ())
+      (Backend.install certificates () ![0, 1, 1, 1, 3]
+        (Backend.data certificates ⟨fun _ => 3, 3⟩)) y n ∧
+    n ≤ Backend.factor certificates * 3 ∧ y.regs (result 0) = 1 ∧
+      y.regs (result 1) = 0 := by
+  obtain ⟨y, n, he, hn, _, h0, h1⟩ := native_body (w := 2)
+    (d := ![0, 1, 1, 1, 3]) (s := ⟨fun _ => 3, 3⟩)
+    ⟨by decide, fun _ => (by decide : Fits 2 3)⟩ (fun i => by fin_cases i <;> decide)
+    (by change 0 + 1 ≤ 1 ∧ 1 + 2 * 1 ≤ 3; decide)
+  exact ⟨y, n, he, hn, h0, h1⟩
+
+-- The same body exits with zero capacity, keeping every dirty memory cell.
+example : ∃ y n, Exec 1 (Backend.code certificates ())
+      (Backend.install certificates () ![0, 0, 0, 0, 1]
+        (Backend.data certificates ⟨fun _ => 1, 0⟩)) y n ∧
+    n ≤ Backend.factor certificates ∧ y.mem = (fun _ => 1) ∧
+      y.regs (result 0) = 0 ∧ y.regs (result 1) = 0 := by
+  obtain ⟨y, n, he, hn, hm, h0, h1⟩ := native_body (w := 1)
+    (d := ![0, 0, 0, 0, 1]) (s := ⟨fun _ => 1, 0⟩)
+    ⟨by decide, fun _ => (by decide : Fits 1 1)⟩ (fun i => by fin_cases i <;> decide)
+    (by change 0 + 0 ≤ 0 ∧ 0 + 2 * 0 ≤ 0; decide)
+  exact ⟨y, n, he, by simpa using hn, hm, h0, h1⟩
+
+end ComplexityTests.QueueRegisterTransfer
diff --git a/ComplexityTests/WordRAMQueue.lean b/ComplexityTests/WordRAMQueue.lean
index 0662003f72..28e1760459 100644
--- a/ComplexityTests/WordRAMQueue.lean
+++ b/ComplexityTests/WordRAMQueue.lean
@@ -7,7 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: local-only (test driver)
 
-public import Complexity.DataStructure.Queue.WordRAM.Dynamic
+public import Complexity.DataStructure.Queue.WordRAM.RegisterDynamic
 
 /-!
 # A worked adaptive FIFO example
@@ -20,7 +20,7 @@ a nonempty-front dequeue, and an enqueue while both stack regions contain live v
 
 @[expose] public section
 
-open Cslib Cslib.WordRAM
+open Cslib Cslib.WordRAM Cslib.WordRAM.Realization
 open Cslib.DataStructure Cslib.DataStructure.Queue
 
 namespace WordRAMQueueTest
@@ -47,15 +47,16 @@ theorem cycle_valid {w capacity a b : ℕ} (hc : 2 ≤ capacity) (ha : Fits w a)
 
 /-- The backend-independent FIFO trace becomes actual queue-operation executions. -/
 example {w base capacity a b : ℕ} (h1 : Fits w 1)
-    (hc : Fits w (base + 2 * capacity)) (hsize : 2 ≤ capacity)
-    (ha : Fits w a) (hb : Fits w b) {x : Data 11}
+    (hsize : 2 ≤ capacity)
+    (ha : Fits w a) (hb : Fits w b) {x : Data Queue.WordRAM.registers}
     (hr : Queue.WordRAM.QueueRep w base capacity [] x) :
     ∃ y traces,
       DataStructure.Executes ((Queue.WordRAM.implementation w capacity).ExecOp w)
         (cycle a b) x (some a, some b) y traces ∧
       Queue.WordRAM.QueueRep w base capacity [a] y ∧
       DataStructure.total DynamicProgram.OperationTrace.instructions traces +
-        Queue.WordRAM.potential y ≤ 70 + Queue.WordRAM.potential x := by
+        Queue.WordRAM.potential y ≤
+          5 * (4 * Backend.factor Queue.WordRAM.family + 6) + Queue.WordRAM.potential x := by
   have hv : (Queue.WordRAM.spec w capacity).ValidHistory []
       ((Queue.WordRAM.spec w capacity).runClient [] (cycle a b)).2.2 :=
     ⟨⟨by simpa using (show 0 < capacity by omega), ha⟩,
@@ -66,17 +67,19 @@ example {w base capacity a b : ℕ} (h1 : Fits w 1)
     Queue.WordRAM.spec, queue,
     List.nil_append, List.cons_append, List.tail_cons, List.head?_cons,
     Option.getD_some, List.length_cons, List.length_nil] using
-    Queue.WordRAM.run_client h1 hc (cycle a b) hr hv
+    Queue.WordRAM.run_client h1 (cycle a b) hr hv
 
 -- Nonzero unused memory is legitimate: only live prefixes carry queue contents.
-private def stale : Data 11 := ⟨fun _ => 15, fun _ => 15⟩
+private def stale : Data Queue.WordRAM.registers := ⟨fun _ => 15, fun _ => 15⟩
 
 private theorem stale_bounded : stale.Bounded 4 :=
   ⟨fun _ => (by decide : Fits 4 15), fun _ => (by decide : Fits 4 15)⟩
 
 example : ∃ ready, Exec 4 (Queue.WordRAM.initializeCode 3 2) stale ready 6 ∧
     Queue.WordRAM.Rep 4 3 2 [] [] ready ∧ ready.mem = stale.mem :=
-  Queue.WordRAM.initialize_exec stale_bounded (by decide) (by decide)
+  ⟨Queue.WordRAM.initialized 3 2 stale,
+    (Queue.WordRAM.initialize_exec stale_bounded (by decide)).1,
+    Queue.WordRAM.initialized_rep stale_bounded (by decide), rfl⟩
 
 -- All five adaptive calls work from an initialized representation, including a zero word.
 example : ∃ ready y traces, Exec 4 (Queue.WordRAM.initializeCode 3 2) stale ready 6 ∧
@@ -84,8 +87,10 @@ example : ∃ ready y traces, Exec 4 (Queue.WordRAM.initializeCode 3 2) stale re
       (cycle 0 15) ready (some 0, some 15) y traces ∧
     Queue.WordRAM.QueueRep 4 3 2 [0] y ∧
     6 + DataStructure.total DynamicProgram.OperationTrace.instructions traces +
-      Queue.WordRAM.potential y ≤ 76 := by
-  exact Queue.WordRAM.run_initialized (by decide) (by decide) (cycle 0 15)
+      Queue.WordRAM.potential y ≤
+        6 + 5 * (4 * Backend.factor Queue.WordRAM.family + 6) := by
+  exact Queue.WordRAM.run_initialized (w := 4) (base := 3) (capacity := 2)
+    (by decide) (by decide) (cycle 0 15)
     stale_bounded (cycle_valid (by decide) (by decide) (by decide))
 
 -- Capacity zero allows an empty dequeue, but no enqueue (even of zero), and capacity/width bounds
@@ -97,14 +102,18 @@ example :
     ¬(Queue.WordRAM.spec 4 2).valid [] (.enqueue 16) :=
   ⟨by decide, trivial, by decide, by decide⟩
 
--- A refill of two rear words costs 28 including halt: a false 27 bound is rejected.
-example {x y : Data 11} {a : Option ℕ} {trace : DynamicProgram.OperationTrace}
+-- The realized program has one uniform factor rather than the removed hand-code's exact28
+-- refill clock. Its actual trace still pays control, commit and halt with terminal credit.
+example {x y : Data Queue.WordRAM.registers} {a : Option ℕ}
+    {trace : DynamicProgram.OperationTrace}
     (hr : Queue.WordRAM.Rep 4 3 2 [] [15, 0] x)
     (he : (Queue.WordRAM.implementation 4 2).ExecOp 4 x .dequeue a y trace) :
-    trace.instructions = 28 ∧ ¬trace.instructions ≤ 27 := by
-  have h := Queue.WordRAM.instructions_eq (by decide) hr trivial he
-  change trace.instructions = 28 at h
-  omega
+    trace.instructions + Queue.WordRAM.potential y ≤
+      4 * Backend.factor Queue.WordRAM.family + 6 + Queue.WordRAM.potential x := by
+  obtain ⟨z, n, hz, _, _, _, hp⟩ := Queue.WordRAM.execute (by decide) hr .dequeue trivial
+  obtain ⟨rfl, hn⟩ := he.eq_of_exec hz
+  rw [hn]
+  exact hp
 
 -- Empty and zero-valued observations are semantically distinct, and the footprint size is `2 * c`.
 example :
diff --git a/ROADMAP.md b/ROADMAP.md
index 3893700ec0..5074aa693c 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -653,8 +653,12 @@ reusing graph and matroid foundations and the shared data-structure interfaces.
   remains only as the stepped component of Chan–He traversal (`Traversal.WordStack`). Backends of
   framed refinements export their frame (`modifies`, `frame`), run products over one memory,
   and allocate from arbitrary memory through `Memory.Allocator` (`Backend.Allocation`); the stack
-  and a pair of stacks check all three. Remaining: the queue and binary-heap migrations onto them,
-  and the full C2/M1b objective; arbitrary host continuations do not acquire runtime bounds.
+  and a pair of stacks check all three. Queue operation calls now use one fixed native
+  dispatcher over physical-array memory programs, with resident count words and paid commits.
+  Its dynamic certificate preserves the original two-array space, dirty six-instruction
+  initialization and adaptive-call bounds. Remaining are the binary-heap migration, the full
+  framed queue/faithful-allocation client and generic stateful composition, and the full C2/M1b
+  objective; 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
   allocation and deallocation, shrinking, and live and peak space accounting; ownership and
diff --git a/UPSTREAM.md b/UPSTREAM.md
index 02705160b6..c74d4a36b1 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -570,10 +570,15 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   a balanced tree or machine-time certificate.
   `WordRAM/Dynamic` separately connects
   fixed bounded-word operation programs and faithful memory transcripts to those contracts.
-  The direct shared-heap queue uses the existing FIFO operation signature and native operation
-  traces, with a hidden two-stack representation, a concrete-register potential, framed storage,
-  and separately charged initialization. Its `2 * capacity` reservation is explicit; external
-  client computation and argument delivery are not charged by the operation-history bound.
+  The direct shared-heap queue realizes physical-array memory programs through one fixed
+  finite Backend family and the existing dynamic certificate. Count words remain in registers;
+  one native dispatcher, charged metadata copies and a scaled rear potential give uniform
+  amortized instruction bounds, including halt. Initialization uses six register instructions
+  from arbitrary bounded dirty data, preserving every memory cell. The original `2 * capacity`
+  reservation and end-fit domain are retained. The shared register count and exchange factor are
+  fixed before widths, layouts, values and clients; the removed hand-code's literal instruction
+  constants are not asserted. External client computation and tag/payload delivery remain outside
+  the operation-history bound; no generic stateful memory-only Backend instance is claimed.
   Coordinate placement and overlap with Srinivas's #685 and the merged #401 (`Algorithms/Lean/Query`)
   before upstream submission; #685 is not copied here. This is a prototype of composition and
   refinement, not a replacement for their query models or a general cell-probe lower-bound semantics.