diff --git a/Complexity.lean b/Complexity.lean
index b551409be2..b99812895a 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2649,6 +2649,7 @@ public import Complexity.Computability.WordRAM.Realization.MemoryBackend
 public import Complexity.Computability.WordRAM.Realization.Module
 public import Complexity.Computability.WordRAM.Realization.Primitive
 public import Complexity.Computability.WordRAM.Realization.Program
+public import Complexity.Computability.WordRAM.Realization.Program.Standard
 public import Complexity.Computability.WordRAM.Realization.Reindex
 public import Complexity.Computability.WordRAM.Realization.Result
 public import Complexity.Computability.WordRAM.Realization.While
diff --git a/Complexity/Computability/WordRAM/Realization/Program/Standard.lean b/Complexity/Computability/WordRAM/Realization/Program/Standard.lean
new file mode 100644
index 0000000000..7053543fb4
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Program/Standard.lean
@@ -0,0 +1,192 @@
+/-
+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.Program
+
+/-!
+# Initialized flat programs with a fixed register layout
+
+Choose the frontier, input bank and fresh scratch bank once, before every runtime width and
+argument. Clients supply the same encoded-input, fit, domain and memory-history premises as
+`Realizes.exists_init_program`, without proving register-placement conditions themselves.
+The real `Data.init` prefix, native body and trailing halt are all charged. Its positive
+next-free address must fit even for an empty input; this is not a width-zero initialization.
+
+## Main results
+
+* `Realizes.exists_standard_init_program_state_from_words`: one flat program for independent
+  raw memory and register arguments, related by their input prefix.
+* `Realizes.exists_standard_init_program_state`: the argument-indexed specialization, retaining
+  the exact whole-memory, frontier and all encoded result words at its fixed halting location.
+* `Realizes.exists_standard_init_program`: the scalar `Executes` projection of that same run.
+
+The observed coordinate is static, as in the existing scalar export. Zero-output Unit clients
+continue to use the separate charged Unit-observation API.
+
+## References
+
+This is original infrastructure over the existing realization certificate, charged input prefix
+and native `Code.program` compiler. It introduces no execution model or client language.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization
+
+open Cslib.DataStructure
+
+private abbrev registers (k l n : ℕ) : ℕ := 1 + (k + (l + n + 1))
+
+private def standardFrontier {k l n : ℕ} : Fin (registers k l n) :=
+  ⟨0, by unfold registers; omega⟩
+
+private def standardInput {k l n : ℕ} (i : Fin k) : Fin (registers k l n) :=
+  Fin.natAdd 1 (Fin.castAdd (l + n + 1) i)
+
+private def standardScratch {k l n : ℕ} (i : Fin (l + n + 1)) : Fin (registers k l n) :=
+  Fin.natAdd 1 (Fin.natAdd k i)
+
+private theorem standardPlacement (k l n : ℕ) :
+    Function.Injective (standardInput (k := k) (l := l) (n := n)) ∧
+    Function.Injective (standardScratch (k := k) (l := l) (n := n)) ∧
+    (∀ i j, standardInput (l := l) (n := n) i ≠ standardScratch (k := k) j) ∧
+    (∀ j, standardScratch (k := k) (l := l) (n := n) j ≠ standardFrontier) ∧
+    (∀ i, standardInput (k := k) (l := l) (n := n) i ≠ standardFrontier) := by
+  refine ⟨?_, ?_, ?_, ?_, ?_⟩
+  · intro i j h
+    apply Fin.ext
+    have := congrArg Fin.val h
+    simpa only [standardInput, Fin.val_natAdd, Fin.val_castAdd,
+      Nat.add_left_cancel_iff] using this
+  · intro i j h
+    apply Fin.ext
+    have := congrArg Fin.val h
+    simp only [standardScratch, Fin.val_natAdd] at this
+    omega
+  · intro i j h
+    have := congrArg Fin.val h
+    simp only [standardInput, standardScratch, Fin.val_natAdd, Fin.val_castAdd] at this
+    have := i.isLt
+    omega
+  · intro i h
+    have := congrArg Fin.val h
+    simp only [standardScratch, standardFrontier, Fin.val_natAdd] at this
+    omega
+  · intro i h
+    have := congrArg Fin.val h
+    simp only [standardInput, standardFrontier, Fin.val_natAdd, Fin.val_castAdd] at this
+    omega
+
+namespace Realizes
+
+variable {k l : ℕ} {δ α : Type} {p : δ → Memory.Prog α}
+  {input : δ ↪ (Fin k → ℕ)} {output : α ↪ (Fin l → ℕ)}
+  {safe : ℕ → δ → Memory.State → Prop} {work : δ → Memory.State → ℕ}
+
+/-- One statically laid-out flat program includes charged input installation and its halt.
+The witnessed native state is the actual final state of the flat run, retaining the entire
+source memory and frontier and every result coordinate. The raw input words vary independently
+of the register-encoded argument: only their input prefix must agree. All witnesses precede
+both kinds of runtime data. -/
+theorem exists_standard_init_program_state_from_words
+    (h : Realizes .exact p input output safe work) (i : Fin l) :
+    ∃ r C pc : ℕ, ∃ prog : Program .exact r,
+      ∃ frontier : Fin r, ∃ out : Fin l → Fin r,
+      ∀ w d words, (∀ j : Fin k, words.getD j.val 0 = input d j) →
+        k ≤ words.length → Fits w (words.length + 1) → InputFits w words →
+        safe w d (inputState words) →
+        (Memory.spec w).ValidHistory (inputState words)
+          ((Memory.spec w).clientHistory (inputState words) (p d)) →
+        ∃ y n, Runs w prog (State.init words) ⟨pc, y⟩ n ∧
+          step w prog ⟨pc, y⟩ =
+            .halt (output ((Memory.spec w).clientResult (inputState words) (p d)) i) ∧
+          memoryState frontier y = (Memory.spec w).clientState (inputState words) (p d) ∧
+          (∀ j, y.regs (out j) =
+            output ((Memory.spec w).clientResult (inputState words) (p d)) j) ∧
+          n + 1 ≤ C * (memoryCost (p d) (inputState words) +
+            work d (inputState words) + 1) + 1 := by
+  obtain ⟨n, C, emit, he⟩ := h
+  let r := registers k l n
+  let frontier : Fin r := standardFrontier
+  let src : Fin k → Fin r := standardInput
+  let tmp : Fin (l + n + 1) → Fin r := standardScratch
+  obtain ⟨hsrc, htmp, hd, hf, hs⟩ := standardPlacement k l n
+  let code := Code.seq (inputPrefix frontier (tmp (Fin.last (l + n))) src)
+    (emit frontier src tmp)
+  let prog := code.program (tmp (Fin.castAdd (n + 1) i))
+  refine ⟨r, C + (2 * k + 5), code.size, prog, frontier,
+    (fun j => tmp (Fin.castAdd (n + 1) j)), ?_⟩
+  intro w d words hlayout hk hw hin hsafe hv
+  obtain ⟨x, ex, hx, hm, hwords, _⟩ := inputPrefix_exec frontier (tmp (Fin.last (l + n)))
+    src words hsrc (hf _) (fun j => hd j _) hs hk hw hin
+  have harg : x.regs ∘ src = input d := by
+    funext j
+    exact (hwords j).trans (hlayout j)
+  obtain ⟨y, ey, hmem, hout, _⟩ := (he frontier src tmp htmp hd hf hs).2 w d x hx harg
+    (hm.symm ▸ hsafe) (hm.symm ▸ hv)
+  rw [hm] at ey hmem hout
+  obtain ⟨steps, hsteps, erun⟩ := ex.seq ey
+  have hr := erun.runs (pc := 0) (p := prog) (Program.Contains.self _).append_left
+  refine ⟨y, steps, ?_, ?_, hmem, hout, ?_⟩
+  · simpa only [Nat.zero_add, State.init, code] using hr
+  · rw [← hout i]
+    exact step_halt (by simp [prog, Code.program])
+  · have hpos : 1 ≤ memoryCost (p d) (inputState words) +
+        work d (inputState words) + 1 := by omega
+    have hover := Nat.mul_le_mul_left (2 * k + 5) hpos
+    simp only [Nat.mul_one] at hover
+    rw [Nat.add_mul]
+    omega
+
+/-- One statically laid-out flat program includes charged input installation and its halt.
+The witnessed native state is the actual final state of the flat run, retaining the entire
+source memory and frontier and every result coordinate. All witnesses precede runtime data. -/
+theorem exists_standard_init_program_state (h : Realizes .exact p input output safe work)
+    (raw : δ → List ℕ) (hlayout : ∀ d (i : Fin k), (raw d).getD i.val 0 = input d i)
+    (i : Fin l) :
+    ∃ r C pc : ℕ, ∃ prog : Program .exact r,
+      ∃ frontier : Fin r, ∃ out : Fin l → Fin r,
+      ∀ w d, k ≤ (raw d).length → Fits w ((raw d).length + 1) → InputFits w (raw d) →
+        safe w d (inputState (raw d)) →
+        (Memory.spec w).ValidHistory (inputState (raw d))
+          ((Memory.spec w).clientHistory (inputState (raw d)) (p d)) →
+        ∃ y n, Runs w prog (State.init (raw d)) ⟨pc, y⟩ n ∧
+          step w prog ⟨pc, y⟩ =
+            .halt (output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) i) ∧
+          memoryState frontier y = (Memory.spec w).clientState (inputState (raw d)) (p d) ∧
+          (∀ j, y.regs (out j) =
+            output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) j) ∧
+          n + 1 ≤ C * (memoryCost (p d) (inputState (raw d)) +
+            work d (inputState (raw d)) + 1) + 1 := by
+  obtain ⟨r, C, pc, prog, frontier, out, he⟩ :=
+    h.exists_standard_init_program_state_from_words i
+  exact ⟨r, C, pc, prog, frontier, out, fun w d => he w d (raw d) (hlayout d)⟩
+
+/-- The canonical initialized export requires no caller-written register layout. Its bound
+includes the actual prefix, body and final halt, with code fixed before every width and input. -/
+theorem exists_standard_init_program (h : Realizes .exact p input output safe work)
+    (raw : δ → List ℕ) (hlayout : ∀ d (i : Fin k), (raw d).getD i.val 0 = input d i)
+    (i : Fin l) :
+    ∃ r C : ℕ, ∃ prog : Program .exact r,
+      ∀ w d, k ≤ (raw d).length → Fits w ((raw d).length + 1) → InputFits w (raw d) →
+        safe w d (inputState (raw d)) →
+        (Memory.spec w).ValidHistory (inputState (raw d))
+          ((Memory.spec w).clientHistory (inputState (raw d)) (p d)) →
+        ∃ t, Executes w prog (State.init (raw d))
+            (output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) i) t ∧
+          t ≤ C * (memoryCost (p d) (inputState (raw d)) +
+            work d (inputState (raw d)) + 1) + 1 := by
+  obtain ⟨r, C, pc, prog, _, _, he⟩ := h.exists_standard_init_program_state raw hlayout i
+  refine ⟨r, C, prog, ?_⟩
+  intro w d hk hw hin hsafe hv
+  obtain ⟨y, n, hr, hh, _, _, hn⟩ := he w d hk hw hin hsafe hv
+  exact ⟨n + 1, ⟨⟨pc, y⟩, n, hr, hh, rfl⟩, hn⟩
+
+end Realizes
+end Cslib.WordRAM.Realization
diff --git a/ComplexityTests/WordRAMRealizationProgram.lean b/ComplexityTests/WordRAMRealizationProgram.lean
index 808b775985..abc00e6d03 100644
--- a/ComplexityTests/WordRAMRealizationProgram.lean
+++ b/ComplexityTests/WordRAMRealizationProgram.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
-import Complexity.Computability.WordRAM.Realization.Program
+import Complexity.Computability.WordRAM.Realization.Program.Standard
 
 /-! Nonvacuous flat-program projections with uniform code and clock constants, for both
 already installed arguments and an actually charged native list-input prefix. The former
@@ -99,47 +99,19 @@ example : ∃ (r C : ℕ) (p : Program .exact r),
 example : ∃ (r C : ℕ) (p : Program .exact r),
     ∀ w d, Fits w 2 → Fits w d →
       ∃ t, Executes w p (State.init [d]) d t ∧ t ≤ C + 1 := by
-  obtain ⟨n, C, emit, he⟩ := copy_realizes.exists_init_program (fun d => [d]) (by
+  obtain ⟨r, C, prog, he⟩ := copy_realizes.exists_standard_init_program (fun d => [d]) (by
     intro d i
     have hi : i = 0 := Fin.eq_zero i
     subst i
-    rfl)
-  let m := 1 + n + 1
-  let r := m + 2
-  let frontier : Fin r := ⟨1, by dsimp [r, m]; omega⟩
-  let src : Fin 1 → Fin r := fun _ => ⟨0, by dsimp [r, m]; omega⟩
-  let tmp : Fin (1 + n + 1) → Fin r := fun j => ⟨j.val + 2, by dsimp [r, m]; omega⟩
-  have hi : Function.Injective tmp := by
-    intro a b h
-    apply Fin.ext
-    have := congrArg Fin.val h
-    dsimp [tmp] at this
-    omega
-  have hd : ∀ i j, src i ≠ tmp j := by
-    intro i j h
-    have := congrArg Fin.val h
-    change 0 = j.val + 2 at this
-    omega
-  have hf : ∀ j, tmp j ≠ frontier := by
-    intro j h
-    have := congrArg Fin.val h
-    change j.val + 2 = 1 at this
-    omega
-  have hs : ∀ i, src i ≠ frontier := by
-    intro i h
-    have := congrArg Fin.val h
-    change 0 = 1 at this
-    omega
-  refine ⟨r, C, (Code.seq (inputPrefix frontier (tmp (Fin.last (1 + n))) src)
-    (emit frontier src tmp)).program (tmp (Fin.castAdd (n + 1) (0 : Fin 1))), ?_⟩
+    rfl) 0
+  refine ⟨r, C, prog, ?_⟩
   intro w d h2 hfit
   have hin : InputFits w [d] := by
     refine ⟨h2.of_le (by simp), ?_⟩
     intro v hv
     simp only [List.mem_singleton] at hv
     exact hv.symm ▸ hfit
-  obtain ⟨t, ht, htime⟩ := he frontier src tmp (fun _ _ _ => Subsingleton.elim _ _) hi
-    hd hf hs 0 w d (by simp) h2 hin trivial (by trivial)
+  obtain ⟨t, ht, htime⟩ := he w d (by simp) h2 hin trivial (by trivial)
   change t ≤ C * (0 + 0 + 1) + 1 at htime
   exact ⟨t, ht, by simpa using htime⟩
 
diff --git a/ComplexityTests/WordRAMRealizationStandardProgram.lean b/ComplexityTests/WordRAMRealizationStandardProgram.lean
new file mode 100644
index 0000000000..20ed5e4f22
--- /dev/null
+++ b/ComplexityTests/WordRAMRealizationStandardProgram.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: local-only (canonical initialized flat-program clients)
+
+public import Complexity.Algorithms.WordRAM.Dijkstra.ListEncode
+public import Complexity.Computability.WordRAM.Realization.Bind
+public import Complexity.Computability.WordRAM.Realization.Glue
+public import Complexity.Computability.WordRAM.Realization.Primitive
+public import Complexity.Computability.WordRAM.Realization.Program.Standard
+
+/-!
+# Canonical flat programs for an actual memory client
+
+One fixed program writes a runtime word to an input-memory cell and reads it back. The complete
+native post-memory, frontier and encoded result are checked without any register-bank proof in
+the client. The empty-input case keeps the actual positive next-free-address premise.
+-/
+
+public section
+
+namespace Cslib.WordRAM.Realization.Tests.StandardProgram
+
+open Cslib.DataStructure
+
+private abbrev word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+private abbrev unitWords : Unit ↪ (Fin 0 → ℕ) := (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+private abbrev arguments : ℕ × ℕ ↪ (Fin 2 → ℕ) := appendWords word word
+
+private def writeRead (d : ℕ × ℕ) : Memory.Prog ℕ := do
+  Memory.write d.1 d.2
+  Memory.read d.1
+
+private theorem writeRead_realizes :
+    Realizes .exact writeRead arguments word (fun _ _ _ => True) (fun _ _ => 1) := by
+  have h := (Realizes.write (B := .exact) arguments 0 1).bind
+    (Realizes.read (appendWords arguments unitWords) 0)
+  exact h.consequence (fun _ _ _ _ _ _ => ⟨trivial, trivial⟩) (fun _ _ => le_rfl)
+
+/-- A uniform flat program preserves the actual final data of a write followed by a read.
+There are no caller-written register indices, disjointness conditions or intermediate states. -/
+theorem writeRead_native : ∃ r C pc : ℕ, ∃ prog : Program .exact r,
+    ∃ frontier result : Fin r, ∀ w v, Fits w 3 → Fits w v →
+      ∃ y n, Runs w prog (State.init [1, v]) ⟨pc, y⟩ n ∧
+        step w prog ⟨pc, y⟩ = .halt v ∧
+        y.mem 1 = v ∧ y.mem 2 = v ∧ y.mem 100 = 0 ∧
+        y.regs frontier = 3 ∧ y.regs result = v ∧ n + 1 ≤ C * 4 + 1 := by
+  obtain ⟨r, C, pc, prog, frontier, out, he⟩ :=
+    writeRead_realizes.exists_standard_init_program_state (fun d => [d.1, d.2])
+      (by intro d i; fin_cases i <;> rfl) 0
+  refine ⟨r, C, pc, prog, frontier, out 0, ?_⟩
+  intro w v h3 hv
+  have hin : InputFits w [1, v] := by
+    refine ⟨h3.of_le (by change 2 ≤ 3; decide), ?_⟩
+    intro a ha
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at ha
+    rcases ha with rfl | rfl
+    · exact h3.of_le (by decide)
+    · exact hv
+  have hvalid : (Memory.spec w).ValidHistory (inputState [1, v])
+      ((Memory.spec w).clientHistory (inputState [1, v]) (writeRead (1, v))) := by
+    change (1 < 3 ∧ Fits w v) ∧ 1 < 3 ∧ True
+    exact ⟨⟨by decide, hv⟩, by decide, trivial⟩
+  obtain ⟨y, n, hr, hh, hm, hout, hn⟩ := he w (1, v)
+    (by change 2 ≤ 2; exact le_rfl) h3 hin trivial hvalid
+  exact ⟨y, n, hr, hh, congrArg (fun s : Memory.State => s.mem 1) hm,
+    congrArg (fun s : Memory.State => s.mem 2) hm,
+    congrArg (fun s : Memory.State => s.mem 100) hm,
+    congrArg Memory.State.frontier hm, hout 0, hn⟩
+
+-- A concrete maximum-width payload inhabits the uniform memory-client endpoint.
+example : ∃ r : ℕ, ∃ prog : Program .exact r, ∃ y : Data r, ∃ pc n : ℕ,
+    Runs 4 prog (State.init [1, 15]) ⟨pc, y⟩ n ∧
+      step 4 prog ⟨pc, y⟩ = .halt 15 ∧ y.mem 1 = 15 ∧ y.mem 100 = 0 := by
+  obtain ⟨r, _, pc, prog, _, _, he⟩ := writeRead_native
+  obtain ⟨y, n, hr, hh, hm, _, ht, _⟩ := he 4 15 (by decide) (by decide)
+  exact ⟨r, prog, y, pc, n, hr, hh, hm, ht⟩
+
+private theorem zero_realizes :
+    Realizes .exact (fun _ : Unit => (pure 0 : Memory.Prog ℕ)) unitWords word
+      (fun _ _ _ => True) (fun _ _ => 1) := by
+  have h := Realizes.glue unitWords (GlueComputes.const (B := .exact) (P := fun _ => True)
+    (bound := fun _ => 0) 0 (fun _ _ => le_rfl))
+  exact h.consequence (fun w _ _ _ _ _ => ⟨trivial, fits_zero w⟩) (fun _ _ => le_rfl)
+
+/-- Empty input still installs frontier one, with its neutral copy and halt charged. -/
+theorem emptyInput_native : ∃ r C : ℕ, ∃ prog : Program .exact r,
+    ∀ w, Fits w 1 → ∃ t, Executes w prog (State.init []) 0 t ∧ t ≤ C * 2 + 1 := by
+  obtain ⟨r, C, prog, he⟩ := zero_realizes.exists_standard_init_program (fun _ => [])
+    (fun _ i => Fin.elim0 i) 0
+  refine ⟨r, C, prog, ?_⟩
+  intro w h1
+  exact he w () (by decide) h1 ⟨fits_zero w, by simp⟩ trivial (by trivial)
+
+private theorem readHeader_realizes :
+    Realizes .exact (fun _ : Unit => Memory.read 1) unitWords word
+      (fun w _ _ => Fits w 1) (fun _ _ => 2) := by
+  have h := (Realizes.glue unitWords (GlueComputes.const (B := .exact)
+    (P := fun _ => True) (bound := fun _ => 1) 1 (fun _ _ => le_rfl))).bind
+      (Realizes.read (appendWords unitWords word) 0)
+  exact h.consequence (fun _ _ _ _ _ hfit => ⟨⟨trivial, hfit⟩, trivial⟩)
+    (fun _ _ => le_rfl)
+
+/-- The graph is runtime memory, while the register argument is only Unit. One fixed program
+reads its first header word for every adjacency-list instance, preserving all input memory. -/
+theorem graphHeader_native : ∃ r C pc : ℕ, ∃ prog : Program .exact r,
+    ∃ frontier result : Fin r,
+    ∀ w (G : Cslib.Algorithms.WordRAM.Dijkstra.ListInstance),
+      Fits w (G.encode.length + 1) → InputFits w G.encode →
+      ∃ y n, Runs w prog (State.init G.encode) ⟨pc, y⟩ n ∧
+        step w prog ⟨pc, y⟩ = .halt G.n ∧
+        y.mem = (Data.init G.encode : Data 0).mem ∧
+        y.regs frontier = G.encode.length + 1 ∧ y.regs result = G.n ∧
+        n + 1 ≤ C * 4 + 1 := by
+  obtain ⟨r, C, pc, prog, frontier, out, he⟩ :=
+    readHeader_realizes.exists_standard_init_program_state_from_words 0
+  refine ⟨r, C, pc, prog, frontier, out 0, ?_⟩
+  intro w G hw hin
+  have hvalid : (Memory.spec w).ValidHistory (inputState G.encode)
+      ((Memory.spec w).clientHistory (inputState G.encode) (Memory.read 1)) := by
+    change 1 < G.encode.length + 1 ∧ True
+    rw [G.encode_length]
+    exact ⟨by omega, trivial⟩
+  obtain ⟨y, n, hr, hh, hm, hout, hn⟩ := he w () G.encode
+    (fun j => Fin.elim0 j) (Nat.zero_le _) hw hin (hw.of_le (by omega)) hvalid
+  exact ⟨y, n, hr, hh, congrArg Memory.State.mem hm,
+    congrArg Memory.State.frontier hm, hout 0, hn⟩
+
+private def isolatedVertex : Cslib.Algorithms.WordRAM.Dijkstra.ListInstance :=
+  ⟨1, fun _ => [], 0⟩
+
+private def maximumEdge : Cslib.Algorithms.WordRAM.Dijkstra.ListInstance :=
+  ⟨2, fun u => if u.val = 0 then [(1, 15)] else [], 0⟩
+
+-- Two different graph memories share one program; the maximum fitting edge weight survives.
+example : ∃ r pc : ℕ, ∃ prog : Program .exact r, ∃ y₁ y₂ : Data r, ∃ n₁ n₂ : ℕ,
+    Runs 4 prog (State.init isolatedVertex.encode) ⟨pc, y₁⟩ n₁ ∧
+      Runs 4 prog (State.init maximumEdge.encode) ⟨pc, y₂⟩ n₂ ∧
+      step 4 prog ⟨pc, y₁⟩ = .halt 1 ∧ step 4 prog ⟨pc, y₂⟩ = .halt 2 ∧
+      y₂.mem 7 = 15 := by
+  obtain ⟨r, _, pc, prog, _, _, he⟩ := graphHeader_native
+  obtain ⟨y₁, n₁, hr₁, hh₁, _⟩ := he 4 isolatedVertex (by decide) (by decide)
+  obtain ⟨y₂, n₂, hr₂, hh₂, hm₂, _⟩ := he 4 maximumEdge (by decide) (by decide)
+  exact ⟨r, pc, prog, y₁, y₂, n₁, n₂, hr₁, hr₂, hh₁, hh₂,
+    congrFun hm₂ 7⟩
+
+-- No initialized width-zero instance is claimed, even on empty input.
+example : ¬Fits 0 (([] : List ℕ).length + 1) := by decide
+
+end Cslib.WordRAM.Realization.Tests.StandardProgram
diff --git a/manual/algorithms-and-memory/memory-specifications.md b/manual/algorithms-and-memory/memory-specifications.md
index 1b01af2993..c2f11311a5 100644
--- a/manual/algorithms-and-memory/memory-specifications.md
+++ b/manual/algorithms-and-memory/memory-specifications.md
@@ -28,6 +28,55 @@ The native allocation library [Complexity/Computability/WordRAM/Allocation.lean]
 
 [Realizes](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/WordRAM/Realization/Basic.lean#L95) is a graded realization interface. It chooses scratch registers, a constant and a uniform code emitter **before** arguments, width and memory. It requires faithful register encodings, a whole-memory/frontier abstraction, register framing and explicit safety/work bounds. Its instruction allowance is proportional to `memoryCost + work + 1`. The `work` term is necessary because pure/control code can take time without making memory queries. `Realizes.exists_refines` connects it to the native controller layer. Primitive, bind and branch modules provide a compositional foundation, not a compiler for every arbitrary Lean function.
 
+### Export a canonical initialized flat program
+
+Import `Complexity.Computability.WordRAM.Realization.Program.Standard` when you have a
+`Realizes .exact` certificate and want one flat program with a fixed register layout.
+The [canonical exports](../../Complexity/Computability/WordRAM/Realization/Program/Standard.lean)
+choose the program, frontier register, result bank, halt location and constant factor before
+runtime word width and input. You supply the encoding and admissibility proofs; the exports
+supply the register placement and disjointness proofs.
+
+Choose the conclusion your client needs:
+
+- `Realizes.exists_standard_init_program_state_from_words` lets the raw memory list vary
+  independently of the register-encoded argument. Use it when a small argument controls an
+  operation on a larger input already in memory. The first `k` raw words must agree pointwise
+  with the `k` encoded argument words.
+- `Realizes.exists_standard_init_program_state` specializes that rule to a chosen `raw d`
+  list for each argument `d`. It retains the actual final native state, complete memory and
+  frontier, every encoded result word, and the fixed halting location.
+- `Realizes.exists_standard_init_program` projects the same run to scalar `Executes` at a
+  fixed result coordinate `i : Fin l`. Use the state variant when a later proof needs memory
+  or other result coordinates. Zero-output Unit clients use the separate Unit-observation
+  exports in [Program](../../Complexity/Computability/WordRAM/Realization/Program.lean).
+
+For each runtime input, prove `k ≤ words.length`, `Fits w (words.length + 1)`,
+`InputFits w words`, the certificate's `safe w d (inputState words)` condition, and
+`Memory.spec`'s `ValidHistory` for that client from `inputState words`. The raw-words rule
+also requires the prefix equality described above; the other two take that equality for
+`raw d` when choosing the program. The resulting instruction bound is
+`C * (memoryCost + work + 1) + 1`, including the executed prefix, body and halt.
+If an application fails, check the prefix, fit, safe-domain and history obligations before
+changing the program or dropping a premise. Even an empty input needs `Fits w 1`; these
+exports do not initialize at word width zero.
+
+`Data.init` places the raw input list in memory by the existing **uncharged calling
+convention**. The charged native prefix takes at most `2*k+5` instructions to install the
+frontier and the first `k` argument registers while preserving memory. It does not construct
+or copy the whole graph or other raw-memory input. Work used to obtain that initial input
+requires a separate bound if the surrounding application charges it.
+
+Open the complete checked
+[StandardProgram clients](../../ComplexityTests/WordRAMRealizationStandardProgram.lean),
+including their imports, encodings and premises, for a starting point.
+`writeRead_native` uses the state export for a write followed by a read, with a concrete
+maximum-fitting payload `15`; `emptyInput_native` uses the scalar export and exposes the
+positive frontier-fit premise. `graphHeader_native` uses the raw-words export with a Unit
+register argument and actual Dijkstra adjacency-list encodings. One program handles two
+different graphs, reads their first header word and preserves the entire input memory.
+This client is a header-read demonstration, not a Dijkstra execution or shortest-path bound.
+
 ## Footprints, traces, and memory windows
 
 [HeapAssertion](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/WordRAM/Heap.lean#L62) records a finite support and a predicate on total memory. Separating conjunction uses disjoint supports; `Modifies` records agreement outside an allowed write set. This is an explicit-footprint frame calculus inspired by separation logic, not a replacement semantics in which inaccessible cells disappear [reynolds02][reynolds02].