diff --git a/Complexity.lean b/Complexity.lean
index 69ba19053..91fb76617 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1562,9 +1562,11 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Basic
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Bounds
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Correctness
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.CounterBounds
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Expr
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.ReadInput
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.Table
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Injective
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Radix
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.ReadSymbol
diff --git a/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean b/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean
index 5472e8800..1e8e43343 100644
--- a/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean
+++ b/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean
@@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Expr
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.ReadSymbol
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Correctness
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.CounterBounds
 
 /-!
 # The configuration graph as an instance of directed connectivity
@@ -388,26 +389,6 @@ private theorem reachesOut_matrix (hL : w.length ≤ B)
   exact ⟨_, hreach, bounded_regs hL (by omega) (by omega) (by omega)⟩
 
 
-/-- The polynomial bound `((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1)` dominates
-`vertexBound + 1`, `w.length`, and `2`. -/
-private theorem configurationInstance_bounds :
-    vertexBound (k := k) (radix D w.length) + 1 ≤
-      ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) ∧
-    w.length ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) ∧
-    2 ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) := by
-  set L := w.length
-  set E := D * Fintype.card (Register k)
-  have hVB : vertexBound (k := k) (radix D L) = (L + 2) ^ E := vertexBound_eq_pow D L
-  have hpow : (L + 2) ^ E ≤ (2 * L + 2) ^ E := Nat.pow_le_pow_left (by omega) E
-  have hone : 1 ≤ (2 * L + 2) ^ E := Nat.one_le_pow _ _ (by omega)
-  have hB : ((frame w).length + 1) ^ (E + 1) = (2 * L + 2) ^ E * (2 * L + 2) := by
-    rw [length_frame, show 2 * L + 1 + 1 = 2 * L + 2 by omega, pow_succ]
-  have hmul : (2 * L + 2) ^ E * 2 ≤ (2 * L + 2) ^ E * (2 * L + 2) :=
-    Nat.mul_le_mul_left _ (by omega)
-  have hmul' : 2 * L + 2 ≤ (2 * L + 2) ^ E * (2 * L + 2) := Nat.le_mul_of_pos_left _ hone
-  rw [hB]
-  exact ⟨by omega, by omega, by omega⟩
-
 /-- A `forCode` block in `writer` is at `b` when instructions `b`, `b + 1`, `b + 2` match. -/
 private theorem codeAt_forCode {b u body exit : ℕ} {bound : Expr}
     (h₀ : (writer ntm D).instr b = .assign u (const 0) (b + 1))
@@ -429,7 +410,7 @@ theorem computableInLogSpace_configurationInstance :
   set S := startID ntm (radix D w.length)
   set B := ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1)
   have hS : S < VB := startID_lt_vertexBound ntm c w.length
-  obtain ⟨hN, hL, h2⟩ := configurationInstance_bounds (k := k) (D := D) w
+  obtain ⟨hN, hL, h2⟩ := configurationCounter_bounds (k := k) D w
   have hreg (i : ℕ) (hi : i ≤ B) : ∀ r ∈ [w.length, i, 0, 0], r ≤ B :=
     bounded_regs hL hi (by omega) (by omega)
   have hones₁ := reachesOut_ones (ntm := ntm) (D := D) w
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean
new file mode 100644
index 000000000..a018b8f44
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/CounterBounds.lean
@@ -0,0 +1,51 @@
+/-
+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.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Bounds
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame
+
+/-!
+# Polynomial counter bounds for configuration-graph writers
+
+The STCON writer and the fair-coin table writer enumerate the same polynomial compact box.
+`configurationCounter_bounds` gives a common bound for the loop counters, original input length,
+and ternary symbol/count scratch register in terms of the length of the framed input.
+
+## Main results
+
+* `Turing.MultiTapeNTM.ConfigurationGraph.configurationCounter_bounds`: the standard counter bound.
+-/
+
+public section
+
+namespace Turing.MultiTapeNTM.ConfigurationGraph
+
+open MultiTapeTM
+
+/-- The polynomial counter bound dominates the compact box plus one, the input length, and two.
+The statement includes exponent zero and the empty original word. -/
+theorem configurationCounter_bounds {k : ℕ} (D : ℕ) (w : List Bool) :
+    vertexBound (k := k) (radix D w.length) + 1 ≤
+      ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) ∧
+    w.length ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) ∧
+    2 ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) := by
+  set L := w.length
+  set E := D * Fintype.card (Register k)
+  have hVB : vertexBound (k := k) (radix D L) = (L + 2) ^ E := vertexBound_eq_pow D L
+  have hpow : (L + 2) ^ E ≤ (2 * L + 2) ^ E := Nat.pow_le_pow_left (by omega) E
+  have hone : 1 ≤ (2 * L + 2) ^ E := Nat.one_le_pow _ _ (by omega)
+  have hB : ((frame w).length + 1) ^ (E + 1) = (2 * L + 2) ^ E * (2 * L + 2) := by
+    rw [length_frame, show 2 * L + 1 + 1 = 2 * L + 2 by omega, pow_succ]
+  have hmul : (2 * L + 2) ^ E * 2 ≤ (2 * L + 2) ^ E * (2 * L + 2) :=
+    Nat.mul_le_mul_left _ (by omega)
+  have hmul' : 2 * L + 2 ≤ (2 * L + 2) ^ E * (2 * L + 2) := Nat.le_mul_of_pos_left _ hone
+  rw [hB]
+  exact ⟨by omega, by omega, by omega⟩
+
+end Turing.MultiTapeNTM.ConfigurationGraph
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Table.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Table.lean
new file mode 100644
index 000000000..0d2733d78
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Table.lean
@@ -0,0 +1,288 @@
+/-
+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.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.ReadInput
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Words
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.CounterBounds
+import Complexity.Foundations.Data.List.RowMajor
+
+/-!
+# A native writer for the compact fair-coin table
+
+`coinTable` enumerates the polynomial compact box, including its guarded invalid IDs. Each entry
+has two bits: `[false, false]`, `[true, false]`, or `[true, true]` records a coin count of zero,
+one, or two. The order is row-major, with the two bits consecutive at each entry.
+
+`coinTableProgram` starts from its actual zeroed initializer on the original framed word. It
+reads the input length with the existing word header, enumerates both compact IDs with bounded
+counter loops, and calls `coinCountCode` for every entry. No input length or vertex ID is supplied
+in advance. `computableInLogSpace_coinTable` is a native space certificate for the entire writer.
+
+This is the ambient ordinary coin-count table. Invalid compact IDs retain the existing edge
+predicate's behavior. Clocked enumeration, the bridge to the strict-forward configuration system,
+paired ports, and the recursive estimator remain separate.
+
+## Main definitions
+
+* `Turing.MultiTapePTM.ConfigurationGraph.coinTable`: the row-major two-bit count table.
+* `Turing.MultiTapePTM.ConfigurationGraph.coinTableProgram`: its initialized counter transducer.
+
+## Main results
+
+* `Turing.MultiTapePTM.ConfigurationGraph.getD_coinTable`: the exact bit at a row-major index.
+* `Turing.MultiTapePTM.ConfigurationGraph.coinTable_count`: decoding the two bits gives the count.
+* `Turing.MultiTapePTM.ConfigurationGraph.reachesOut_coinTableProgram`: the actual initialized run.
+* `Turing.MultiTapePTM.ConfigurationGraph.computableInLogSpace_coinTable`: native logarithmic space.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM.ConfigurationGraph
+
+open MultiTapeNTM.ConfigurationGraph CounterProgram Instr Expr MultiTapeTM
+open Cslib.Turing
+
+variable {k : ℕ} {State : Type} [Fintype State]
+
+/-- Every compact row and column, with two consecutive threshold bits encoding its coin count.
+The original input is read at the source's existing `queryIndex`. -/
+noncomputable def coinTable (machine : MultiTapePTM k Bool State) (D : ℕ) (w : List Bool) :
+    List Bool :=
+  let B := radix D w.length
+  let N := vertexBound (k := k) B
+  (List.finRange N).flatMap fun u : Fin N => (List.finRange N).flatMap fun v : Fin N =>
+    List.ofFn fun b : Fin 2 => decide (b.val <
+      coinCountWithSymbol machine B w.length u v w[queryIndex (k := k) B u]?)
+
+variable (machine : MultiTapePTM k Bool State) (D : ℕ) (w : List Bool)
+
+/-- The finite-index definition agrees with the natural-counter enumeration used by the writer. -/
+theorem coinTable_eq_flatMap :
+    coinTable machine D w =
+      (List.range (vertexBound (k := k) (radix D w.length))).flatMap fun u =>
+        (List.range (vertexBound (k := k) (radix D w.length))).flatMap fun v =>
+          let c := coinCountWithSymbol machine (radix D w.length) w.length u v
+            w[queryIndex (k := k) (radix D w.length) u]?
+          [decide (0 < c), decide (1 < c)] := by
+  have hval (n : ℕ) : (List.finRange n).map Fin.val = List.range n := by
+    apply List.ext_getElem <;> simp
+  dsimp only [coinTable]
+  conv_rhs => rw [← hval]; simp only [List.flatMap_map]
+  apply List.flatMap_congr
+  intro u _
+  apply List.flatMap_congr
+  intro v _
+  simp [List.ofFn_succ]
+
+/-- The table has exactly two bits for each ordered pair of compact IDs. -/
+@[simp] theorem length_coinTable :
+    (coinTable machine D w).length =
+      2 * vertexBound (k := k) (radix D w.length) ^ 2 := by
+  dsimp only [coinTable]
+  simp_rw [List.flatMap_ofFn_prod]
+  simp only [List.length_ofFn]
+  ring
+
+/-- Reading either bit at its ordinary row-major address returns the corresponding threshold. -/
+theorem getD_coinTable
+    (u v : Fin (vertexBound (k := k) (radix D w.length))) (b : Fin 2) :
+    (coinTable machine D w).getD
+        (2 * (u.val * vertexBound (k := k) (radix D w.length) + v.val) + b.val) false =
+      decide (b.val < coinCountWithSymbol machine (radix D w.length) w.length u v
+        w[queryIndex (k := k) (radix D w.length) u]?) := by
+  let p := finProdFinEquiv (u, finProdFinEquiv (v, b))
+  have hp : 2 * (u.val * vertexBound (k := k) (radix D w.length) + v.val) + b.val = p.val := by
+    simp only [p, finProdFinEquiv, Equiv.coe_fn_mk]
+    ring
+  rw [hp]
+  dsimp only [coinTable]
+  simp_rw [List.flatMap_ofFn_prod]
+  rw [List.getD_eq_getElem _ _ (by simp), List.getElem_ofFn]
+  simp only [Fin.eta, p, Equiv.symm_apply_apply]
+
+/-- Summing the two stored bits recovers the exact count, including coincident successors. -/
+theorem coinTable_count (u v : Fin (vertexBound (k := k) (radix D w.length))) :
+    ((coinTable machine D w).getD
+        (2 * (u.val * vertexBound (k := k) (radix D w.length) + v.val)) false).toNat +
+      ((coinTable machine D w).getD
+        (2 * (u.val * vertexBound (k := k) (radix D w.length) + v.val) + 1) false).toNat =
+      coinCountWithSymbol machine (radix D w.length) w.length u v
+        w[queryIndex (k := k) (radix D w.length) u]? := by
+  have h0 := getD_coinTable machine D w u v 0
+  have h1 := getD_coinTable machine D w u v 1
+  simp only [Fin.val_zero, Fin.val_one, Nat.add_zero] at h0 h1
+  rw [h0, h1]
+  have hc := coinCountWithSymbol_le_two machine (radix D w.length) w.length u v
+    w[queryIndex (k := k) (radix D w.length) u]?
+  interval_cases coinCountWithSymbol machine (radix D w.length) w.length u v
+    w[queryIndex (k := k) (radix D w.length) u]? <;> rfl
+
+/-- The initialized writer. The header occupies labels zero to three, the two loops start at
+four and seven, the count reader starts at ten, and labels sixteen to twenty-one emit its bits.
+Label twenty-two halts. The four registers are length, row, column, and count scratch. -/
+@[expose] noncomputable def coinTableProgram : CounterProgram where
+  code :=
+    Words.headerCode ++
+    forCode 4 1 (vertexBoundExpr k (radixExpr D (reg 0))) 7 22 ++
+    forCode 7 2 (vertexBoundExpr k (radixExpr D (reg 0))) 10 6 ++
+    coinCountCode machine D 10 16 ++
+    [lt (const 0) (reg 3) 17 18, emit true 19, emit false 19,
+     lt (const 1) (reg 3) 20 21, emit true 9, emit false 9, halt []]
+  registers := 4
+
+variable {machine D w} {S : ℕ}
+
+private theorem bounded_regs {a b c d : ℕ} (ha : a ≤ S) (hb : b ≤ S)
+    (hc : c ≤ S) (hd : d ≤ S) : ∀ r ∈ [a, b, c, d], r ≤ S := by
+  simp only [List.mem_cons, List.not_mem_nil, or_false]
+  omega
+
+private theorem reachesOut_entry {u v y : ℕ}
+    (hregs : ∀ r ∈ [w.length, u, v, y], r ≤ S) (h2 : 2 ≤ S) :
+    let c := coinCountWithSymbol machine (radix D w.length) w.length u v
+      w[queryIndex (k := k) (radix D w.length) u]?
+    (coinTableProgram machine D).ReachesOut (frame w) ((coinTableProgram machine D).Active S)
+      (10, [w.length, u, v, y]) (9, [w.length, u, v, c])
+      [decide (0 < c), decide (1 < c)] := by
+  let P := coinTableProgram machine D
+  let c := coinCountWithSymbol machine (radix D w.length) w.length u v
+    w[queryIndex (k := k) (radix D w.length) u]?
+  have hc : c ≤ 2 := coinCountWithSymbol_le_two ..
+  have hb : ∀ r ∈ [w.length, u, v, c], r ≤ S :=
+    bounded_regs (hregs _ (by simp)) (hregs _ (by simp)) (hregs _ (by simp)) (hc.trans h2)
+  have hcode : P.CodeAt 10 (coinCountCode machine D 10 16) := by
+    simp only [coinCountCode, readSymbolCode, codeAt_append,
+      codeAt_cons, codeAt_nil, and_true]
+    exact ⟨⟨rfl, rfl, rfl, rfl, rfl⟩, rfl⟩
+  have hr := reachesOut_coinCountCode machine hcode hregs h2
+  have hfirst : P.ReachesOut (frame w) (P.Active S)
+      (16, [w.length, u, v, c]) (19, [w.length, u, v, c]) [decide (0 < c)] := by
+    refine ReachesOut.lt (show P.instr 16 = _ from rfl) hb ?_
+    simp only [eval_const, eval_reg, List.getD_cons_zero, List.getD_cons_succ]
+    by_cases h : 0 < c
+    · simpa [h] using ReachesOut.emit (show P.instr 17 = _ from rfl) hb (ReachesOut.refl _)
+    · simpa [h] using ReachesOut.emit (show P.instr 18 = _ from rfl) hb (ReachesOut.refl _)
+  have hsecond : P.ReachesOut (frame w) (P.Active S)
+      (19, [w.length, u, v, c]) (9, [w.length, u, v, c]) [decide (1 < c)] := by
+    refine ReachesOut.lt (show P.instr 19 = _ from rfl) hb ?_
+    simp only [eval_const, eval_reg, List.getD_cons_zero, List.getD_cons_succ]
+    by_cases h : 1 < c
+    · simpa [h] using ReachesOut.emit (show P.instr 20 = _ from rfl) hb (ReachesOut.refl _)
+    · simpa [h] using ReachesOut.emit (show P.instr 21 = _ from rfl) hb (ReachesOut.refl _)
+  exact (hr.trans (hfirst.trans hsecond)).of_eq (by simp [c])
+
+private theorem reachesOut_row
+    (hL : w.length ≤ S) (hN : vertexBound (k := k) (radix D w.length) ≤ S) (h2 : 2 ≤ S)
+    {u x y : ℕ} (hu : u < vertexBound (k := k) (radix D w.length))
+    (hx : x ≤ vertexBound (k := k) (radix D w.length)) (hy : y ≤ 2) :
+    ∃ y' ≤ 2, (coinTableProgram machine D).ReachesOut (frame w)
+      ((coinTableProgram machine D).Active S)
+      (7, [w.length, u, x, y])
+      (6, [w.length, u, vertexBound (k := k) (radix D w.length), y'])
+      ((List.range (vertexBound (k := k) (radix D w.length))).flatMap fun v =>
+        let c := coinCountWithSymbol machine (radix D w.length) w.length u v
+          w[queryIndex (k := k) (radix D w.length) u]?
+        [decide (0 < c), decide (1 < c)]) := by
+  have hcode : (coinTableProgram machine D).CodeAt 7
+      (forCode 7 2 (vertexBoundExpr k (radixExpr D (reg 0))) 10 6) := by
+    simp only [forCode, codeAt_cons, codeAt_nil, and_true]
+    exact ⟨rfl, rfl, rfl⟩
+  obtain ⟨regs', hreach, y', rfl, -, hy'⟩ := reachesOut_forCode (w := frame w)
+    (o := fun v =>
+      let c := coinCountWithSymbol machine (radix D w.length) w.length u v
+        w[queryIndex (k := k) (radix D w.length) u]?
+      [decide (0 < c), decide (1 < c)])
+    (N := vertexBound (k := k) (radix D w.length)) hcode
+    (fun v regs => ∃ y, regs = [w.length, u, v, y] ∧
+      v ≤ vertexBound (k := k) (radix D w.length) ∧ y ≤ 2) hN
+    (by
+      rintro v regs ⟨y, rfl, hv, hy⟩
+      exact ⟨rfl, by simp, by simp, bounded_regs hL (by omega) (by omega) (by omega)⟩)
+    (by
+      rintro v hv regs ⟨y, rfl, -, hy⟩
+      let c := coinCountWithSymbol machine (radix D w.length) w.length u v
+        w[queryIndex (k := k) (radix D w.length) u]?
+      have hc : c ≤ 2 := coinCountWithSymbol_le_two ..
+      exact ⟨[w.length, u, v, c],
+        reachesOut_entry (bounded_regs hL (by omega) (by omega) (by omega)) h2,
+        rfl, bounded_regs hL (by omega) (by omega) (hc.trans h2), c, by simp, by omega, hc⟩)
+    [w.length, u, x, y] (bounded_regs hL (by omega) (by omega) (by omega))
+    ⟨y, by simp, by omega, hy⟩
+  exact ⟨y', hy', hreach⟩
+
+private theorem reachesOut_table
+    (hL : w.length ≤ S) (hN : vertexBound (k := k) (radix D w.length) ≤ S) (h2 : 2 ≤ S) :
+    ∃ regs, (coinTableProgram machine D).ReachesOut (frame w)
+      ((coinTableProgram machine D).Active S)
+      (4, [w.length, 0, 0, 0]) (22, regs) (coinTable machine D w) ∧
+      ∀ r ∈ regs, r ≤ S := by
+  have hcode : (coinTableProgram machine D).CodeAt 4
+      (forCode 4 1 (vertexBoundExpr k (radixExpr D (reg 0))) 7 22) := by
+    simp only [forCode, codeAt_cons, codeAt_nil, and_true]
+    exact ⟨rfl, rfl, rfl⟩
+  obtain ⟨regs', hreach, x, y, rfl, -, hx, hy⟩ := reachesOut_forCode (w := frame w)
+    (o := fun u => (List.range (vertexBound (k := k) (radix D w.length))).flatMap fun v =>
+      let c := coinCountWithSymbol machine (radix D w.length) w.length u v
+        w[queryIndex (k := k) (radix D w.length) u]?
+      [decide (0 < c), decide (1 < c)])
+    (N := vertexBound (k := k) (radix D w.length)) hcode
+    (fun u regs => ∃ x y, regs = [w.length, u, x, y] ∧
+      u ≤ vertexBound (k := k) (radix D w.length) ∧
+      x ≤ vertexBound (k := k) (radix D w.length) ∧ y ≤ 2) hN
+    (by
+      rintro u regs ⟨x, y, rfl, hu, hx, hy⟩
+      exact ⟨rfl, by simp, by simp, bounded_regs hL (by omega) (by omega) (by omega)⟩)
+    (by
+      rintro u hu regs ⟨x, y, rfl, -, hx, hy⟩
+      obtain ⟨y', hy', hr⟩ := reachesOut_row (machine := machine) hL hN h2 hu hx hy
+      exact ⟨_, hr, rfl, bounded_regs hL (by omega) (by omega) (by omega),
+        _, y', by simp, by omega, le_rfl, hy'⟩)
+    [w.length, 0, 0, 0] (bounded_regs hL (by omega) (by omega) (by omega))
+    ⟨0, 0, by simp, by omega, by omega, by omega⟩
+  exact ⟨_, hreach.of_eq (coinTable_eq_flatMap machine D w).symm,
+    bounded_regs hL (by omega) (by omega) (by omega)⟩
+
+variable (machine D w)
+
+/-- The actual zero-initialized program counts the input length, enumerates every compact pair,
+emits the whole table, and reaches its halt with all final registers within the common bound. -/
+theorem reachesOut_coinTableProgram
+    (hinput : (frame w).length ≤ S)
+    (hN : vertexBound (k := k) (radix D w.length) ≤ S) (h2 : 2 ≤ S) :
+    ∃ regs, (coinTableProgram machine D).ReachesOut (frame w)
+      ((coinTableProgram machine D).Active S) (coinTableProgram machine D).init
+      (22, regs) (coinTable machine D w) ∧ ∀ r ∈ regs, r ≤ S := by
+  have hcode : (coinTableProgram machine D).CodeAt 0 Words.headerCode := by
+    simp only [Words.headerCode, codeAt_cons, codeAt_nil, and_true]
+    exact ⟨rfl, rfl, rfl, rfl⟩
+  have hh := Words.reachesOut_header (w := w) (k := 0) hcode (by
+    simpa only [length_frame, Nat.add_zero] using hinput)
+  simp only [List.replicate_zero, List.append_nil] at hh
+  have hL : w.length ≤ S := by rw [length_frame] at hinput; omega
+  obtain ⟨regs, hr, hregs⟩ := reachesOut_table (machine := machine) hL hN h2
+  exact ⟨regs, (hh.trans hr).of_eq (by simp), hregs⟩
+
+/-- The entire compact coin table is computed from the original framed word in native
+deterministic logarithmic space. No parameters or counters are preloaded. -/
+theorem computableInLogSpace_coinTable :
+    ComputableInLogSpace (coinTable machine D) (encFramed encBits) encBits := by
+  refine (coinTableProgram machine D).computableInLogSpace_of_reachesOut
+    (D * Fintype.card (Register k) + 1) fun w => ?_
+  simp only [encFramed_apply, encBits_apply]
+  obtain ⟨hN, _, h2⟩ := configurationCounter_bounds (k := k) D w
+  have hinput : (frame w).length ≤
+      ((frame w).length + 1) ^ (D * Fintype.card (Register k) + 1) := by
+    rw [pow_succ]
+    have hone : 1 ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k)) :=
+      Nat.one_le_pow _ _ (by omega)
+    exact (Nat.le_succ _).trans (Nat.le_mul_of_pos_left _ hone)
+  obtain ⟨regs, hr, hregs⟩ := reachesOut_coinTableProgram machine D w hinput (by omega) h2
+  exact ⟨(22, regs), _, [], hr, rfl, by simp, hregs⟩
+
+end Turing.MultiTapePTM.ConfigurationGraph
diff --git a/ComplexityTests/FairCoinTable.lean b/ComplexityTests/FairCoinTable.lean
new file mode 100644
index 000000000..e1f117f30
--- /dev/null
+++ b/ComplexityTests/FairCoinTable.lean
@@ -0,0 +1,171 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.Table
+import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationReader
+
+/-!
+# Initialized fair-coin table runs
+
+A concrete machine's entire 1458-bit table is emitted from zero registers on its original framed
+one-bit input. At one fixed row and column, the two output bits change from `[true, false]` to
+`[false, false]` when only the original input bit changes, and to `[true, true]` when the two coin
+successors coincide. The output index is the ordinary row-major index, not an assumed oracle.
+The empty input and exponent-zero compact box also have actual initialized runs.
+-/
+
+namespace ComplexityTests.FairCoinTable
+
+open Cslib.Turing Turing MultiTapeTM CounterProgram Instr
+open MultiTapeNTM.ConfigurationGraph MultiTapePTM.ConfigurationGraph
+
+private def machine (different : Bool) : MultiTapePTM 0 Bool Unit where
+  initial := ()
+  tr _ symbol _ _ bit :=
+    .step
+      { inputTape := 0
+        workTapes := Fin.elim0
+        output := some (symbol.getD false && (if different then bit else true))
+        state := none }
+      Empty.elim Empty.elim
+
+private def running (input : Bool) : FiniteCfg 0 Bool Unit :=
+  ⟨[input], some (), 1, Fin.elim0, []⟩
+
+private def stopped (input output : Bool) : FiniteCfg 0 Bool Unit :=
+  ⟨[input], none, 1, Fin.elim0, [output]⟩
+
+private theorem viewCoinStep_running (different input bit : Bool) :
+    (machine different).viewCoinStep (running input) bit =
+      stopped input (input && (if different then bit else true)) := by
+  cases different <;> cases input <;> cases bit <;>
+    simp [MultiTapePTM.viewCoinStep, running, FiniteCfg.inputSymbol_eq_getD, machine,
+      MultiTapePTM.withCoin, MultiTapeMachine.toTM, MultiTapeMachine.Action.emptyOracleEquiv,
+      FiniteCfg.step, FiniteCfg.summarizeOutput, MultiTapeNTM.outputClass, stopped, funext_iff]
+
+private theorem stopped_injective (input : Bool) : Function.Injective (stopped input) := by
+  intro a b h
+  have ho := congrArg FiniteCfg.output h
+  simpa only [stopped, List.cons.injEq, and_true] using ho
+
+private theorem fits_three (v : FiniteCfg 0 Bool Unit) (hinput : v.input.length = 1) :
+    Fits 3 (registers v) := by
+  intro i
+  cases i with
+  | inputPos =>
+    change v.inputPos.val < 3
+    simpa only [hinput] using v.inputPos.isLt
+  | control =>
+    have h : stateCode v.state < 2 := (Fintype.equivFin (Option Unit) v.state).isLt
+    exact h.trans_le (by decide)
+  | output => exact outputCode_lt _
+  | head i => exact Fin.elim0 i
+  | left i => exact Fin.elim0 i
+  | right i => exact Fin.elim0 i
+
+private noncomputable def source : ℕ := vertexID 3 (running true)
+
+private noncomputable def target : ℕ := vertexID 3 (stopped true true)
+
+private noncomputable def address : ℕ := 2 * (source * 27 + target)
+
+-- Input symbols are absent from the compact IDs, so all runs use the same table address.
+example (input : Bool) : vertexID 3 (running input) = source ∧
+    vertexID 3 (stopped input true) = target := ⟨rfl, rfl⟩
+
+private theorem count_input (different input : Bool) :
+    coinCountWithSymbol (machine different) 3 1 source target
+      [input][queryIndex (k := 0) 3 source]? =
+        if input then (if different then 1 else 2) else 0 := by
+  change coinCountWithSymbol (machine different) 3 1
+    (vertexID 3 (running input)) (vertexID 3 (stopped input true))
+    [input][queryIndex (k := 0) 3 (vertexID 3 (running input))]? = _
+  have hcoin (bit : Bool) := edgeWithSymbol_withCoin_iff (machine different)
+    (a := running input) (b := stopped input true) rfl
+    (by simp [running, MultiTapeNTM.outputClass])
+    (by simp [stopped, MultiTapeNTM.outputClass])
+    (fits_three _ rfl) (fits_three _ rfl) bit
+  simp only [viewCoinStep_running, (stopped_injective input).eq_iff] at hcoin
+  have hfalse := hcoin false
+  have htrue := hcoin true
+  rw [coinCountWithSymbol]
+  cases input <;> cases different <;> simp_all [running]
+
+private theorem table_bits (different input : Bool) :
+    (coinTable (machine different) 1 [input]).getD address false = input ∧
+      (coinTable (machine different) 1 [input]).getD (address + 1) false =
+        (input && !different) := by
+  have hbox : vertexBound (k := 0) 3 = 27 := by decide
+  have hu : source < vertexBound (k := 0) 3 := vertexID_lt (fits_three (running true) rfl)
+  have hv : target < vertexBound (k := 0) 3 := vertexID_lt (fits_three (stopped true true) rfl)
+  let u : Fin (vertexBound (k := 0) (radix 1 [input].length)) := ⟨source, hu⟩
+  let v : Fin (vertexBound (k := 0) (radix 1 [input].length)) := ⟨target, hv⟩
+  have h0 := getD_coinTable (machine different) 1 [input] u v 0
+  have h1 := getD_coinTable (machine different) 1 [input] u v 1
+  change (coinTable (machine different) 1 [input]).getD
+    (2 * (source * vertexBound (k := 0) 3 + target) + 0) false =
+      decide (0 < coinCountWithSymbol (machine different) 3 1 source target
+        [input][queryIndex (k := 0) 3 source]?) at h0
+  change (coinTable (machine different) 1 [input]).getD
+    (2 * (source * vertexBound (k := 0) 3 + target) + 1) false =
+      decide (1 < coinCountWithSymbol (machine different) 3 1 source target
+        [input][queryIndex (k := 0) 3 source]?) at h1
+  rw [hbox, count_input] at h0 h1
+  cases input <;> cases different <;> simp_all [address]
+
+private theorem initialized_run (different input : Bool) :
+    ∃ regs out, (coinTableProgram (machine different) 1).ReachesOut (frame [input])
+      ((coinTableProgram (machine different) 1).Active 27)
+      (0, [0, 0, 0, 0]) (22, regs) out ∧
+      out.length = 1458 ∧ out.getD address false = input ∧
+      out.getD (address + 1) false = (input && !different) := by
+  obtain ⟨regs, hr, _⟩ := reachesOut_coinTableProgram (machine different) 1 [input]
+    (S := 27) (by simp) (by change 27 ≤ 27; rfl) (by decide)
+  exact ⟨regs, coinTable (machine different) 1 [input], hr,
+    by rw [length_coinTable]; change 2 * 27 ^ 2 = 1458; norm_num, (table_bits different input).1,
+    (table_bits different input).2⟩
+
+-- One accepting coin, with all parameters counted or enumerated from zero registers.
+example : ∃ regs out, (coinTableProgram (machine true) 1).ReachesOut (frame [true])
+    ((coinTableProgram (machine true) 1).Active 27)
+    (0, [0, 0, 0, 0]) (22, regs) out ∧
+    out.length = 1458 ∧ out.getD address false = true ∧
+    out.getD (address + 1) false = false := initialized_run true true
+
+-- Changing just the original input bit changes the same table entry to count zero.
+example : ∃ regs out, (coinTableProgram (machine true) 1).ReachesOut (frame [false])
+    ((coinTableProgram (machine true) 1).Active 27)
+    (0, [0, 0, 0, 0]) (22, regs) out ∧
+    out.length = 1458 ∧ out.getD address false = false ∧
+    out.getD (address + 1) false = false := initialized_run true false
+
+-- The same entry records two when the two coin successors coincide.
+example : ∃ regs out, (coinTableProgram (machine false) 1).ReachesOut (frame [true])
+    ((coinTableProgram (machine false) 1).Active 27)
+    (0, [0, 0, 0, 0]) (22, regs) out ∧
+    out.length = 1458 ∧ out.getD address false = true ∧
+    out.getD (address + 1) false = true := initialized_run false true
+
+-- Empty original input still counts its marker correctly and emits all 8 × 8 entries.
+example : ∃ regs out, (coinTableProgram (machine true) 1).ReachesOut (frame [])
+    ((coinTableProgram (machine true) 1).Active 8)
+    (0, [0, 0, 0, 0]) (22, regs) out ∧ out.length = 128 := by
+  obtain ⟨regs, hr, _⟩ := reachesOut_coinTableProgram (machine true) 1 []
+    (S := 8) (by decide) (by decide) (by decide)
+  exact ⟨regs, _, hr, by rw [length_coinTable]; decide⟩
+
+-- Exponent zero produces a one-entry ambient box, with the count scratch still bounded by two.
+example : ∃ regs out, (coinTableProgram (machine true) 0).ReachesOut (frame [])
+    ((coinTableProgram (machine true) 0).Active 2)
+    (0, [0, 0, 0, 0]) (22, regs) out ∧ out.length = 2 := by
+  obtain ⟨regs, hr, _⟩ := reachesOut_coinTableProgram (machine true) 0 []
+    (S := 2) (by decide) (by decide) (by decide)
+  exact ⟨regs, _, hr, by rw [length_coinTable]; decide⟩
+
+-- The final label is a halt; the entire counted table is emitted before reaching it.
+example (different : Bool) : (coinTableProgram (machine different) 1).instr 22 = halt [] := rfl
+
+end ComplexityTests.FairCoinTable