diff --git a/Complexity.lean b/Complexity.lean
index 899bc48751..9a3cb449d4 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -3065,6 +3065,7 @@ public import Complexity.DataStructure.StateTransition.Composition
 public import Complexity.DataStructure.StateTransition.CostHoare
 public import Complexity.DataStructure.StateTransition.Hoare
 public import Complexity.DataStructure.StateTransition.Impl
+public import Complexity.DataStructure.StateTransition.LinkCongr
 public import Complexity.DataStructure.StateTransition.Module
 public import Complexity.DataStructure.StateTransition.Oracle
 public import Complexity.DataStructure.StateTransition.Randomized
diff --git a/Complexity/DataStructure/StateTransition/LinkCongr.lean b/Complexity/DataStructure/StateTransition/LinkCongr.lean
new file mode 100644
index 0000000000..fb858875d6
--- /dev/null
+++ b/Complexity/DataStructure/StateTransition/LinkCongr.lean
@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.DataStructure.StateTransition.Module
+
+/-!
+# Linking methods with identical complete runs
+
+Changing a method's source syntax preserves a linked adaptive client when every method keeps
+its complete deterministic run: result, final state and lower-operation history. Equality of
+answers alone would not preserve the reached memories or the subsequent client behavior.
+
+## Main results
+
+* `StateTransitionSpec.runClient_link_congr`: equality of complete method runs lifts to every
+  adaptive client, retaining the entire lower-operation history and final state.
+
+This is a semantic transport result. It assigns no native cost to calling or argument staging;
+equal histories can be used with the existing `totalCost` function at any chosen charge.
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.StateTransitionSpec
+
+universe u v w
+
+variable {D E : StateTransitionSpec.{u, v, w}}
+  {f : (s : E.State) → (o : E.Op) → E.State × E.Result o} [E.HasStepFn f]
+  {α : Type w}
+
+/-- Methods with identical complete deterministic runs can replace one another under linking.
+The equality retains the lower history, including operations of every reached continuation. -/
+theorem runClient_link_congr (methods methods' : Methods D E)
+    (hmethods : ∀ s o, E.runClient s (methods o) = E.runClient s (methods' o))
+    (p : D.Client α) (s : E.State) :
+    E.runClient s (link methods p) = E.runClient s (link methods' p) := by
+  induction p generalizing s with
+  | pure a => rfl
+  | liftBind o k ih =>
+    change E.runClient s ((methods o).bind fun a => link methods (k a)) =
+      E.runClient s ((methods' o).bind fun a => link methods' (k a))
+    rw [E.runClient_bind, E.runClient_bind, hmethods s o]
+    exact congrArg (fun r : α × E.State × List E.Op =>
+      (r.1, r.2.1, (E.runClient s (methods' o)).2.2 ++ r.2.2))
+      (ih (E.runClient s (methods' o)).1 (E.runClient s (methods' o)).2.1)
+
+end Cslib.DataStructure.StateTransitionSpec
diff --git a/Complexity/Tactic/Realize.lean b/Complexity/Tactic/Realize.lean
index 62d022dd23..8ba3720907 100644
--- a/Complexity/Tactic/Realize.lean
+++ b/Complexity/Tactic/Realize.lean
@@ -8,10 +8,14 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.WordRAM.Realization.WhileAbsorb
+public import Complexity.Computability.WordRAM.Realization.Reindex
 
 /-!
 # The `realize` tactic
 
+The tactic is available inside `Cslib.WordRAM`, or after `open Cslib.WordRAM` or
+`open scoped Cslib.WordRAM`. Importing this module alone does not activate its syntax.
+
 `realize` proves a goal `Realizes B p input output safe work` for a memory client `p`. It walks
 the client syntax, unfolding definitions, with one rule per form:
 
@@ -21,6 +25,8 @@ the client syntax, unfolding definitions, with one rule per form:
   from the closure rules of `Complexity.Computability.WordRAM.Glue`: projections, constants, and
   the exact- or standard-basis arithmetic and bitwise operations.
 * the four memory queries: `Realizes.read`, `write`, `alloc` and `allocDirty`.
+* a method with a local zero-work `Realizes` certificate: `Realizes.reindex`, selecting its
+  arguments from live words before unfolding its implementation.
 * `if` on `a = b`, `a < b` or `a > b`: `Realizes.branch₀`.
 * `match` on an optional word or word pair: the client equals the branch on its presence tag
   (`Realizes.congr`, proved by cases).
@@ -53,7 +59,10 @@ updated memories, or the interpreter's result of a called method; a loop contrib
 After the composition, `realize` introduces `w d s hwords hmem h`: the word width, the
 environment, the memory, the fit of the input words, memory well-formedness, and the goal's
 domain. It splits the conjunctions and `if`s of the synthesized domain and leaves each remaining
-condition as a goal. There is no search: an unsupported form is reported with its subterm.
+condition as a goal. Local method certificates are tried in context order; the remaining rule
+selection follows the client syntax, without searching for bounds. An unsupported form is
+reported with its subterm. A called method's arguments must already be live words; computed
+arguments need an explicit `pure` step, whose glue is certified and charged as usual.
 
 Each certificate is stated for the client form as written, with its domain in the client's terms
 (`certify`), so certificates compose syntactically. A bind's continuation domain is stated at the
@@ -719,6 +728,73 @@ private def bindRun (hP hQ reply next : Expr) : MetaM Expr := do
     lambdaBoundedTelescope f 2 fun xs b => do mkLambdaFVars xs (← mkEqRefl b)
   mkAppM ``Realizes.bind₀_of_run #[hP, hQ, reply, next, ← refl reply, ← refl next]
 
+/-- Expose pair projections to unification when a certificate packages curried arguments.
+Other types remain whole metavariables: no data constructor or runtime value is guessed. -/
+private partial def callArgument (ty : Expr) : MetaM Expr := do
+  let ty ← whnfR ty
+  if let some (a, b) := ty.app2? ``Prod then
+    return mkAppN (mkConst ``Prod.mk ty.getAppFn.constLevels!)
+      #[a, b, ← callArgument a, ← callArgument b]
+  if let some (a, b) := ty.app2? ``Sigma then
+    let x ← callArgument a
+    return mkAppN (mkConst ``Sigma.mk ty.getAppFn.constLevels!)
+      #[a, b, x, ← callArgument (b.beta #[x])]
+  mkFreshExprMVar ty
+
+/-- Reuse a local method certificate before unfolding its body. Every input word must already
+be live: `Realizes.reindex` supplies static wiring, without granting argument computation. -/
+private def tryRealizeCall (ctx : Ctx) (env : Env) (d : Expr) (atoms : Array Expr)
+    (body : Expr) (output? : Option Expr) : TermElabM (Option Out) := do
+  for decl in ← getLCtx do
+    if decl.isImplementationDetail then continue
+    let ty ← instantiateMVars decl.type
+    unless ty.isAppOfArity ``Realizes 10 do continue
+    let saved ← saveState
+    try
+      let args := ty.getAppArgs
+      unless ← withReducible (isDefEq args[4]! ctx.basis) do
+        throwError "realize: the method's basis differs"
+      unless ← withReducible (isDefEq args[9]! (← zeroWork args[2]!)) do
+        throwError "realize: a called certificate must have absorbed local work"
+      let arg ← callArgument args[2]!
+      let called := (mkApp args[5]! arg).headBeta
+      -- Solve dependent arguments in binder order without unfolding a matching method head.
+      let matched ← if called.getAppFn == body.getAppFn &&
+          called.getAppNumArgs == body.getAppNumArgs then
+          (called.getAppArgs.zip body.getAppArgs).allM fun (a, b) => do
+            withReducible (isDefEq (← whnfR a) (← whnfR b))
+        else withReducible (isDefEq called body)
+      unless matched do
+        throwError "realize: the method does not match"
+      let arg ← instantiateMVars arg
+      if arg.hasMVar then throwError "realize: the method argument is undetermined"
+      let out ← checkOutput decl.toExpr output?
+      let k ← encodingWidth args[6]!
+      let coords ← encodingAtoms args[6]! arg k
+      let positions ← coords.mapM fun a => do
+        let some i ← findAtom atoms a
+          | throwError "realize: a method argument must first be computed into a live word"
+        pure i
+      let finK := mkApp (mkConst ``Fin) (mkNatLit k)
+      let finEnv := mkApp (mkConst ``Fin) (mkNatLit env.k)
+      let rec indices : List Nat → MetaM Expr
+        | [] => mkAppOptM ``Matrix.vecEmpty #[finEnv]
+        | i :: is => do mkAppM ``Matrix.vecCons #[← finLit env.k i, ← indices is]
+      let ix ← indices positions.toList
+      let f ← mkLambdaFVars #[d] arg
+      let hwTy ← withLocalDeclD `e env.ty fun e => withLocalDeclD `i finK fun i => do
+        let lhs := mkApp (← mkAppM ``DFunLike.coe #[args[6]!, f.beta #[e]]) i
+        let rhs := mkApp (← mkAppM ``DFunLike.coe #[env.input, e]) (mkApp ix i)
+        mkForallFVars #[e, i] (← mkEq lhs rhs)
+      let hw ← proveResult hwTy k
+      let proof ← mkAppM ``Realizes.reindex #[decl.toExpr, f, env.input, ix, hw]
+      let safe ← withLocalDeclD `w (mkConst ``Nat) fun w =>
+        withLocalDeclD `s (mkConst ``Memory.State) fun s => do
+          mkLambdaFVars #[w, d, s] (← reducePairs (mkApp3 args[8]! w arg s))
+      return some { proof, output := out, safe }
+    catch _ => saved.restore
+  return none
+
 mutual
 
 /-- Certify a client `prog : δ → Memory.Prog α` in the environment `env`. -/
@@ -726,6 +802,8 @@ private partial def realizeProg (ctx : Ctx) (env : Env) (prog : Expr) (output? :
     TermElabM Out :=
   withLocalDeclD `d env.ty fun d => do
     let atoms := env.atoms.map (·.beta #[d])
+    if let some out ← tryRealizeCall ctx env d atoms (prog.beta #[d]).headBeta output? then
+      return { out with proof := ← certify ctx env out.proof prog out.output out.safe }
     let body ← normBody (prog.beta #[d]).headBeta
     let out ← realizeBody ctx env d atoms body output?
     return { out with proof := ← certify ctx env out.proof prog out.output out.safe }
@@ -1113,10 +1191,12 @@ private partial def splitDomain (g : MVarId) : MetaM (List MVarId) := g.withCont
 
 end Cslib.Tactic.Realize
 
+namespace Cslib.WordRAM
+
 open Lean Meta Elab Tactic Cslib.WordRAM Cslib.WordRAM.Realization Cslib.Tactic.Realize in
 /-- Prove `Realizes B p input output safe work` for a memory client `p`, leaving the genuine fit
 and domain conditions as goals in the context `w d s hwords hmem h`. -/
-elab "realize" : tactic => withMainContext do
+scoped elab "realize" : tactic => withMainContext do
   let goal ← getMainGoal
   let target ← instantiateMVars (← whnfR (← goal.getType))
   unless target.isAppOfArity ``Realizes 10 do
@@ -1163,3 +1243,5 @@ elab "realize" : tactic => withMainContext do
     | some g' => g.assign (mkMVar g')
     | none => kept := kept.push g
   setGoals kept.toList
+
+end Cslib.WordRAM
diff --git a/ComplexityTests/StateTransitionLinkCongr.lean b/ComplexityTests/StateTransitionLinkCongr.lean
new file mode 100644
index 0000000000..cd4314391d
--- /dev/null
+++ b/ComplexityTests/StateTransitionLinkCongr.lean
@@ -0,0 +1,48 @@
+/-
+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 (complete linked-run transport regressions)
+
+public import Complexity.DataStructure.Memory.Spec
+public import Complexity.DataStructure.StateTransition.LinkCongr
+
+/-! Complete method runs preserve adaptive replies, changed memory and the selected history.
+An extra read has the same result and final state but a different charged history. -/
+
+public section
+
+namespace Cslib.DataStructure.Tests.LinkCongr
+
+/-- Replacing every method by a result-staging wrapper preserves the complete adaptive run. -/
+theorem linked_write_read (w : ℕ) (s : Memory.State) :
+    (Memory.spec w).runClient s
+      (link (D := Memory.spec w) (E := Memory.spec w)
+        (fun o => do let a ← PFunctor.FreeM.lift o; pure a)
+        (do let v ← Memory.read 1; Memory.write 2 (v + 1); Memory.read 2)) =
+      (s.mem 1 + 1, ⟨Function.update s.mem 2 (s.mem 1 + 1), s.frontier⟩,
+        [Memory.Op.read 1, Memory.Op.write 2 (s.mem 1 + 1), Memory.Op.read 2]) := by
+  have hmethods : ∀ t (o : Memory.Op),
+      (Memory.spec w).runClient t (PFunctor.FreeM.lift o) =
+        (Memory.spec w).runClient t (do let a ← PFunctor.FreeM.lift o; pure a) := by
+    intro t o
+    change (Memory.spec w).runClient t (PFunctor.FreeM.lift o) =
+      (Memory.spec w).runClient t ((PFunctor.FreeM.lift o).bind fun a => .pure a)
+    rw [StateTransitionSpec.runClient_bind]
+    rfl
+  rw [← StateTransitionSpec.runClient_link_congr _ _ hmethods]
+  rfl
+
+-- Keeping the answer and final state alone is insufficient: the lower history differs.
+example (w : ℕ) (s : Memory.State) :
+    (Memory.spec w).runClient s (Memory.read 1) ≠
+      (Memory.spec w).runClient s (do let _ ← Memory.read 1; Memory.read 1) := by
+  intro h
+  have hlength := congrArg (fun r : ℕ × Memory.State × List Memory.Op => r.2.2.length) h
+  change 1 = 2 at hlength
+  omega
+
+end Cslib.DataStructure.Tests.LinkCongr
diff --git a/ComplexityTests/WordRAMRealizationCall.lean b/ComplexityTests/WordRAMRealizationCall.lean
new file mode 100644
index 0000000000..143e1f100b
--- /dev/null
+++ b/ComplexityTests/WordRAMRealizationCall.lean
@@ -0,0 +1,145 @@
+/-
+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 (realize certificate-call regression tests)
+
+public import Complexity.Tactic.Realize
+
+/-!
+# Calls to separately certified memory methods
+
+The methods are parameters, so their implementations cannot be unfolded. Calls select existing
+live words, may alias inputs, and carry their method domain to the reached memory. Argument
+computation requires an explicit, charged glue step.
+-/
+
+public section
+
+namespace Cslib.WordRAM.Realization.Tests.Call
+
+open Cslib.DataStructure
+
+private abbrev word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+private abbrev pairWords : ℕ × ℕ ↪ (Fin 2 → ℕ) := appendWords word word
+private abbrev unitWords : Unit ↪ (Fin 0 → ℕ) := (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+
+-- A separately certified method consumes a projection of a larger live environment.
+theorem projection_call (m : ℕ → Memory.Prog ℕ) (P : ℕ → ℕ → Memory.State → Prop)
+    (hm : Realizes .exact m (WordEncoding.encode (α := ℕ)) (WordEncoding.encode (α := ℕ))
+      P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ × ℕ => m d.2) (WordEncoding.encode (α := ℕ × ℕ))
+      (WordEncoding.encode (α := ℕ)) (fun w d s => P w d.2 s) (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- A tuple-argument certificate can certify a curried method without unfolding its body.
+example (m : ℕ → ℕ → Memory.Prog ℕ) (P : ℕ → ℕ × ℕ → Memory.State → Prop)
+    (hm : Realizes .exact (fun d : ℕ × ℕ => m d.1 d.2) pairWords word P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ × ℕ => m d.2 d.1) pairWords word
+      (fun w d s => P w (d.2, d.1) s) (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- A curried opaque extraction feeds the canonical three-word optional-pair continuation.
+example (extract : ℕ → ℕ → Memory.Prog (Option (ℕ × ℕ)))
+    (P : ℕ → ℕ × ℕ → Memory.State → Prop)
+    (hm : Realizes .exact (fun d : ℕ × ℕ => extract d.1 d.2) pairWords
+      (WordEncoding.encode (α := Option (ℕ × ℕ))) P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ × ℕ => do
+      match ← extract d.2 d.1 with
+      | none => pure (0, 0)
+      | some (v, k) => pure (v, k)) pairWords pairWords
+      (fun w d s => P w (d.2, d.1) s) (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- A small faithful dependent-index fixture pins the actual staged-call failure.
+private def indexedWords : (Σ n : ℕ, Fin n) ↪ (Fin 2 → ℕ) where
+  toFun d := ![d.1, d.2.val]
+  inj' := by
+    rintro ⟨n, i⟩ ⟨m, j⟩ h
+    have hn : n = m := congrFun h 0
+    subst m
+    have hi : i = j := Fin.ext (congrFun h 1)
+    cases hi
+    rfl
+
+private abbrev IndexedArgument := ((Σ n : ℕ, Fin n) × ℕ) × ℕ
+private abbrev indexedInput : IndexedArgument ↪ (Fin 4 → ℕ) :=
+  appendWords (appendWords indexedWords word) word
+
+-- The implicit index must be solved before its dependent argument after charged pair staging.
+example (m : {n : ℕ} → Fin n → ℕ → ℕ → Memory.Prog Unit)
+    (P : ℕ → IndexedArgument → Memory.State → Prop)
+    (hm : Realizes .exact (fun d : IndexedArgument => m d.1.1.2 d.1.2 d.2)
+      indexedInput unitWords P (fun _ _ => 0)) :
+    Realizes .exact (fun d : IndexedArgument => do
+      let a ← pure (d.1.2, d.2)
+      m d.1.1.2 a.1 a.2) indexedInput unitWords P (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- Scalar staging also charges the subtraction and constant before entering the method domain.
+example (m : {n : ℕ} → Fin n → ℕ → ℕ → Memory.Prog Unit)
+    (P : ℕ → IndexedArgument → Memory.State → Prop)
+    (hm : Realizes .exact (fun d : IndexedArgument => m d.1.1.2 d.1.2 d.2)
+      indexedInput unitWords P (fun _ _ => 0)) :
+    Realizes .exact (fun d : IndexedArgument => do
+      let size ← pure (d.1.2 - 1)
+      let start ← pure 1
+      m d.1.1.2 size start) indexedInput unitWords
+      (fun w d s => 1 ≤ d.1.2 ∧ P w ((d.1.1, d.1.2 - 1), 1) s)
+      (fun _ _ => 0) := by
+  realize <;> first | exact h.1 | exact h.2 | exact (hwords 2).of_le h.1
+
+-- Input registers need not be distinct: the existing reindex rule permits aliasing.
+example (m : ℕ × ℕ → Memory.Prog ℕ) (P : ℕ → ℕ × ℕ → Memory.State → Prop)
+    (hm : Realizes .exact m pairWords word P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ => m (d, d)) word word
+      (fun w d s => P w (d, d) s) (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- The returned word is live in the continuation, without revealing the method body.
+example (m : ℕ → Memory.Prog ℕ) (P : ℕ → ℕ → Memory.State → Prop)
+    (hm : Realizes .exact m word word P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ × ℕ => do
+      let a ← m d.1
+      Memory.write d.2 a) pairWords unitWords
+      (fun w d s => P w d.1 s) (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- A call's domain is required at the actual state reached after a write.
+example (m : ℕ → Memory.Prog ℕ) (P : ℕ → ℕ → Memory.State → Prop)
+    (hm : Realizes .exact m word word P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ × ℕ => do
+      Memory.write d.1 d.2
+      m d.2) pairWords word
+      (fun w d s => P w d.2 ⟨Function.update s.mem d.1 d.2, s.frontier⟩)
+      (fun _ _ => 0) := by
+  realize
+  exact h
+
+-- An arithmetic argument cannot be passed by free static rewiring.
+example (m : ℕ → Memory.Prog ℕ)
+    (_hm : Realizes .exact m word word (fun _ _ _ => True) (fun _ _ => 0)) : True := by
+  fail_if_success
+    have _ : Realizes .exact (fun d : ℕ => m (d + 1)) word word
+        (fun _ _ _ => True) (fun _ _ => 0) := by realize
+  trivial
+
+-- Its explicit pure step is certified glue; the fitting arithmetic result stays visible.
+example (m : ℕ → Memory.Prog ℕ) (P : ℕ → ℕ → Memory.State → Prop)
+    (hm : Realizes .exact m word word P (fun _ _ => 0)) :
+    Realizes .exact (fun d : ℕ => do
+      let a ← pure (d + 1)
+      m a) word word
+      (fun w d s => Fits w (d + 1) ∧ P w (d + 1) s) (fun _ _ => 0) := by
+  realize <;> first | exact h.1 | exact h.2
+
+end Cslib.WordRAM.Realization.Tests.Call
diff --git a/ComplexityTests/WordRAMRealizeScope.lean b/ComplexityTests/WordRAMRealizeScope.lean
new file mode 100644
index 0000000000..94bccad482
--- /dev/null
+++ b/ComplexityTests/WordRAMRealizeScope.lean
@@ -0,0 +1,52 @@
+/-
+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 (realize syntax-scope regression tests)
+
+public import Complexity.Computability.WordRAM.Realization.Basic
+import Complexity.Tactic.Realize
+
+/-!
+# Importing realization machinery does not activate its tactic
+
+A private import, including one through an abstract's bridge, must not make `realize` available
+outside the Word-RAM scope. Opening either the namespace or its scope activates the same tactic.
+-/
+
+public section
+
+namespace ComplexityTests.WordRAMRealizeScope
+
+-- Test the parser directly: an unknown tactic is a parse error, outside `#guard_msgs`' scope.
+run_cmd do
+  match Lean.Parser.runParserCategory (← Lean.getEnv) `tactic "realize" with
+  | .error _ => pure ()
+  | .ok _ => throwError "`realize` is active without the Word-RAM scope"
+
+open scoped Cslib.WordRAM in
+/-- Opening the scope activates the tactic without opening its declaration namespace. -/
+theorem read_with_scoped_open : Cslib.WordRAM.Realization.Realizes .exact
+    (fun n : ℕ => Cslib.DataStructure.Memory.read n)
+    (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+    (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun _ _ _ => True) (fun _ _ => 0) := by
+  realize
+
+open Cslib.WordRAM in
+/-- Opening the namespace also activates its scoped tactic. -/
+theorem read_with_namespace_open : Cslib.WordRAM.Realization.Realizes .exact
+    (fun n : ℕ => Cslib.DataStructure.Memory.read n)
+    (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+    (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun _ _ _ => True) (fun _ _ => 0) := by
+  realize
+
+-- The command-local opens above must not activate the syntax for later declarations.
+run_cmd do
+  match Lean.Parser.runParserCategory (← Lean.getEnv) `tactic "realize" with
+  | .error _ => pure ()
+  | .ok _ => throwError "a command-local open leaked the `realize` syntax"
+
+end ComplexityTests.WordRAMRealizeScope
diff --git a/manual/algorithms-and-memory/memory-specifications.md b/manual/algorithms-and-memory/memory-specifications.md
index c2f11311a5..e7f21ffaeb 100644
--- a/manual/algorithms-and-memory/memory-specifications.md
+++ b/manual/algorithms-and-memory/memory-specifications.md
@@ -8,6 +8,15 @@
 
 A client charge sums explicitly chosen operation weights. Pure Lean work in the continuation is uncharged. An abstract client bound therefore measures interaction with the supplied backend, not total machine time. Refinement packages an invariant, abstract-state map and lower-level method programs; composition transports correctness and cost bounds. [Complexity/DataStructure/StateTransition/Amortized.lean](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/DataStructure/StateTransition/Amortized.lean) adds potential-based telescoping.
 
+For deterministic methods, import `Complexity.DataStructure.StateTransition.LinkCongr` to
+use `StateTransitionSpec.runClient_link_congr` when replacing methods under an adaptive client.
+Its premise equates each complete method run at every starting state and operation: answer,
+final state and lower-operation history. The linked client retains all three. This transports
+semantics; native call and argument-staging costs need their own realization. Open the complete
+[linked-run clients](../../ComplexityTests/StateTransitionLinkCongr.lean): `linked_write_read`
+preserves changed memory and history, while an extra-read counterexample shows why equal
+answers and final states alone do not preserve the charged history.
+
 ## Randomized and oblivious interfaces
 
 [RandomizedSpec](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/DataStructure/StateTransition/Randomized.lean#L98) supplies a PMF stateful handler. Support induces the relational specification, while `withCoins` allows clients their own samples. `RandomizedRefinement` requires the exact output/state law, not just a relation between possible outcomes. `run_link` transports this law through adaptive clients. `ExpectedAmortized.client` and `.comp` telescope expected lower-level costs plus potential and compose refinement layers. Until-bad rules transport explicit error bounds when exact equality is unavailable.
diff --git a/manual/design-and-assurance/automation.md b/manual/design-and-assurance/automation.md
index 0d436e4965..8742be8cbb 100644
--- a/manual/design-and-assurance/automation.md
+++ b/manual/design-and-assurance/automation.md
@@ -21,6 +21,37 @@ Plain and internal tidy predicates have separate search rules at this snapshot.
 
 This is a family of focused proof tools, not one universal automatic complexity analyzer. Their common interface makes reusable algorithms easier to recognize without conflating the predicates they prove.
 
+## Certify and reuse memory methods
+
+Import `Complexity.Tactic.Realize` for a memory-client goal
+`Realizes B p input output safe work`. Activate `realize` inside `Cslib.WordRAM`, with
+`open Cslib.WordRAM`, or with `open scoped Cslib.WordRAM`. Importing the module alone leaves
+the syntax inactive; a command-local open ends with that declaration. Open the complete
+[scope clients](../../ComplexityTests/WordRAMRealizeScope.lean) for both activation forms and
+the check that local opens do not leak into later declarations.
+
+Place a callee's zero-local-work `Realizes` certificate in the local context to reuse an opaque
+method before unfolding it. The tactic checks its basis and output encoding and uses existing
+`Realizes.reindex` to wire every encoded argument coordinate to an already live word. The
+complete [method-call clients](../../ComplexityTests/WordRAMRealizationCall.lean) cover
+projections, aliased inputs, curried and dependent arguments, and optional-pair replies.
+Certificates are tried in context order; this does not search for a runtime bound.
+Zero local work is an absorbed grading: the callee still has its certified native allowance
+against memory charge. It does not mean zero machine instructions.
+
+The called method's domain must hold at the memory actually reached by earlier queries.
+The call client after a write demonstrates that obligation explicitly. Computed arguments
+such as `d+1` need an explicit certified `pure` stage and its fit/domain proof; they cannot be
+supplied by static register wiring. The same file contrasts the rejected unstaged call with
+its successful staged version and includes dependent pair/scalar staging.
+
+If `realize` is unavailable, check scope activation. If a method call is unsupported, check the
+certificate's basis, output encoding, zero local work and live input coordinates, then inspect
+the domain at the reached memory. Retain the fit and safety obligations left by the tactic;
+unfolding the method or dropping a resource premise does not supply those proofs. The
+[realization reference](../algorithms-and-memory/memory-specifications.md) explains the uniform
+code and charging contract; the complete clients above supply imports and local context.
+
 ## Circuit construction
 
 [`synthesis_step`](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Tactic/Synthesis.lean#L13) applies an explicitly supplied synthesis rule and locates its required wires among available values. `Synthesis.Builder` retains earlier wires and accumulates certified cost. Membership search itself adds no gates. Reusing a computed value preserves sharing; invoking a new construction charges its bound. A final budget check verifies the chosen construction fits the target, but does not search globally for an optimal circuit.