diff --git a/Complexity.lean b/Complexity.lean
index 9196f243f..e4d8a2192 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1552,8 +1552,10 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Correctness
 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.Injective
 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
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Tape
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Configurations
diff --git a/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean b/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean
index 8020124d9..5472e8800 100644
--- a/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean
+++ b/Complexity/Computability/Complexity/Problems/STCON/Reduction.lean
@@ -10,9 +10,8 @@ module
 public import Complexity.Computability.Complexity.Problems.STCON
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Expr
-public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Output
+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.Encodings.Frame
 
 /-!
 # The configuration graph as an instance of directed connectivity
@@ -192,13 +191,9 @@ noncomputable def writer : CounterProgram where
     forCode 12 1 (vertexBoundExpr k (radixExpr D (reg 0))) 15 16 ++ [emit true 14, emit false 17] ++
     forCode 17 1 (numVerticesExpr (k := k) D) 20 33 ++
     forCode 20 2 (numVerticesExpr (k := k) D) 23 19 ++
-    [lt (reg 2) (vertexBoundExpr k (radixExpr D (reg 0))) 24 30,
-     lt (queryIndexExpr k (radixExpr D (reg 0)) (reg 1)) (reg 0) 25 28,
-     read (add (mul (const 2) (queryIndexExpr k (radixExpr D (reg 0)) (reg 1))) (const 1)) 26 27 27,
-     assign 3 (const 2) 29,
-     assign 3 (const 1) 29,
-     assign 3 (const 0) 29,
-     lt (const 0) (edgeExpr ntm (radixExpr D (reg 0)) (reg 0) (reg 1) (reg 2) (reg 3)) 31 32,
+    [lt (reg 2) (vertexBoundExpr k (radixExpr D (reg 0))) 24 30] ++
+    readSymbolCode 24 3 29 (reg 0) (queryIndexExpr k (radixExpr D (reg 0)) (reg 1)) ++
+    [lt (const 0) (edgeExpr ntm (radixExpr D (reg 0)) (reg 0) (reg 1) (reg 2) (reg 3)) 31 32,
      lt (const 0) (badExpr k State (radixExpr D (reg 0)) (reg 0) (reg 1)) 31 32,
      emit true 22,
      emit false 22,
@@ -293,29 +288,13 @@ private theorem reachesOut_entry_symbol (hL : w.length ≤ B)
     ∃ y' ≤ 2, y' = symbolCode w[queryIndex (k := k) (radix D w.length) u]? ∧
       (writer ntm D).ReachesOut (frame w) ((writer ntm D).Active B)
         (24, [w.length, u, v, y]) (29, [w.length, u, v, y']) [] := by
-  -- the code of the symbol requested by the row `u`
   have hB : ∀ r ∈ [w.length, u, v, y], r ≤ B := bounded_regs hL (by omega) (by omega) (by omega)
-  set q := queryIndex (k := k) (radix D w.length) u with hq_def
-  by_cases hq : q < w.length
-  · obtain ⟨b, hb⟩ : ∃ b, w[q]? = some b := ⟨w[q], List.getElem?_eq_getElem hq⟩
-    refine ⟨symbolCode (some b), by cases b <;> decide, by rw [hb], ?_⟩
-    refine ReachesOut.lt (show (writer ntm D).instr 24 = _ from rfl) hB ?_
-    simp only [eval_queryIndexExpr, eval_radixExpr, eval_reg, List.getD_cons_zero,
-      List.getD_cons_succ, ← hq_def, hq, ↓reduceIte]
-    refine ReachesOut.read (show (writer ntm D).instr 25 = _ from rfl) hB ?_
-    simp only [eval_add, eval_mul, eval_const, eval_queryIndexExpr, eval_radixExpr, eval_reg,
-      List.getD_cons_zero, List.getD_cons_succ, ← hq_def, getElem?_frame_two_mul_add_one hq, hb]
-    cases b
-    · refine ReachesOut.assign (show (writer ntm D).instr 27 = _ from rfl) hB ?_
-      simpa [symbolCode] using ReachesOut.refl _
-    · refine ReachesOut.assign (show (writer ntm D).instr 26 = _ from rfl) hB ?_
-      simpa [symbolCode] using ReachesOut.refl _
-  · refine ⟨0, by omega, congrArg symbolCode (List.getElem?_eq_none (by omega)).symm, ?_⟩
-    refine ReachesOut.lt (show (writer ntm D).instr 24 = _ from rfl) hB ?_
-    simp only [eval_queryIndexExpr, eval_radixExpr, eval_reg, List.getD_cons_zero,
-      List.getD_cons_succ, ← hq_def, hq, ↓reduceIte]
-    refine ReachesOut.assign (show (writer ntm D).instr 28 = _ from rfl) hB ?_
-    simpa using ReachesOut.refl _
+  have hcode : (writer ntm D).CodeAt 24
+      (readSymbolCode 24 3 29 (reg 0) (queryIndexExpr k (radixExpr D (reg 0)) (reg 1))) := by
+    simp only [readSymbolCode, codeAt_cons, codeAt_nil, and_true]
+    exact ⟨rfl, rfl, rfl, rfl, rfl⟩
+  refine ⟨_, Nat.le_of_lt_succ (symbolCode_lt _), rfl, ?_⟩
+  simpa using reachesOut_readSymbolCode (w := w) hcode (by simp) hB
 
 /-- **An entry of the matrix**: the code of the requested input symbol is stored in register `3`,
 and the entry is written. -/
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/ReadInput.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/ReadInput.lean
new file mode 100644
index 000000000..c75e73a3a
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/ReadInput.lean
@@ -0,0 +1,156 @@
+/-
+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
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Expr
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.ReadSymbol
+
+/-!
+# A fair-coin count block reading the original input
+
+The six-instruction `coinCountCode` reads the one original input symbol requested by a compact
+source ID, then evaluates both fixed-coin edges and adds their multiplicities. It uses four
+registers: the original word length, source ID, target ID, and one scratch register. The scratch
+register first holds the symbol code and then the count, which is zero, one, or two.
+
+`reachesOut_coinCountCode` proves execution on the actual framed input. The other registers do
+not change, no output is emitted, and every intermediate register is bounded by any common bound
+for the initial registers and two. Invalid compact IDs retain the existing guarded behavior.
+
+The concrete `coinCountProgram` places this block at label zero and a halt at label six. Its
+query and execution callbacks have native linear-space certificates in the binary register-state
+encoding. The execution theorem starts with the length and IDs already in registers; it does not
+parse those parameters or enumerate a matrix. Connecting an ambient enumeration, paired ports,
+and the time-layered matrix remains separate from this input-reading component.
+
+## Main definitions
+
+* `Turing.MultiTapePTM.ConfigurationGraph.coinCountExpr`: arithmetic counting both coin edges.
+* `Turing.MultiTapePTM.ConfigurationGraph.coinCountCode`: the placed input-reading count block.
+* `Turing.MultiTapePTM.ConfigurationGraph.coinCountProgram`: the concrete four-register program.
+
+## Main results
+
+* `Turing.MultiTapePTM.ConfigurationGraph.reachesOut_coinCountCode`: bounded execution from the
+  actual framed input, yielding the exact compact transition count.
+* `Turing.MultiTapePTM.ConfigurationGraph.reachesOut_coinCountProgram`: the concrete program run.
+* `Turing.MultiTapePTM.ConfigurationGraph.coinCountProgram_query_inSpace`,
+  `Turing.MultiTapePTM.ConfigurationGraph.coinCountProgram_exec_inSpace`: native space certificates
+  for the actual query and register-update routines.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM.ConfigurationGraph
+
+open MultiTapeNTM.ConfigurationGraph CounterProgram Instr Expr MultiTapeTM
+open Cslib.Turing
+
+variable {k : ℕ} {State : Type} [Fintype State]
+
+/-- Add the two fixed-coin arithmetic edge tests, retaining multiplicity when the successors
+coincide. The symbol expression contains the ternary code used by `readSymbolCode`. -/
+noncomputable def coinCountExpr (machine : MultiTapePTM k Bool State)
+    (B n u v sym : Expr) : Expr :=
+  add (edgeExpr (machine.withCoin false).toTM.toMultiTapeNTM B n u v sym)
+    (edgeExpr (machine.withCoin true).toTM.toMultiTapeNTM B n u v sym)
+
+/-- The count expression computes the existing compact fair-coin transition count. -/
+theorem eval_coinCountExpr (machine : MultiTapePTM k Bool State)
+    {B n u v sym : Expr} {regs : List ℕ} {symbol : Option Bool}
+    (hs : sym.eval regs = symbolCode symbol) :
+    (coinCountExpr machine B n u v sym).eval regs =
+      coinCountWithSymbol machine (B.eval regs) (n.eval regs) (u.eval regs) (v.eval regs)
+        symbol := by
+  rw [coinCountExpr, eval_add, eval_edgeExpr _ hs, eval_edgeExpr _ hs]
+  rfl
+
+/-- Read from `frame w` and store the coin count in register three, then continue at `exit`.
+Registers zero through two hold `w.length`, the source ID, and the target ID. The radix is
+`(w.length + 2) ^ D`; the six instructions start at `b`. -/
+@[expose] noncomputable def coinCountCode (machine : MultiTapePTM k Bool State)
+    (D b exit : ℕ) : List Instr :=
+  readSymbolCode b 3 (b + 5) (reg 0) (queryIndexExpr k (radixExpr D (reg 0)) (reg 1)) ++
+    [assign 3 (coinCountExpr machine (radixExpr D (reg 0))
+      (reg 0) (reg 1) (reg 2) (reg 3)) exit]
+
+/-- The reader and the arithmetic assignment occupy six consecutive labels. -/
+@[simp] theorem length_coinCountCode (machine : MultiTapePTM k Bool State) (D b exit : ℕ) :
+    (coinCountCode machine D b exit).length = 6 := rfl
+
+/-- The actual block reads the original input and returns its exact fair-coin edge multiplicity.
+All pre-exit register states satisfy the supplied common bound. No valid-ID or reachable-view
+premise is needed: the existing compact edge predicates also define the invalid-ID cases. -/
+theorem reachesOut_coinCountCode (machine : MultiTapePTM k Bool State)
+    {P : CounterProgram} {D b exit S u v y : ℕ} {w : List Bool}
+    (hcode : P.CodeAt b (coinCountCode machine D b exit))
+    (hS : ∀ r ∈ [w.length, u, v, y], r ≤ S) (h2 : 2 ≤ S) :
+    P.ReachesOut (frame w) (P.Active S) (b, [w.length, u, v, y])
+      (exit, [w.length, u, v, coinCountWithSymbol machine (radix D w.length) w.length u v
+        w[queryIndex (k := k) (radix D w.length) u]?]) [] := by
+  simp only [coinCountCode, codeAt_append, length_readSymbolCode, codeAt_cons] at hcode
+  obtain ⟨hread, hassign, -⟩ := hcode
+  let symbol := w[queryIndex (k := k) (radix D w.length) u]?
+  have hr : P.ReachesOut (frame w) (P.Active S) (b, [w.length, u, v, y])
+      (b + 5, [w.length, u, v, symbolCode symbol]) [] := by
+    simpa [symbol] using reachesOut_readSymbolCode (w := w) hread (by simp) hS
+  have hbound : ∀ r ∈ [w.length, u, v, symbolCode symbol], r ≤ S := by
+    intro r hr
+    have hm : r ∈ [w.length, u, v, y].set 3 (symbolCode symbol) := hr
+    rcases List.mem_or_eq_of_mem_set hm with hm | rfl
+    · exact hS r hm
+    · exact (Nat.le_of_lt_succ (symbolCode_lt symbol)).trans h2
+  have heval :
+      (coinCountExpr machine (radixExpr D (reg 0)) (reg 0) (reg 1) (reg 2) (reg 3)).eval
+        [w.length, u, v, symbolCode symbol] =
+      coinCountWithSymbol machine (radix D w.length) w.length u v symbol := by
+    simpa using eval_coinCountExpr machine (symbol := symbol)
+      (B := radixExpr D (reg 0)) (n := reg 0) (u := reg 1) (v := reg 2) (sym := reg 3)
+      (regs := [w.length, u, v, symbolCode symbol]) rfl
+  refine (hr.trans (ReachesOut.assign hassign hbound ?_)).of_eq rfl
+  rw [heval]
+  exact ReachesOut.refl _
+
+/-- The count block followed by a halt. The caller supplies the original input length and the
+two compact IDs in registers zero through two before entering the block. -/
+@[expose] noncomputable def coinCountProgram (machine : MultiTapePTM k Bool State)
+    (D : ℕ) : CounterProgram where
+  code := coinCountCode machine D 0 6 ++ [halt []]
+  registers := 4
+
+/-- The concrete program reaches its halt label, returning the count in register three and
+emitting nothing. The initial register values are explicit; they are not the zeroed program
+initializer. -/
+theorem reachesOut_coinCountProgram (machine : MultiTapePTM k Bool State)
+    {D S u v y : ℕ} {w : List Bool}
+    (hS : ∀ r ∈ [w.length, u, v, y], r ≤ S) (h2 : 2 ≤ S) :
+    (coinCountProgram machine D).ReachesOut (frame w) ((coinCountProgram machine D).Active S)
+      (0, [w.length, u, v, y])
+      (6, [w.length, u, v, coinCountWithSymbol machine (radix D w.length) w.length u v
+        w[queryIndex (k := k) (radix D w.length) u]?]) [] :=
+  reachesOut_coinCountCode machine
+    (codeAt_of_code_eq (pre := []) (post := [halt []]) rfl) hS h2
+
+/-- The concrete reader's query-index routine has a native linear-space certificate in its
+binary label-and-register encoding, rather than the length of the original input word. -/
+theorem coinCountProgram_query_inSpace (machine : MultiTapePTM k Bool State) (D : ℕ) :
+    ComputableInSpace (coinCountProgram machine D).query Simulation.encConfig encNat
+      (fun s => (Simulation.encConfig s).length) :=
+  (Simulation.query_inSpace (P := coinCountProgram machine D)).computableInSpace
+
+/-- The concrete reader's register-update routine has a native linear-space certificate in the
+binary register state together with the one optional input bit returned by the native query. -/
+theorem coinCountProgram_exec_inSpace (machine : MultiTapePTM k Bool State) (D : ℕ) :
+    ComputableInSpace
+      (fun p : Config × Option Bool => (coinCountProgram machine D).exec p.1 p.2)
+      Simulation.encConfigRead Simulation.encConfig
+      (fun p => (Simulation.encConfigRead p).length) :=
+  (Simulation.exec_inSpace (P := coinCountProgram machine D)).computableInSpace
+
+end Turing.MultiTapePTM.ConfigurationGraph
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/ReadSymbol.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/ReadSymbol.lean
new file mode 100644
index 000000000..1e5b8940e
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/ReadSymbol.lean
@@ -0,0 +1,85 @@
+/-
+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.Tape
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Output
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame
+
+/-!
+# Reading a configuration graph's input symbol
+
+`readSymbolCode` is the five-instruction block used by the STCON reduction to obtain the ternary
+code of one original input bit. It checks the query against the stored input length, reads position
+`2 * query + 1` of the framed input when in range, and stores zero otherwise. The block changes only
+its destination register and emits no output.
+
+The query is a zero-based position in the original word. Configuration-head boundary conventions
+are handled separately by the compact graph's edge test: this block returns the actual optional
+word symbol, not the symbol after that boundary correction.
+
+## Main definitions
+
+* `Turing.MultiTapeNTM.ConfigurationGraph.readSymbolCode`: the relocatable input-reading block.
+
+## Main results
+
+* `Turing.MultiTapeNTM.ConfigurationGraph.reachesOut_readSymbolCode`: the actual block reads
+  `w[query]?` from `frame w`, preserving the bound on every pre-exit register state.
+-/
+
+public section
+
+namespace Turing.MultiTapeNTM.ConfigurationGraph
+
+open CounterProgram Instr Expr MultiTapeTM
+
+/-- Read one original input symbol from a framed word into `dst`, then continue at `exit`.
+The five instructions start at `b`; `len` is the original word length and `query` its zero-based
+index. The result is `symbolCode`: zero for no symbol, one for false, and two for true. -/
+@[expose] def readSymbolCode (b dst exit : ℕ) (len query : Expr) : List Instr :=
+  [lt query len (b + 1) (b + 4),
+   read (add (mul (const 2) query) (const 1)) (b + 2) (b + 3) (b + 3),
+   assign dst (const 2) exit,
+   assign dst (const 1) exit,
+   assign dst (const 0) exit]
+
+/-- The reader occupies five consecutive instruction labels. -/
+@[simp] theorem length_readSymbolCode (b dst exit : ℕ) (len query : Expr) :
+    (readSymbolCode b dst exit len query).length = 5 := rfl
+
+/-- The placed block reads the original word's optional symbol, changes only `dst`, and emits
+nothing. All states before the exit have the original registers, so their bound needs no extra
+assumption. The final destination is at most two by `symbolCode_lt`. -/
+theorem reachesOut_readSymbolCode {P : CounterProgram} {b dst exit S : ℕ}
+    {len query : Expr} {regs : List ℕ} {w : List Bool}
+    (hcode : P.CodeAt b (readSymbolCode b dst exit len query))
+    (hlen : len.eval regs = w.length) (hS : ∀ r ∈ regs, r ≤ S) :
+    P.ReachesOut (frame w) (P.Active S) (b, regs)
+      (exit, regs.set dst (symbolCode w[query.eval regs]?)) [] := by
+  simp only [readSymbolCode, codeAt_cons] at hcode
+  obtain ⟨h₀, h₁, h₂, h₃, h₄, -⟩ := hcode
+  simp only [Nat.add_assoc] at h₂ h₃ h₄
+  refine ReachesOut.lt h₀ hS ?_
+  rw [hlen]
+  by_cases hq : query.eval regs < w.length
+  · obtain ⟨bit, hb⟩ : ∃ bit, w[query.eval regs]? = some bit :=
+      ⟨w[query.eval regs], List.getElem?_eq_getElem hq⟩
+    rw [ite_eq_left hq, hb]
+    refine ReachesOut.read h₁ hS ?_
+    simp only [eval_add, eval_mul, eval_const, getElem?_frame_two_mul_add_one hq, hb]
+    cases bit
+    · refine ReachesOut.assign h₃ hS ?_
+      simpa only [eval_const, symbolCode] using ReachesOut.refl _
+    · refine ReachesOut.assign h₂ hS ?_
+      simpa only [eval_const, symbolCode] using ReachesOut.refl _
+  · rw [ite_eq_right hq, List.getElem?_eq_none (by omega)]
+    refine ReachesOut.assign h₄ hS ?_
+    simpa only [eval_const, symbolCode] using ReachesOut.refl _
+
+end Turing.MultiTapeNTM.ConfigurationGraph
diff --git a/ComplexityTests/FairCoinInput.lean b/ComplexityTests/FairCoinInput.lean
new file mode 100644
index 000000000..4c41283fa
--- /dev/null
+++ b/ComplexityTests/FairCoinInput.lean
@@ -0,0 +1,170 @@
+/-
+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.ReadInput
+import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationReader
+
+/-!
+# Fair-coin count blocks on actual framed inputs
+
+The shared reader obtains true, false, and absent symbols from actual framed words. A concrete
+zero-work-tape machine then makes its output depend on both the input symbol and its coin. With
+the same source and target compact IDs, changing the original input bit changes the block's
+answer from one to zero. Making both coin branches coincide changes one to two. All representation
+and runtime register bounds in these runs are discharged.
+-/
+
+namespace ComplexityTests.FairCoinInput
+
+open Cslib.Turing Turing MultiTapeTM CounterProgram Instr Expr
+open MultiTapeNTM.ConfigurationGraph MultiTapePTM.ConfigurationGraph
+
+private def symbolProgram : CounterProgram where
+  code := readSymbolCode 0 2 5 (reg 0) (reg 1) ++ [halt []]
+  registers := 3
+
+-- The first original true bit is read from its data cell, not from a frame marker.
+example : symbolProgram.ReachesOut (frame [true, false]) (symbolProgram.Active 2)
+    (0, [2, 0, 0]) (5, [2, 0, 2]) [] := by
+  have hcode : symbolProgram.CodeAt 0 (readSymbolCode 0 2 5 (reg 0) (reg 1)) :=
+    codeAt_of_code_eq (pre := []) (post := [halt []]) rfl
+  simpa [symbolCode] using reachesOut_readSymbolCode (w := [true, false])
+    (regs := [2, 0, 0]) hcode rfl (by simp)
+
+-- The second data cell is false, whose ternary code is one.
+example : symbolProgram.ReachesOut (frame [true, false]) (symbolProgram.Active 2)
+    (0, [2, 1, 0]) (5, [2, 1, 1]) [] := by
+  have hcode : symbolProgram.CodeAt 0 (readSymbolCode 0 2 5 (reg 0) (reg 1)) :=
+    codeAt_of_code_eq (pre := []) (post := [halt []]) rfl
+  simpa [symbolCode] using reachesOut_readSymbolCode (w := [true, false])
+    (regs := [2, 1, 0]) hcode rfl (by simp)
+
+-- An index at the original length returns no symbol, despite the trailing frame marker.
+example : symbolProgram.ReachesOut (frame [true, false]) (symbolProgram.Active 2)
+    (0, [2, 2, 1]) (5, [2, 2, 0]) [] := by
+  have hcode : symbolProgram.CodeAt 0 (readSymbolCode 0 2 5 (reg 0) (reg 1)) :=
+    codeAt_of_code_eq (pre := []) (post := [halt []]) rfl
+  simpa [symbolCode] using reachesOut_readSymbolCode (w := [true, false])
+    (regs := [2, 2, 1]) hcode rfl (by simp)
+
+-- Empty original input also returns no symbol and overwrites stale scratch data.
+example : symbolProgram.ReachesOut (frame []) (symbolProgram.Active 2)
+    (0, [0, 0, 2]) (5, [0, 0, 0]) [] := by
+  have hcode : symbolProgram.CodeAt 0 (readSymbolCode 0 2 5 (reg 0) (reg 1)) :=
+    codeAt_of_code_eq (pre := []) (post := [halt []]) rfl
+  simpa [symbolCode] using reachesOut_readSymbolCode (w := [])
+    (regs := [0, 0, 2]) hcode rfl (by simp)
+
+/-- A true input symbol enables acceptance. When `different` is true, only the true coin accepts;
+otherwise both coins accept. A false or absent input symbol always emits false. -/
+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 theorem count_input (different input : Bool) :
+    coinCountWithSymbol (machine different) 3 1
+      (vertexID 3 (running input)) (vertexID 3 (stopped input true))
+      [input][queryIndex (k := 0) 3 (vertexID 3 (running input))]? =
+        if input then (if different then 1 else 2) else 0 := by
+  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 noncomputable def source : ℕ := vertexID 3 (running true)
+
+private noncomputable def target : ℕ := vertexID 3 (stopped true true)
+
+-- The original bit is not part of the compact ID; all runs below use these same two IDs.
+example (input : Bool) : vertexID 3 (running input) = source ∧
+    vertexID 3 (stopped input true) = target := ⟨rfl, rfl⟩
+
+private theorem count_program (different input : Bool) :
+    (coinCountProgram (machine different) 1).ReachesOut (frame [input])
+      ((coinCountProgram (machine different) 1).Active 27)
+      (0, [1, source, target, 0])
+      (6, [1, source, target, if input then (if different then 1 else 2) else 0]) [] := by
+  have hbox : vertexBound (k := 0) 3 = 27 := by decide
+  have hu : source < 27 := by
+    simpa only [source, hbox] using vertexID_lt (fits_three (running true) rfl)
+  have hv : target < 27 := by
+    simpa only [target, hbox] using vertexID_lt (fits_three (stopped true true) rfl)
+  have hbound : ∀ r ∈ [1, source, target, 0], r ≤ 27 := by
+    simp only [List.mem_cons, List.not_mem_nil, or_false]
+    omega
+  have hr := reachesOut_coinCountProgram (machine different) (D := 1) (w := [input])
+    hbound (by decide : 2 ≤ 27)
+  have hc : coinCountWithSymbol (machine different) (radix 1 [input].length) [input].length
+      source target [input][queryIndex (k := 0) (radix 1 [input].length) source]? =
+      if input then (if different then 1 else 2) else 0 := count_input different input
+  rw [hc] at hr
+  simpa only [List.length_singleton] using hr
+
+-- One accepting coin on the true input: the actual framed input reaches a count of one.
+example : (coinCountProgram (machine true) 1).ReachesOut (frame [true])
+    ((coinCountProgram (machine true) 1).Active 27)
+    (0, [1, source, target, 0]) (6, [1, source, target, 1]) [] := count_program true true
+
+-- Changing only that input bit to false changes the count to zero.
+example : (coinCountProgram (machine true) 1).ReachesOut (frame [false])
+    ((coinCountProgram (machine true) 1).Active 27)
+    (0, [1, source, target, 0]) (6, [1, source, target, 0]) [] := count_program true false
+
+-- Coincident accepting successors retain multiplicity two in the register result.
+example : (coinCountProgram (machine false) 1).ReachesOut (frame [true])
+    ((coinCountProgram (machine false) 1).Active 27)
+    (0, [1, source, target, 0]) (6, [1, source, target, 2]) [] := count_program false true
+
+-- The returned label is an actual halt of the concrete program.
+example (different : Bool) : (coinCountProgram (machine different) 1).instr 6 = halt [] := rfl
+
+end ComplexityTests.FairCoinInput