diff --git a/Complexity.lean b/Complexity.lean
index 8f5f9ddb1e..cb913e27a7 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1094,6 +1094,7 @@ public import Complexity.Computability.Complexity.Classes.LogSpace.PolyTime
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.Amplification
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.BPP
+public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ClockedTable
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.CompactMatrix
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.CompactTimeLayer
 public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationMatrix
@@ -1578,9 +1579,12 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Deterministic
 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.Clocked
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.ClockedTable
 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.InputTable
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Radix
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.ReadSymbol
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Routines
@@ -2696,6 +2700,7 @@ public import Complexity.Foundations.Data.List.OfFn
 public import Complexity.Foundations.Data.List.Range
 public import Complexity.Foundations.Data.List.RowMajor
 public import Complexity.Foundations.Data.List.SelectDistinct
+public import Complexity.Foundations.Data.List.TwoBitTable
 public import Complexity.Foundations.Data.Matrix.Binary
 public import Complexity.Foundations.Data.Matrix.IntegerBits
 public import Complexity.Foundations.Data.Matrix.PairChunks
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ClockedTable.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ClockedTable.lean
new file mode 100644
index 0000000000..9d46fd1db7
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ClockedTable.lean
@@ -0,0 +1,81 @@
+/-
+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.Complexity.Classes.LogSpace.Randomized.CompactTimeLayer
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin.ClockedTable
+
+/-!
+# Exact interpretation of the initialized clocked coin table
+
+The two threshold bits emitted by `clockedCoinTableProgram` recover every entry of the existing
+`Matrix.finTimeLayer` of the actual compact coin matrix. This includes invalid configurations,
+off-clock entries and terminal rows; no represented-view or reachability premise is needed.
+The finite terminal reward also agrees with the local `clockedAccept` computation.
+
+Together with `computableInLogSpace_clockedCoinTable`, this gives native initialized serialization
+of the matrix payload in the canonical BPL construction. A complete serialized instance with
+dimension, start and reward fields, directed paired ports, and the native estimator remain open.
+
+## Main results
+
+* `Turing.MultiTapePTM.ConfigurationGraph.finTimeLayer_compactCoinMatrix_eq_clockedCoinCount`:
+  every clocked matrix entry is half the guarded base count.
+* `Turing.MultiTapePTM.ConfigurationGraph.finTimeLayer_compactCoinMatrix_eq_clockedCoinTable`:
+  the initialized native output gives every clocked matrix entry exactly.
+* `Turing.MultiTapePTM.ConfigurationGraph.finTimeLayerReward_eq_clockedAccept`:
+  the terminal reward equals its local native predicate.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM.ConfigurationGraph
+
+open MultiTapeNTM.ConfigurationGraph Matrix
+
+variable {k : ℕ} {State : Type} [Fintype State] {machine : MultiTapePTM k Bool State}
+  {R : Type*} [Field R]
+
+/-- Every numeric clocked entry is half the guarded base count, including invalid IDs and
+terminal rows. The input symbol is read at the base source's input position. -/
+theorem finTimeLayer_compactCoinMatrix_eq_clockedCoinCount (B T : ℕ) (w : List Bool)
+    (u v : Fin ((T + 1) * vertexBound (k := k) B)) :
+    finTimeLayer T (compactCoinMatrix machine R B w) u v =
+      (clockedCoinCountWithSymbol machine B w.length u v
+        w[queryIndex (k := k) B (u.val % vertexBound (k := k) B)]? : R) / 2 := by
+  rw [finTimeLayer_apply]
+  dsimp only [clockedCoinCountWithSymbol, compactCoinMatrix]
+  split_ifs <;> simp
+
+/-- The two output bits at the row-major address give the exact finite time-layer matrix entry.
+This interprets the initialized writer's payload on the same consecutive IDs as the BPL theorem. -/
+theorem finTimeLayer_compactCoinMatrix_eq_clockedCoinTable (D d : ℕ) (w : List Bool)
+    (u v : Fin (clockedVertexBound (k := k) D d w.length)) :
+    finTimeLayer (2 * (2 * (w.length + 1)) ^ d)
+        (compactCoinMatrix machine R (radix D w.length) w) u v =
+      (((clockedCoinTable machine D d w).getD
+          (2 * (u.val * clockedVertexBound (k := k) D d w.length + v.val)) false).toNat +
+        ((clockedCoinTable machine D d w).getD
+          (2 * (u.val * clockedVertexBound (k := k) D d w.length + v.val) + 1)
+          false).toNat : ℕ) / 2 := by
+  rw [clockedCoinTable_count]
+  exact finTimeLayer_compactCoinMatrix_eq_clockedCoinCount _ _ _ _ _
+
+/-- The terminal reward on consecutive IDs is the local native accepting-ID predicate.
+This equality concerns the value, without packaging it into the matrix payload. -/
+theorem finTimeLayerReward_eq_clockedAccept (B n T : ℕ)
+    (u : Fin ((T + 1) * vertexBound (k := k) B)) :
+    finTimeLayerReward T (compactAcceptVec (k := k) (State := State) R B n) u =
+      ((clockedAccept (k := k) (State := State) B n T u).toNat : R) := by
+  change (if u.val / vertexBound (k := k) B = T then
+    (if bad (k := k) (State := State) B n (u.val % vertexBound (k := k) B) then 1 else 0)
+    else 0) = _
+  dsimp only [clockedAccept]
+  split_ifs <;> simp_all
+
+end Turing.MultiTapePTM.ConfigurationGraph
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactMatrix.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactMatrix.lean
index 5f7ba706cf..c774b21086 100644
--- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactMatrix.lean
+++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactMatrix.lean
@@ -23,8 +23,9 @@ For a logarithmic-space run the box contains every reachable view; restriction t
 image therefore proves exact finite-time acceptance for the ambient matrix.
 
 This supplies the enumerated base matrix of [OpenAI2026LogSpace, Lemma 2.1]. Clocking and the
-terminal reward are treated separately. Native clocked serialization, paired ports and the
-recursive estimator are not asserted here.
+terminal reward are treated separately; `Randomized.ClockedTable` supplies the initialized native
+clocked matrix payload. Complete instance packaging, paired ports and the recursive estimator
+remain separate.
 
 ## Main definitions
 
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactTimeLayer.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactTimeLayer.lean
index 3c2cd9c082..77bcdc6b94 100644
--- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactTimeLayer.lean
+++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/CompactTimeLayer.lean
@@ -23,7 +23,8 @@ acceptance gap at the encoded initial configuration.
 The endpoint preserves the original logarithmic-space constant and derives the fitting radix
 from it. It does not choose an arbitrary ordering of reachable views. The ordinary entries are
 the counts written by the native initialized table, via `compactCoinMatrix_eq_coinTable`.
-Native clocked serialization, paired ports and the native recursive estimator remain open.
+The initialized clocked payload is supplied by `Randomized.ClockedTable`. Complete instance
+packaging, paired ports and the native recursive estimator remain open.
 
 ## Main results
 
@@ -75,8 +76,8 @@ clock/base IDs, gives a real strict-forward substochastic matrix and a terminal
 bounded inverse potential has the original acceptance gap. The dimension is explicitly polynomial.
 
 The space witness is produced by this theorem, and all radix, start and representation bounds
-are derived from it. This is a semantic bridge for the existing initialized ordinary table;
-it does not assert native clocked serialization or incoming paired-port computation. -/
+are derived from it. `Randomized.ClockedTable` supplies the initialized native matrix payload;
+complete instance packaging and incoming paired-port computation remain separate. -/
 theorem exists_compactTimeLayer_of_mem_BPL (h : A ∈ BPL enc) :
     ∃ (k : ℕ) (State : Type) (_ : Fintype State) (M : MultiTapePTM k Bool State) (c d : ℕ),
       ∀ a, ∃ hs : M.toNTM.RunsInSpace (enc a) (c * (Nat.log2 (enc a).length + 1)),
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Clocked.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Clocked.lean
new file mode 100644
index 0000000000..4a5723ef57
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Clocked.lean
@@ -0,0 +1,162 @@
+/-
+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.ConfigurationGraph.CounterBounds
+
+/-!
+# Local arithmetic for clocked compact configurations
+
+A clocked identifier is `clock * N + baseID`, with `N = vertexBound B`. Division and remainder
+recover the clock and base ID. A transition has the existing fair-coin count exactly when the
+target clock is the next one; every other count is zero. The polynomial horizon and terminal
+acceptance test also have native space-budget certificates on their short binary arguments.
+
+The start at clock zero retains its ordinary numeric ID, so the existing `startID_budget`
+applies unchanged. These local certificates do not serialize a complete matrix-instance header,
+reward vector or start field. The initialized matrix payload is supplied by `ClockedTable`.
+
+## Main definitions
+
+* `Turing.MultiTapeNTM.ConfigurationGraph.clockedVertexBound`: the polynomial clocked box size.
+* `Turing.MultiTapeNTM.ConfigurationGraph.clockedAccept`: the terminal accepting-ID test.
+* `Turing.MultiTapePTM.ConfigurationGraph.clockedCoinCountWithSymbol`: the guarded clocked count.
+* `Turing.MultiTapePTM.ConfigurationGraph.clockedCoinCountExpr`: its arithmetic expression.
+
+## Main results
+
+* `Turing.MultiTapeNTM.ConfigurationGraph.clockedVertexBound_budget`,
+  `Turing.MultiTapeNTM.ConfigurationGraph.clockedAccept_budget`: local native space certificates.
+* `Turing.MultiTapePTM.ConfigurationGraph.clockedCoinCountWithSymbol_le_two`: count bound.
+* `Turing.MultiTapePTM.ConfigurationGraph.eval_clockedCoinCountExpr`: exact expression evaluation.
+-/
+
+public section
+
+namespace Turing.MultiTapeNTM.ConfigurationGraph
+
+open CounterProgram Expr MultiTapeTM ComputableInSpace
+
+variable {k : ℕ}
+
+/-- Number of compact clock/base pairs at the standard polynomial horizon. -/
+@[expose] def clockedVertexBound (D d n : ℕ) : ℕ :=
+  (2 * (2 * (n + 1)) ^ d + 1) * vertexBound (k := k) (radix D n)
+
+/-- The dimension as a counter expression in the original word length. -/
+noncomputable def clockedVertexBoundExpr (k D d : ℕ) (n : Expr) : Expr :=
+  mul (add (mul (const 2) (pow (mul (const 2) (add n (const 1))) d)) (const 1))
+    (vertexBoundExpr k (radixExpr D n))
+
+/-- The dimension expression has exactly the polynomial clocked-box value. -/
+@[simp] theorem eval_clockedVertexBoundExpr (k D d : ℕ) (n : Expr) (regs : List ℕ) :
+    (clockedVertexBoundExpr k D d n).eval regs = clockedVertexBound (k := k) D d (n.eval regs) := by
+  simp [clockedVertexBoundExpr, clockedVertexBound]
+
+/-- The last layer pays the accepting-halt indicator of the base compact ID. -/
+@[expose] noncomputable def clockedAccept {State : Type} [Fintype State] (B n T u : ℕ) : Bool :=
+  if u / vertexBound (k := k) B = T then
+    bad (k := k) (State := State) B n (u % vertexBound (k := k) B) else false
+
+variable {α : Type} {enc : α ↪ List Bool} {S : α → ℕ} {B n T u : α → ℕ}
+
+/-- Computing the clocked dimension preserves any common native space budget for the input
+length. The exponents are fixed with the source machine. -/
+theorem clockedVertexBound_budget (D d : ℕ) (hn : ComputableInSpace n enc encNat S)
+    (hin : (fun a => (enc a).length) ≼ S) :
+    ComputableInSpace (fun a => clockedVertexBound (k := k) D d (n a)) enc encNat S := by
+  have htwo : ComputableInSpace (fun _ : α => 2) enc encNat S := budget_const 2 hin
+  exact budget_natMul
+    (budget_natSucc (budget_natMul htwo
+      (budget_natPow (budget_natMul htwo (budget_natSucc hn)) hin d)))
+    (vertexBound_budget (k := k) (budget_natPow (budget_natAdd hn htwo) hin D) hin)
+
+/-- The terminal reward test preserves the native space budget of its binary arguments. -/
+theorem clockedAccept_budget {State : Type} [Fintype State]
+    (hB : ComputableInSpace B enc encNat S) (hn : ComputableInSpace n enc encNat S)
+    (hT : ComputableInSpace T enc encNat S) (hu : ComputableInSpace u enc encNat S)
+    (hin : (fun a => (enc a).length) ≼ S) :
+    ComputableInSpace (fun a => clockedAccept (k := k) (State := State)
+      (B a) (n a) (T a) (u a)) enc encBool S := by
+  have hN := vertexBound_budget (k := k) hB hin
+  simpa only [clockedAccept, decide_eq_true_eq] using
+    budget_ite (budget_natEq (budget_natDiv hu hN) hT)
+      (bad_budget (State := State) hB hn (budget_natMod hu hN) hin) (budget_const false hin)
+
+end Turing.MultiTapeNTM.ConfigurationGraph
+
+namespace Turing.MultiTapePTM.ConfigurationGraph
+
+open MultiTapeNTM.ConfigurationGraph CounterProgram Expr MultiTapeTM ComputableInSpace
+
+variable {k : ℕ} {State : Type} [Fintype State]
+
+/-- The ordinary base-ID coin count on a next-clock pair, and zero otherwise. No represented
+view premise is required; the base-ID predicates still guard invalid configurations. -/
+@[expose] noncomputable def clockedCoinCountWithSymbol (machine : MultiTapePTM k Bool State)
+    (B n u v : ℕ) (symbol : Option Bool) : ℕ :=
+  let N := vertexBound (k := k) B
+  if u / N + 1 = v / N then coinCountWithSymbol machine B n (u % N) (v % N) symbol else 0
+
+/-- Clock gating preserves the exact zero/one/two range of a fair-coin count. -/
+theorem clockedCoinCountWithSymbol_le_two (machine : MultiTapePTM k Bool State)
+    (B n u v : ℕ) (symbol : Option Bool) :
+    clockedCoinCountWithSymbol machine B n u v symbol ≤ 2 := by
+  dsimp only [clockedCoinCountWithSymbol]
+  split_ifs
+  · exact coinCountWithSymbol_le_two ..
+  · decide
+
+/-- Every terminal row has zero count at every bounded clocked target, regardless of validity
+or reachability of either base configuration. -/
+theorem clockedCoinCountWithSymbol_terminal (machine : MultiTapePTM k Bool State)
+    {B n T : ℕ} (u v : Fin ((T + 1) * vertexBound (k := k) B))
+    (hu : u.val / vertexBound (k := k) B = T) (symbol : Option Bool) :
+    clockedCoinCountWithSymbol machine B n u v symbol = 0 := by
+  have hv : v.val / vertexBound (k := k) B < T + 1 := v.divNat.isLt
+  dsimp only [clockedCoinCountWithSymbol]
+  rw [hu, ite_eq_right (by omega)]
+
+/-- Clock division, base remainders and the same coin-count expression form one arithmetic
+expression. The symbol is still read separately from the original input at the base source. -/
+noncomputable def clockedCoinCountExpr (machine : MultiTapePTM k Bool State)
+    (B n u v sym : Expr) : Expr :=
+  let N := vertexBoundExpr k B
+  iteB (eqB (add (div u N) (const 1)) (div v N))
+    (coinCountExpr machine B n (mod u N) (mod v N) sym) (const 0)
+
+/-- The clocked expression is exactly the guarded count, including off-clock pairs. -/
+theorem eval_clockedCoinCountExpr (machine : MultiTapePTM k Bool State)
+    {B n u v sym : Expr} {regs : List ℕ} {symbol : Option Bool}
+    (hs : sym.eval regs = symbolCode symbol) :
+    (clockedCoinCountExpr machine B n u v sym).eval regs =
+      clockedCoinCountWithSymbol machine (B.eval regs) (n.eval regs) (u.eval regs) (v.eval regs)
+        symbol := by
+  rw [clockedCoinCountExpr, eval_iteB eval_eqB, eval_coinCountExpr machine hs]
+  simp only [eval_add, eval_div, eval_const, eval_vertexBoundExpr, eval_mod,
+    decide_eq_true_eq, clockedCoinCountWithSymbol]
+
+variable {α : Type} {enc : α ↪ List Bool} {S : α → ℕ}
+  {B n u v : α → ℕ} {symbol : α → Option Bool}
+
+/-- The local clocked count has the same native space-budget contract as its base count. -/
+theorem clockedCoinCountWithSymbol_budget (machine : MultiTapePTM k Bool State)
+    (hB : ComputableInSpace B enc encNat S) (hn : ComputableInSpace n enc encNat S)
+    (hu : ComputableInSpace u enc encNat S) (hv : ComputableInSpace v enc encNat S)
+    (hs : ComputableInSpace symbol enc (encOption encBool) S)
+    (hin : (fun a => (enc a).length) ≼ S) :
+    ComputableInSpace (fun a => clockedCoinCountWithSymbol machine
+      (B a) (n a) (u a) (v a) (symbol a)) enc encNat S := by
+  have hN := vertexBound_budget (k := k) hB hin
+  simpa only [clockedCoinCountWithSymbol, decide_eq_true_eq] using
+    budget_ite (budget_natEq (budget_natSucc (budget_natDiv hu hN)) (budget_natDiv hv hN))
+      (coinCountWithSymbol_budget machine hB hn (budget_natMod hu hN)
+        (budget_natMod hv hN) hs hin) (budget_const 0 hin)
+
+end Turing.MultiTapePTM.ConfigurationGraph
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/ClockedTable.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/ClockedTable.lean
new file mode 100644
index 0000000000..c9ed3de0f2
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/ClockedTable.lean
@@ -0,0 +1,159 @@
+/-
+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.Clocked
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.InputTable
+
+/-!
+# Native initialized serialization of the clocked coin matrix
+
+`clockedCoinTable` stores two threshold bits for every ordered pair of numeric clock/base IDs.
+At horizon `T = 2 * (2 * (n + 1)) ^ d`, the dimension is `(T + 1) * N`, where `N` is the
+ordinary compact box. The count is the existing base count on remainders exactly when the
+target quotient is one greater than the source quotient. Thus terminal rows are zero.
+
+`clockedCoinTableProgram` uses the same header, loops, original-input reader and emitter as
+the ordinary table. It starts from zero registers on `frame w`, queries using the base source,
+and emits the full table in native logarithmic space. Only the bound, query and value expressions
+differ. The exact semantic matrix interpretation is in `Randomized.ClockedTable`.
+
+This output is the matrix payload. A complete serialized instance containing dimension, start
+and reward fields, directed paired ports, and the native estimator remain separate.
+
+## Main definitions
+
+* `Turing.MultiTapePTM.ConfigurationGraph.clockedCoinTable`: the two-bit matrix payload.
+* `Turing.MultiTapePTM.ConfigurationGraph.clockedCoinTableProgram`: its initialized writer.
+
+## Main results
+
+* `Turing.MultiTapePTM.ConfigurationGraph.length_clockedCoinTable`,
+  `Turing.MultiTapePTM.ConfigurationGraph.getD_clockedCoinTable`,
+  `Turing.MultiTapePTM.ConfigurationGraph.clockedCoinTable_count`: exact length and decoding.
+* `Turing.MultiTapePTM.ConfigurationGraph.reachesOut_clockedCoinTableProgram`: bounded run.
+* `Turing.MultiTapePTM.ConfigurationGraph.computableInLogSpace_clockedCoinTable`: native space.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM.ConfigurationGraph
+
+open MultiTapeNTM.ConfigurationGraph CounterProgram Expr MultiTapeTM
+
+variable {k : ℕ} {State : Type} [Fintype State]
+
+/-- Every pair of clock/base IDs, with two threshold bits encoding the next-clock coin count.
+The one original-input read uses the base source, obtained by remainder modulo the base box. -/
+noncomputable def clockedCoinTable (machine : MultiTapePTM k Bool State)
+    (D d : ℕ) (w : List Bool) : List Bool :=
+  let B := radix D w.length
+  let N := vertexBound (k := k) B
+  List.twoBitTable (clockedVertexBound (k := k) D d w.length) fun u v =>
+    clockedCoinCountWithSymbol machine B w.length u v w[queryIndex (k := k) B (u % N)]?
+
+variable (machine : MultiTapePTM k Bool State) (D d : ℕ) (w : List Bool)
+
+/-- Exactly two bits are emitted for every ordered pair of clocked IDs. -/
+@[simp] theorem length_clockedCoinTable :
+    (clockedCoinTable machine D d w).length =
+      2 * clockedVertexBound (k := k) D d w.length ^ 2 := by
+  simp only [clockedCoinTable, List.length_twoBitTable]
+
+/-- Each bit at its row-major address is the corresponding exact clocked-count threshold. -/
+theorem getD_clockedCoinTable (u v : Fin (clockedVertexBound (k := k) D d w.length))
+    (b : Fin 2) :
+    (clockedCoinTable machine D d w).getD
+        (2 * (u.val * clockedVertexBound (k := k) D d w.length + v.val) + b.val) false =
+      decide (b.val < clockedCoinCountWithSymbol machine (radix D w.length) w.length u v
+        w[queryIndex (k := k) (radix D w.length)
+          (u.val % vertexBound (k := k) (radix D w.length))]?) := by
+  simpa only [clockedCoinTable] using List.getD_twoBitTable
+    (clockedVertexBound (k := k) D d w.length)
+    (fun u v => clockedCoinCountWithSymbol machine (radix D w.length) w.length u v
+      w[queryIndex (k := k) (radix D w.length)
+        (u % vertexBound (k := k) (radix D w.length))]?) u v b
+
+/-- Summing the two bits recovers the exact count, including two coincident coin branches. -/
+theorem clockedCoinTable_count (u v : Fin (clockedVertexBound (k := k) D d w.length)) :
+    ((clockedCoinTable machine D d w).getD
+        (2 * (u.val * clockedVertexBound (k := k) D d w.length + v.val)) false).toNat +
+      ((clockedCoinTable machine D d w).getD
+        (2 * (u.val * clockedVertexBound (k := k) D d w.length + v.val) + 1) false).toNat =
+      clockedCoinCountWithSymbol machine (radix D w.length) w.length u v
+        w[queryIndex (k := k) (radix D w.length)
+          (u.val % vertexBound (k := k) (radix D w.length))]? := by
+  simpa only [clockedCoinTable] using List.count_twoBitTable
+    (clockedVertexBound (k := k) D d w.length)
+    (fun u v => clockedCoinCountWithSymbol machine (radix D w.length) w.length u v
+      w[queryIndex (k := k) (radix D w.length)
+        (u % vertexBound (k := k) (radix D w.length))]?) u v
+    (clockedCoinCountWithSymbol_le_two ..)
+
+/-- Both encoded bits are zero throughout a terminal row, for every bounded target ID. -/
+theorem getD_clockedCoinTable_terminal
+    (u v : Fin (clockedVertexBound (k := k) D d w.length)) (b : Fin 2)
+    (hu : u.val / vertexBound (k := k) (radix D w.length) =
+      2 * (2 * (w.length + 1)) ^ d) :
+    (clockedCoinTable machine D d w).getD
+      (2 * (u.val * clockedVertexBound (k := k) D d w.length + v.val) + b.val) false = false := by
+  rw [getD_clockedCoinTable, clockedCoinCountWithSymbol_terminal machine u v hu]
+  simp
+
+/-- The same 23-label four-register writer as the ordinary table, with clocked arithmetic.
+Registers are length, flat row, flat column and scratch; no parameter is preloaded. -/
+@[expose] noncomputable def clockedCoinTableProgram : CounterProgram :=
+  inputCountTableProgram (clockedVertexBoundExpr k D d (reg 0))
+    (queryIndexExpr k (radixExpr D (reg 0))
+      (mod (reg 1) (vertexBoundExpr k (radixExpr D (reg 0)))))
+    (clockedCoinCountExpr machine (radixExpr D (reg 0)) (reg 0) (reg 1) (reg 2) (reg 3))
+
+variable {S : ℕ}
+
+/-- Starting from the actual zeroed initializer on the original frame, the writer emits the
+whole clocked table and reaches label twenty-two with all registers within the common bound. -/
+theorem reachesOut_clockedCoinTableProgram (hinput : (frame w).length ≤ S)
+    (hN : clockedVertexBound (k := k) D d w.length ≤ S) (h2 : 2 ≤ S) :
+    ∃ regs, (clockedCoinTableProgram machine D d).ReachesOut (frame w)
+      ((clockedCoinTableProgram machine D d).Active S) (clockedCoinTableProgram machine D d).init
+      (22, regs) (clockedCoinTable machine D d w) ∧ ∀ r ∈ regs, r ≤ S := by
+  apply reachesOut_inputCountTableProgram
+    (count := fun u v => clockedCoinCountWithSymbol machine (radix D w.length) w.length u v
+      w[queryIndex (k := k) (radix D w.length)
+        (u % vertexBound (k := k) (radix D w.length))]?)
+    (fun u v y => by simp) ?_ (fun u v => clockedCoinCountWithSymbol_le_two ..) hinput hN h2
+  intro u v y
+  simpa only [eval_queryIndexExpr, eval_radixExpr, eval_reg, eval_mod, eval_vertexBoundExpr,
+    List.getD_cons_zero, List.getD_cons_succ] using
+      eval_clockedCoinCountExpr machine (B := radixExpr D (reg 0))
+        (n := reg 0) (u := reg 1) (v := reg 2) (sym := reg 3)
+        (regs := [w.length, u, v, symbolCode w[queryIndex (k := k) (radix D w.length)
+          (u % vertexBound (k := k) (radix D w.length))]?]) rfl
+
+/-- The entire clocked matrix payload is computed in native deterministic logarithmic space
+from the original framed word, with no preloaded length, clock or configuration IDs. -/
+theorem computableInLogSpace_clockedCoinTable :
+    ComputableInLogSpace (clockedCoinTable machine D d) (encFramed encBits) encBits := by
+  refine (clockedCoinTableProgram machine D d).computableInLogSpace_of_reachesOut
+    (D * Fintype.card (Register k) + d + 2) fun w => ?_
+  simp only [encFramed_apply, encBits_apply]
+  have hframe : (frame w).length + 1 = 2 * (w.length + 1) := by rw [length_frame]; omega
+  have hN : clockedVertexBound (k := k) D d w.length + 1 ≤
+      ((frame w).length + 1) ^ (D * Fintype.card (Register k) + d + 2) := by
+    simpa only [clockedVertexBound, hframe] using
+      clockedVertexBound_add_one_le_pow (k := k) D d w.length
+  have hF : (frame w).length + 1 ≤
+      ((frame w).length + 1) ^ (D * Fintype.card (Register k) + d + 2) :=
+    le_self_pow (by omega) (by omega)
+  have h2 : 2 ≤ ((frame w).length + 1) ^ (D * Fintype.card (Register k) + d + 2) :=
+    (by rw [hframe]; omega : 2 ≤ (frame w).length + 1).trans hF
+  obtain ⟨regs, hr, hregs⟩ := reachesOut_clockedCoinTableProgram machine D d w
+    ((Nat.le_succ _).trans hF) (by omega) h2
+  exact ⟨(22, regs), _, [], hr, rfl, by simp, hregs⟩
+
+end Turing.MultiTapePTM.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
index 0d2733d780..ce8cc4f343 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Table.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/Table.lean
@@ -8,9 +8,8 @@ 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
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.InputTable
 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
@@ -21,12 +20,13 @@ 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.
+counter loops, and evaluates the shared `coinCountExpr` after reading each entry's original input
+symbol. 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.
+predicate's behavior. The clocked writer reuses the same program in `FairCoin.ClockedTable`;
+paired ports and the recursive estimator remain separate.
 
 ## Main definitions
 
@@ -56,9 +56,8 @@ noncomputable def coinTable (machine : MultiTapePTM k Bool State) (D : ℕ) (w :
     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]?)
+  List.twoBitTable N fun u v =>
+    coinCountWithSymbol machine B w.length u v w[queryIndex (k := k) B u]?
 
 variable (machine : MultiTapePTM k Bool State) (D : ℕ) (w : List Bool)
 
@@ -70,24 +69,16 @@ theorem coinTable_eq_flatMap :
           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]
+  simpa only [coinTable] using List.twoBitTable_eq_flatMap
+    (vertexBound (k := k) (radix D w.length))
+    (fun u v => coinCountWithSymbol machine (radix D w.length) w.length u v
+      w[queryIndex (k := k) (radix D w.length) u]?)
 
 /-- 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
+  simp only [coinTable, List.length_twoBitTable]
 
 /-- Reading either bit at its ordinary row-major address returns the corresponding threshold. -/
 theorem getD_coinTable
@@ -96,15 +87,10 @@ theorem getD_coinTable
         (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]
+  simpa only [coinTable] using List.getD_twoBitTable
+    (vertexBound (k := k) (radix D w.length))
+    (fun u v => coinCountWithSymbol machine (radix D w.length) w.length u v
+      w[queryIndex (k := k) (radix D w.length) u]?) u v b
 
 /-- 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))) :
@@ -114,140 +100,21 @@ theorem coinTable_count (u v : Fin (vertexBound (k := k) (radix D w.length))) :
         (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
+  simpa only [coinTable] using List.count_twoBitTable
+    (vertexBound (k := k) (radix D w.length))
+    (fun u v => coinCountWithSymbol machine (radix D w.length) w.length u v
+      w[queryIndex (k := k) (radix D w.length) u]?) u v (coinCountWithSymbol_le_two ..)
 
 /-- 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
+@[expose] noncomputable def coinTableProgram : CounterProgram :=
+  inputCountTableProgram (vertexBoundExpr k (radixExpr D (reg 0)))
+    (queryIndexExpr k (radixExpr D (reg 0)) (reg 1))
+    (coinCountExpr machine (radixExpr D (reg 0)) (reg 0) (reg 1) (reg 2) (reg 3))
 
 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,
@@ -258,15 +125,17 @@ theorem reachesOut_coinTableProgram
     ∃ 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⟩
+  apply reachesOut_inputCountTableProgram
+    (count := fun u v => coinCountWithSymbol machine (radix D w.length) w.length u v
+      w[queryIndex (k := k) (radix D w.length) u]?)
+    (fun u v y => by simp) ?_ (fun u v => coinCountWithSymbol_le_two ..) hinput hN h2
+  intro u v y
+  simpa only [eval_queryIndexExpr, eval_radixExpr, eval_reg,
+    List.getD_cons_zero, List.getD_cons_succ] using
+      eval_coinCountExpr machine (B := radixExpr D (reg 0))
+        (n := reg 0) (u := reg 1) (v := reg 2) (sym := reg 3)
+        (regs := [w.length, u, v, symbolCode
+          w[queryIndex (k := k) (radix D w.length) u]?]) rfl
 
 /-- The entire compact coin table is computed from the original framed word in native
 deterministic logarithmic space. No parameters or counters are preloaded. -/
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/InputTable.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/InputTable.lean
new file mode 100644
index 0000000000..4550c7117b
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/InputTable.lean
@@ -0,0 +1,191 @@
+/-
+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.ReadSymbol
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Words
+public import Complexity.Foundations.Data.List.TwoBitTable
+
+/-!
+# Initialized two-bit table writers with original-input queries
+
+One four-register counter program reads the original word length, enumerates a square table,
+reads one original input symbol per entry and emits the two threshold bits of an arithmetic count.
+The bound, query and count are expressions; the header, loops, reader and emitter are shared.
+This is the existing ordinary fair-coin table program factored for its clocked client.
+
+Registers zero through three hold the word length, row, column and scratch. The input must be
+`frame w`; the program starts from its actual zeroed initializer. The expression contracts below
+are discharged by each client, including the requirement that the count be at most two.
+
+## Main definitions
+
+* `Turing.MultiTapeNTM.ConfigurationGraph.inputCountTableProgram`: the shared initialized writer.
+
+## Main results
+
+* `Turing.MultiTapeNTM.ConfigurationGraph.reachesOut_inputCountTableProgram`: bounded initialized
+  execution emits exactly the shared row-major `List.twoBitTable` representation.
+-/
+
+public section
+
+namespace Turing.MultiTapeNTM.ConfigurationGraph
+
+open CounterProgram Instr Expr MultiTapeTM
+
+/-- The header occupies labels zero to three, loops start at four and seven, the input read at
+ten, and count assignment at fifteen. Labels sixteen through twenty-one emit its two bits;
+twenty-two halts. Registers hold length, row, column and symbol/count scratch. -/
+@[expose] def inputCountTableProgram (bound query value : Expr) : CounterProgram where
+  code :=
+    Words.headerCode ++ forCode 4 1 bound 7 22 ++ forCode 7 2 bound 10 6 ++
+    readSymbolCode 10 3 15 (reg 0) query ++ [assign 3 value 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 {bound query value : Expr} {w : List Bool} {N S : ℕ} {count : ℕ → ℕ → ℕ}
+  (hbound : ∀ u v y, bound.eval [w.length, u, v, y] = N)
+  (hvalue : ∀ u v y,
+    value.eval [w.length, u, v, symbolCode w[query.eval [w.length, u, v, y]]?] = count u v)
+  (hcount : ∀ u v, count u v ≤ 2)
+
+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
+
+include hvalue in
+private theorem reachesOut_count {u v y : ℕ}
+    (hregs : ∀ r ∈ [w.length, u, v, y], r ≤ S) (h2 : 2 ≤ S) :
+    (inputCountTableProgram bound query value).ReachesOut (frame w)
+      ((inputCountTableProgram bound query value).Active S)
+      (10, [w.length, u, v, y]) (16, [w.length, u, v, count u v]) [] := by
+  let P := inputCountTableProgram bound query value
+  let sym := symbolCode w[query.eval [w.length, u, v, y]]?
+  have hcode : P.CodeAt 10 (readSymbolCode 10 3 15 (reg 0) query) := by
+    simp only [readSymbolCode, codeAt_cons, codeAt_nil, and_true]
+    exact ⟨rfl, rfl, rfl, rfl, rfl⟩
+  have hr : P.ReachesOut (frame w) (P.Active S)
+      (10, [w.length, u, v, y]) (15, [w.length, u, v, sym]) [] := by
+    simpa [sym] using reachesOut_readSymbolCode hcode rfl hregs
+  have hb : ∀ r ∈ [w.length, u, v, sym], r ≤ S :=
+    bounded_regs (hregs _ (by simp)) (hregs _ (by simp)) (hregs _ (by simp))
+      ((Nat.le_of_lt_succ (symbolCode_lt _)).trans h2)
+  refine (hr.trans (ReachesOut.assign (show P.instr 15 = _ from rfl) hb ?_)).of_eq rfl
+  rw [hvalue]
+  exact ReachesOut.refl _
+
+include hvalue hcount in
+private theorem reachesOut_entry {u v y : ℕ}
+    (hregs : ∀ r ∈ [w.length, u, v, y], r ≤ S) (h2 : 2 ≤ S) :
+    (inputCountTableProgram bound query value).ReachesOut (frame w)
+      ((inputCountTableProgram bound query value).Active S)
+      (10, [w.length, u, v, y]) (9, [w.length, u, v, count u v])
+      [decide (0 < count u v), decide (1 < count u v)] := by
+  let P := inputCountTableProgram bound query value
+  let c := count u v
+  have hb : ∀ r ∈ [w.length, u, v, c], r ≤ S :=
+    bounded_regs (hregs _ (by simp)) (hregs _ (by simp)) (hregs _ (by simp))
+      ((hcount u v).trans h2)
+  have hr := reachesOut_count (bound := bound) hvalue 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])
+
+include hbound hvalue hcount in
+private theorem reachesOut_row (hL : w.length ≤ S) (hN : N ≤ S) (h2 : 2 ≤ S)
+    {u x y : ℕ} (hu : u < N) (hx : x ≤ N) (hy : y ≤ 2) :
+    ∃ y' ≤ 2, (inputCountTableProgram bound query value).ReachesOut (frame w)
+      ((inputCountTableProgram bound query value).Active S)
+      (7, [w.length, u, x, y]) (6, [w.length, u, N, y'])
+      ((List.range N).flatMap fun v => [decide (0 < count u v), decide (1 < count u v)]) := by
+  have hcode : (inputCountTableProgram bound query value).CodeAt 7
+      (forCode 7 2 bound 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 => [decide (0 < count u v), decide (1 < count u v)]) (N := N) hcode
+    (fun v regs => ∃ y, regs = [w.length, u, v, y] ∧ v ≤ N ∧ y ≤ 2) hN
+    (by
+      rintro v regs ⟨y, rfl, hv, hy⟩
+      exact ⟨rfl, hbound u v y, by simp, bounded_regs hL (by omega) (by omega) (by omega)⟩)
+    (by
+      rintro v hv regs ⟨y, rfl, -, hy⟩
+      have hc := hcount u v
+      exact ⟨[w.length, u, v, count u v],
+        reachesOut_entry hvalue hcount
+          (bounded_regs hL (by omega) (by omega) (by omega)) h2,
+        rfl, bounded_regs hL (by omega) (by omega) (hc.trans h2),
+        count u v, 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⟩
+
+include hbound hvalue hcount in
+private theorem reachesOut_table (hL : w.length ≤ S) (hN : N ≤ S) (h2 : 2 ≤ S) :
+    ∃ regs, (inputCountTableProgram bound query value).ReachesOut (frame w)
+      ((inputCountTableProgram bound query value).Active S)
+      (4, [w.length, 0, 0, 0]) (22, regs) (List.twoBitTable N count) ∧
+      ∀ r ∈ regs, r ≤ S := by
+  have hcode : (inputCountTableProgram bound query value).CodeAt 4
+      (forCode 4 1 bound 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 N).flatMap fun v =>
+      [decide (0 < count u v), decide (1 < count u v)]) (N := N) hcode
+    (fun u regs => ∃ x y, regs = [w.length, u, x, y] ∧ u ≤ N ∧ x ≤ N ∧ y ≤ 2) hN
+    (by
+      rintro u regs ⟨x, y, rfl, hu, hx, hy⟩
+      exact ⟨rfl, hbound u x y, 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 hbound hvalue hcount 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 (List.twoBitTable_eq_flatMap N count).symm,
+    bounded_regs hL (by omega) (by omega) (by omega)⟩
+
+include hbound hvalue hcount in
+/-- Starting from zero registers on the original framed word, the shared writer emits exactly
+the specified two-bit count table and reaches its halt. The three expression contracts state
+that the bound is fixed by the input length and that each actual read produces the intended
+count at most two. All registers stay within the supplied common bound before halting. -/
+theorem reachesOut_inputCountTableProgram
+    (hinput : (frame w).length ≤ S) (hN : N ≤ S) (h2 : 2 ≤ S) :
+    ∃ regs, (inputCountTableProgram bound query value).ReachesOut (frame w)
+      ((inputCountTableProgram bound query value).Active S)
+      (inputCountTableProgram bound query value).init
+      (22, regs) (List.twoBitTable N count) ∧ ∀ r ∈ regs, r ≤ S := by
+  have hcode : (inputCountTableProgram bound query value).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 hbound hvalue hcount hL hN h2
+  exact ⟨regs, (hh.trans hr).of_eq (by simp), hregs⟩
+
+end Turing.MultiTapeNTM.ConfigurationGraph
diff --git a/Complexity/Foundations/Data/List/TwoBitTable.lean b/Complexity/Foundations/Data/List/TwoBitTable.lean
new file mode 100644
index 0000000000..8286a885ad
--- /dev/null
+++ b/Complexity/Foundations/Data/List/TwoBitTable.lean
@@ -0,0 +1,91 @@
+/-
+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.Foundations.Data.List.RowMajor
+import Mathlib.Data.List.Basic
+import Mathlib.Data.List.GetD
+import Mathlib.Tactic.IntervalCases
+import Mathlib.Tactic.Ring
+
+/-!
+# Row-major tables of two-bit counts
+
+Store a square table in row-major order, with the two threshold bits `0 < c` and `1 < c` at
+each entry. Counts zero, one and two are exactly `[false, false]`, `[true, false]` and
+`[true, true]`; larger counts saturate. The ordinary and clocked compact-configuration writers
+share this output specification and its indexing lemmas.
+
+## Main definitions
+
+* `List.twoBitTable`: the row-major two-threshold representation.
+
+## Main results
+
+* `List.length_twoBitTable`, `List.getD_twoBitTable`: exact length and addressing.
+* `List.count_twoBitTable`: recover a count that is at most two.
+* `List.twoBitTable_eq_flatMap`: agreement with natural-counter enumeration.
+-/
+
+public section
+
+namespace List
+
+/-- Two consecutive threshold bits for each entry, enumerated in row-major order. -/
+@[expose] def twoBitTable (N : ℕ) (count : ℕ → ℕ → ℕ) : List Bool :=
+  (finRange N).flatMap fun u : Fin N => (finRange N).flatMap fun v : Fin N =>
+    ofFn fun b : Fin 2 => decide (b.val < count u v)
+
+variable (N : ℕ) (count : ℕ → ℕ → ℕ)
+
+/-- Finite-index enumeration equals the natural-counter loops used by a writer. -/
+theorem twoBitTable_eq_flatMap :
+    twoBitTable N count = (range N).flatMap fun u => (range N).flatMap fun v =>
+      [decide (0 < count u v), decide (1 < count u v)] := by
+  have hval (n : ℕ) : (finRange n).map Fin.val = range n := by
+    apply List.ext_getElem <;> simp
+  dsimp only [twoBitTable]
+  conv_rhs => rw [← hval]; simp only [flatMap_map]
+  apply flatMap_congr
+  intro u _
+  apply flatMap_congr
+  intro v _
+  simp [ofFn_succ]
+
+/-- Exactly two bits are stored for each ordered pair of indices. -/
+@[simp] theorem length_twoBitTable : (twoBitTable N count).length = 2 * N ^ 2 := by
+  dsimp only [twoBitTable]
+  simp_rw [flatMap_ofFn_prod]
+  simp only [length_ofFn]
+  ring
+
+/-- Reading a bit at its row-major address recovers the corresponding threshold. -/
+theorem getD_twoBitTable (u v : Fin N) (b : Fin 2) :
+    (twoBitTable N count).getD (2 * (u.val * N + v.val) + b.val) false =
+      decide (b.val < count u v) := by
+  let p := finProdFinEquiv (u, finProdFinEquiv (v, b))
+  have hp : 2 * (u.val * N + v.val) + b.val = p.val := by
+    simp only [p, finProdFinEquiv, Equiv.coe_fn_mk]
+    ring
+  rw [hp]
+  dsimp only [twoBitTable]
+  simp_rw [flatMap_ofFn_prod]
+  rw [getD_eq_getElem _ _ (by simp), List.getElem_ofFn]
+  simp only [Fin.eta, p, Equiv.symm_apply_apply]
+
+/-- The sum of an entry's two stored bits recovers any count at most two. -/
+theorem count_twoBitTable (u v : Fin N) (hcount : count u v ≤ 2) :
+    ((twoBitTable N count).getD (2 * (u.val * N + v.val)) false).toNat +
+      ((twoBitTable N count).getD (2 * (u.val * N + v.val) + 1) false).toNat = count u v := by
+  have h0 := getD_twoBitTable N count u v 0
+  have h1 := getD_twoBitTable N count u v 1
+  simp only [Fin.val_zero, Fin.val_one, Nat.add_zero] at h0 h1
+  rw [h0, h1]
+  interval_cases count u v <;> rfl
+
+end List
diff --git a/ComplexityTests/ClockedCoinTable.lean b/ComplexityTests/ClockedCoinTable.lean
new file mode 100644
index 0000000000..1526da37d8
--- /dev/null
+++ b/ComplexityTests/ClockedCoinTable.lean
@@ -0,0 +1,223 @@
+/-
+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.Complexity.Classes.LogSpace.Randomized.ClockedTable
+
+/-!
+# Initialized clocked coin-table regressions
+
+An empty-input, zero-work-tape machine gives a small nonzero table: three clock layers of an
+eight-ID base box, with 1152 output bits. The actual zero-initialized writer emits one or two at
+the same pair from clock one to clock two, depending on whether the coin successors coincide.
+Off-clock pairs and terminal rows give zero. The decoded bits recover the semantic matrix entry.
+The ordinary writer is definitionally the same 23-label program after extracting the shared code.
+-/
+
+namespace ComplexityTests.ClockedCoinTable
+
+open Cslib.Turing Turing MultiTapeTM CounterProgram Instr Expr Matrix
+open MultiTapeNTM.ConfigurationGraph MultiTapePTM.ConfigurationGraph
+
+private def machine (different : Bool) : MultiTapePTM 0 Bool Unit where
+  initial := ()
+  tr _ _ _ _ bit :=
+    .step
+      { inputTape := 0
+        workTapes := Fin.elim0
+        output := some (if different then bit else true)
+        state := none }
+      Empty.elim Empty.elim
+
+private def running : FiniteCfg 0 Bool Unit := ⟨[], some (), 1, Fin.elim0, []⟩
+
+private def stopped (output : Bool) : FiniteCfg 0 Bool Unit :=
+  ⟨[], none, 1, Fin.elim0, [output]⟩
+
+private theorem viewCoinStep_running (different bit : Bool) :
+    (machine different).viewCoinStep running bit = stopped (if different then bit else true) := by
+  cases different <;> cases bit <;>
+    simp [MultiTapePTM.viewCoinStep, running, machine, MultiTapePTM.withCoin,
+      MultiTapeMachine.toTM, MultiTapeMachine.Action.emptyOracleEquiv,
+      FiniteCfg.step, FiniteCfg.summarizeOutput, MultiTapeNTM.outputClass, stopped, funext_iff]
+
+private theorem stopped_injective : Function.Injective stopped := by
+  intro a b h
+  have ho := congrArg FiniteCfg.output h
+  simpa only [stopped, List.cons.injEq, and_true] using ho
+
+private theorem running_fits : Fits 2 (registers running) := by
+  intro i
+  cases i with
+  | inputPos => decide
+  | control => exact (Fintype.equivFin (Option Unit) (some ())).isLt
+  | output => decide
+  | head i => exact Fin.elim0 i
+  | left i => exact Fin.elim0 i
+  | right i => exact Fin.elim0 i
+
+private theorem stopped_fits : Fits 2 (registers (stopped true)) := by
+  intro i
+  cases i with
+  | inputPos => decide
+  | control => exact (Fintype.equivFin (Option Unit) none).isLt
+  | output => decide
+  | head i => exact Fin.elim0 i
+  | left i => exact Fin.elim0 i
+  | right i => exact Fin.elim0 i
+
+private noncomputable def source : Fin 8 := ⟨vertexID 2 running, vertexID_lt running_fits⟩
+private noncomputable def target : Fin 8 := ⟨vertexID 2 (stopped true), vertexID_lt stopped_fits⟩
+
+private noncomputable def clockSource : Fin 24 :=
+  ⟨8 + source.val, by have h := source.isLt; omega⟩
+
+private noncomputable def clockTarget : Fin 24 :=
+  ⟨16 + target.val, by have h := target.isLt; omega⟩
+
+private noncomputable def address : ℕ := 2 * (clockSource.val * 24 + clockTarget.val)
+
+private theorem count_base (different : Bool) :
+    coinCountWithSymbol (machine different) 2 0 source target none =
+      if different then 1 else 2 := by
+  have hcoin (bit : Bool) := edgeWithSymbol_withCoin_iff (machine different)
+    (a := running) (b := stopped true) rfl
+    (by simp [running, MultiTapeNTM.outputClass])
+    (by simp [stopped, MultiTapeNTM.outputClass]) running_fits stopped_fits bit
+  simp only [viewCoinStep_running, stopped_injective.eq_iff] at hcoin
+  have hfalse := hcoin false
+  have htrue := hcoin true
+  change edgeWithSymbol ((machine different).withCoin false).toTM.toMultiTapeNTM
+    2 0 source target none = true ↔ _ at hfalse
+  change edgeWithSymbol ((machine different).withCoin true).toTM.toMultiTapeNTM
+    2 0 source target none = true ↔ _ at htrue
+  rw [coinCountWithSymbol]
+  cases different <;> simp_all
+
+private theorem count_clocked (different : Bool) :
+    clockedCoinCountWithSymbol (machine different) 2 0 clockSource clockTarget none =
+      if different then 1 else 2 := by
+  have hs := source.isLt
+  have ht := target.isLt
+  have hsdiv : clockSource.val / 8 = 1 := by dsimp only [clockSource]; omega
+  have htdiv : clockTarget.val / 8 = 2 := by dsimp only [clockTarget]; omega
+  have hsmod : clockSource.val % 8 = source := by dsimp only [clockSource]; omega
+  have htmod : clockTarget.val % 8 = target := by dsimp only [clockTarget]; omega
+  change (if clockSource.val / 8 + 1 = clockTarget.val / 8 then
+    coinCountWithSymbol (machine different) 2 0 (clockSource.val % 8)
+      (clockTarget.val % 8) none else 0) = _
+  rw [hsdiv, htdiv, hsmod, htmod]
+  simpa only [ite_true] using count_base different
+
+private theorem table_bits (different : Bool) :
+    (clockedCoinTable (machine different) 1 0 []).getD address false = true ∧
+      (clockedCoinTable (machine different) 1 0 []).getD (address + 1) false = !different := by
+  have h0 := getD_clockedCoinTable (machine different) 1 0 [] clockSource clockTarget 0
+  have h1 := getD_clockedCoinTable (machine different) 1 0 [] clockSource clockTarget 1
+  change (clockedCoinTable (machine different) 1 0 []).getD
+    (2 * (clockSource.val * 24 + clockTarget.val) + 0) false =
+      decide (0 < clockedCoinCountWithSymbol (machine different) 2 0
+        clockSource clockTarget none) at h0
+  change (clockedCoinTable (machine different) 1 0 []).getD
+    (2 * (clockSource.val * 24 + clockTarget.val) + 1) false =
+      decide (1 < clockedCoinCountWithSymbol (machine different) 2 0
+        clockSource clockTarget none) at h1
+  rw [count_clocked] at h0 h1
+  cases different <;> simp_all [address]
+
+private theorem initialized_run (different : Bool) :
+    ∃ regs out, (clockedCoinTableProgram (machine different) 1 0).ReachesOut (frame [])
+      ((clockedCoinTableProgram (machine different) 1 0).Active 24)
+      (0, [0, 0, 0, 0]) (22, regs) out ∧
+      out.length = 1152 ∧ out.getD address false = true ∧
+      out.getD (address + 1) false = !different := by
+  obtain ⟨regs, hr, _⟩ := reachesOut_clockedCoinTableProgram (machine different) 1 0 []
+    (S := 24) (by decide) (by decide) (by decide)
+  exact ⟨regs, _, hr, by rw [length_clockedCoinTable]; decide,
+    (table_bits different).1, (table_bits different).2⟩
+
+-- One accepting successor at a source in clock one, with no preloaded length or IDs.
+example : ∃ regs out, (clockedCoinTableProgram (machine true) 1 0).ReachesOut (frame [])
+    ((clockedCoinTableProgram (machine true) 1 0).Active 24)
+    (0, [0, 0, 0, 0]) (22, regs) out ∧
+    out.length = 1152 ∧ out.getD address false = true ∧
+    out.getD (address + 1) false = false := initialized_run true
+
+-- Coincident successors retain count two at the same clocked entry.
+example : ∃ regs out, (clockedCoinTableProgram (machine false) 1 0).ReachesOut (frame [])
+    ((clockedCoinTableProgram (machine false) 1 0).Active 24)
+    (0, [0, 0, 0, 0]) (22, regs) out ∧
+    out.length = 1152 ∧ out.getD address false = true ∧
+    out.getD (address + 1) false = true := initialized_run false
+
+-- Same-clock targets are zero even when the underlying base transition has nonzero count.
+example (different : Bool) (b : Fin 2) :
+    (clockedCoinTable (machine different) 1 0 []).getD
+      (2 * (clockSource.val * 24 + (8 + target.val)) + b.val) false = false := by
+  let v : Fin 24 := ⟨8 + target.val, by have h := target.isLt; omega⟩
+  have h := getD_clockedCoinTable (machine different) 1 0 [] clockSource v b
+  have hs := source.isLt
+  have ht := target.isLt
+  have hclock : clockSource.val / 8 + 1 ≠ v.val / 8 := by
+    dsimp only [clockSource, v]
+    omega
+  change (clockedCoinTable (machine different) 1 0 []).getD
+    (2 * (clockSource.val * 24 + (8 + target.val)) + b.val) false =
+      decide (b.val < if clockSource.val / 8 + 1 = v.val / 8 then _ else 0) at h
+  simpa only [ite_eq_right hclock, Nat.not_lt_zero, decide_false] using h
+
+-- Every column of the terminal row is zero, without assuming a valid target configuration.
+example (different : Bool) (v : Fin 24) (b : Fin 2) :
+    (clockedCoinTable (machine different) 1 0 []).getD
+      (2 * (clockTarget.val * 24 + v.val) + b.val) false = false := by
+  apply getD_clockedCoinTable_terminal
+  change clockTarget.val / 8 = 2
+  have h := target.isLt
+  dsimp only [clockTarget]
+  omega
+
+-- The actual initialized output decodes to the existing semantic matrix, in a field.
+example (different : Bool) :
+    finTimeLayer 2 (compactCoinMatrix (machine different) ℚ 2 []) clockSource clockTarget =
+      if different then 1 / 2 else 1 := by
+  have h := finTimeLayer_compactCoinMatrix_eq_clockedCoinTable
+    (machine := machine different) (R := ℚ) 1 0 [] clockSource clockTarget
+  change finTimeLayer 2 (compactCoinMatrix (machine different) ℚ 2 []) clockSource clockTarget =
+    (((clockedCoinTable (machine different) 1 0 []).getD address false).toNat +
+      ((clockedCoinTable (machine different) 1 0 []).getD (address + 1) false).toNat : ℕ) / 2 at h
+  rw [h, (table_bits different).1, (table_bits different).2]
+  cases different <;> norm_num
+
+-- The local native reward predicate selects the accepting target at the terminal clock.
+example :
+    finTimeLayerReward 2 (compactAcceptVec (k := 0) (State := Unit) ℚ 2 0) clockTarget = 1 ∧
+      clockedAccept (k := 0) (State := Unit) 2 0 2 clockTarget = true := by
+  have ht := target.isLt
+  have hdiv : clockTarget.val / 8 = 2 := by dsimp only [clockTarget]; omega
+  have hmod : clockTarget.val % 8 = target := by dsimp only [clockTarget]; omega
+  have hb : bad (k := 0) (State := Unit) 2 0 target = true :=
+    (bad_vertexID stopped_fits).mpr ⟨rfl, rfl⟩
+  have hc : clockedAccept (k := 0) (State := Unit) 2 0 2 clockTarget = true := by
+    change (if clockTarget.val / 8 = 2 then
+      bad (k := 0) (State := Unit) 2 0 (clockTarget.val % 8) else false) = true
+    rw [hdiv, hmod]
+    simpa only [ite_true] using hb
+  have hr := finTimeLayerReward_eq_clockedAccept (k := 0) (State := Unit) (R := ℚ)
+    2 0 2 clockTarget
+  rw [hc] at hr
+  exact ⟨by simpa using hr, hc⟩
+
+-- The ordinary writer's instruction list and register count are definitionally preserved.
+example {k : ℕ} {State : Type} [Fintype State] (M : MultiTapePTM k Bool State) (D : ℕ) :
+    coinTableProgram M D =
+      { 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 M 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 } := rfl
+
+end ComplexityTests.ClockedCoinTable