diff --git a/Complexity.lean b/Complexity.lean
index ef9a73ad4..34b094835 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1070,6 +1070,7 @@ 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.ConfigurationMatrix
+public import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationReader
 public import Complexity.Computability.Complexity.Classes.LogSpace.Savitch
 public import Complexity.Computability.Complexity.Classes.LogSpace.USTCON
 public import Complexity.Computability.Complexity.Classes.MIP
@@ -1534,6 +1535,8 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Bounds
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Correctness
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Expr
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin
+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.Routines
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Tape
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean
new file mode 100644
index 000000000..9ba13cdb2
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized/ConfigurationReader.lean
@@ -0,0 +1,195 @@
+/-
+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.ConfigurationMatrix
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.FairCoin
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Bounds
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Injective
+
+/-!
+# Reading the fair-coin configuration matrix from compact IDs
+
+The native compact-ID query `coinCountWithSymbol` agrees with the actual configuration matrix of
+`MultiTapePTM`, counting both coins even when they select the same successor. Its live variant
+agrees with the live configuration matrix. The correspondence uses the original input only at
+the compact graph's `queryIndex`.
+
+For views reachable under a logarithmic space bound, the prescribed polynomial radix fits every
+view and the output is already summarized. The final two corollaries derive these representation
+conditions from the machine's space bound and reachability, so they apply to the reachable-view
+sets in `exists_configMatrix_of_mem_BPL`.
+
+The count matrix gives halted views an absorbing edge of multiplicity two. The live matrix gives
+halted views a zero row. These are the two conventions of `ConfigurationMatrix`, and do not assert
+that halted executions consume further coins. This module supplies local access with the native
+space certificates of `ConfigurationGraph.FairCoin`; bounded enumeration, time layering and the
+full estimator remain separate constructions.
+
+## Main results
+
+* `Turing.MultiTapePTM.viewStep_withCoin_iff`: a fixed-coin native view edge is its coin successor.
+* `Turing.MultiTapePTM.ConfigurationGraph.coinCountWithSymbol_eq_configMatrix`,
+  `Turing.MultiTapePTM.ConfigurationGraph.liveCoinCountWithSymbol_eq_liveConfigMatrix`:
+  exact matrix entries at fitting canonical views.
+* The corresponding `*_of_reachable` results: the native logspace machine discharges the
+  representation hypotheses at its polynomial radix.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM
+
+open MultiTapeNTM
+
+variable {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State)
+
+/-- Fixing the coin gives exactly the corresponding deterministic view successor. -/
+theorem viewStep_withCoin_iff {a b : FiniteCfg k Bool State} (bit : Bool) :
+    (machine.withCoin bit).toTM.toMultiTapeNTM.ViewStep a b ↔
+      machine.viewCoinStep a bit = b := by
+  cases hs : a.state <;>
+    simp [MultiTapeNTM.ViewStep, viewCoinStep, hs, MultiTapeTM.tr_iff, eq_comm]
+
+private theorem outputClass_idem (w : List Bool) : outputClass (outputClass w) = outputClass w := by
+  simpa only [Option.toList_none, List.append_nil] using outputClass_append w none
+
+private theorem viewCoinStep_input (a : FiniteCfg k Bool State) (bit : Bool) :
+    (machine.viewCoinStep a bit).input = a.input := by
+  cases hs : a.state <;> simp [viewCoinStep, hs, FiniteCfg.summarizeOutput, FiniteCfg.step]
+
+private theorem viewCoinStep_canonical {a : FiniteCfg k Bool State}
+    (ha : outputClass a.output = a.output) (bit : Bool) :
+    outputClass (machine.viewCoinStep a bit).output = (machine.viewCoinStep a bit).output := by
+  cases hs : a.state <;>
+    simp [viewCoinStep, hs, FiniteCfg.summarizeOutput, outputClass_idem, ha]
+
+namespace ConfigurationGraph
+
+open MultiTapeNTM.ConfigurationGraph
+
+variable [Fintype State]
+
+/-- The local edge test for one fixed coin is exact on fitting canonical views. -/
+theorem edgeWithSymbol_withCoin_iff {B : ℕ} {a b : FiniteCfg k Bool State}
+    (hinput : a.input = b.input) (ha : outputClass a.output = a.output)
+    (hb : outputClass b.output = b.output)
+    (hfitA : Fits B (registers a)) (hfitB : Fits B (registers b)) (bit : Bool) :
+    edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B a.input.length
+      (vertexID B a) (vertexID B b) a.input[queryIndex (k := k) B (vertexID B a)]? = true ↔
+        machine.viewCoinStep a bit = b := by
+  change Edge (machine.withCoin bit).toTM.toMultiTapeNTM B a.input
+    (vertexID B a) (vertexID B b) ↔ _
+  constructor
+  · intro he
+    obtain ⟨next, hstep, _, hid, hfit⟩ := edge_sound hfitA he
+    have hnext : machine.viewCoinStep a bit = next := (viewStep_withCoin_iff machine bit).mp hstep
+    subst next
+    exact vertexID_injective ((viewCoinStep_input machine a bit).trans hinput)
+      (viewCoinStep_canonical machine ha bit) hb hfit hfitB hid.symm
+  · intro he
+    exact edge_complete hfitA hfitB ((viewStep_withCoin_iff machine bit).mpr he)
+
+variable {R : Type*} [CommSemiring R]
+
+/-- The certified local coin count, cast to the coefficient semiring, is the actual matrix entry.
+No closedness assumption on `V` is needed for this individual-entry identity. -/
+theorem coinCountWithSymbol_eq_configMatrix {B : ℕ} {V : Finset (FiniteCfg k Bool State)}
+    (x y : V) (hinput : (x : FiniteCfg k Bool State).input = y.val.input)
+    (hx : outputClass x.val.output = x.val.output) (hy : outputClass y.val.output = y.val.output)
+    (hfitX : Fits B (registers x.val)) (hfitY : Fits B (registers y.val)) :
+    (coinCountWithSymbol machine B x.val.input.length (vertexID B x.val) (vertexID B y.val)
+      x.val.input[queryIndex (k := k) B (vertexID B x.val)]? : R) =
+        machine.configMatrix R V x y := by
+  classical
+  have hcoin (bit : Bool) :
+      ((edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B x.val.input.length
+        (vertexID B x.val) (vertexID B y.val)
+        x.val.input[queryIndex (k := k) B (vertexID B x.val)]?).toNat : R) =
+          if machine.viewCoinStep x bit = y then 1 else 0 := by
+    have he := edgeWithSymbol_withCoin_iff machine hinput hx hy hfitX hfitY bit
+    by_cases hb : machine.viewCoinStep x bit = y
+    · simp [he.mpr hb, hb]
+    · have hf : edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B x.val.input.length
+          (vertexID B x.val) (vertexID B y.val)
+          x.val.input[queryIndex (k := k) B (vertexID B x.val)]? = false :=
+        Bool.eq_false_iff.mpr fun h => hb (he.mp h)
+      simp [hf, hb]
+  rw [coinCountWithSymbol, Nat.cast_add, hcoin false, hcoin true, configMatrix,
+    Matrix.coinStepMatrix, Fintype.sum_bool]
+  exact add_comm _ _
+
+/-- The certified local count with halted rows removed is the actual live matrix entry. -/
+theorem liveCoinCountWithSymbol_eq_liveConfigMatrix {B : ℕ}
+    {V : Finset (FiniteCfg k Bool State)} (x y : V)
+    (hinput : x.val.input = y.val.input)
+    (hx : outputClass x.val.output = x.val.output) (hy : outputClass y.val.output = y.val.output)
+    (hfitX : Fits B (registers x.val)) (hfitY : Fits B (registers y.val)) :
+    (liveCoinCountWithSymbol machine B x.val.input.length (vertexID B x.val) (vertexID B y.val)
+      x.val.input[queryIndex (k := k) B (vertexID B x.val)]? : R) =
+        machine.liveConfigMatrix R V x y := by
+  classical
+  rw [liveCoinCountWithSymbol, readRegisters_vertexID hfitX]
+  change ((if stateCode x.val.state = stateCode (none : Option State) then (0 : ℕ)
+    else coinCountWithSymbol machine B x.val.input.length (vertexID B x.val) (vertexID B y.val)
+      x.val.input[queryIndex (k := k) B (vertexID B x.val)]? : ℕ) : R) = _
+  by_cases hs : x.val.state = none
+  · simp [hs, liveConfigMatrix, Matrix.liveCoinStepMatrix]
+  · have hcode : stateCode x.val.state ≠ stateCode (none : Option State) :=
+      fun h => hs (stateCode_injective h)
+    rw [ite_eq_right hcode, liveConfigMatrix, Matrix.liveCoinStepMatrix, ite_eq_left hs]
+    exact coinCountWithSymbol_eq_configMatrix (R := R) machine x y hinput hx hy hfitX hfitY
+
+omit [Fintype State] in
+private theorem canonical_of_reachable {input : List Bool} {v : FiniteCfg k Bool State}
+    (hv : Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) v) :
+    outputClass v.output = v.output := by
+  obtain ⟨p, hrep⟩ := exists_computationPath_of_viewStep hv
+  rw [hrep.output, outputClass_idem]
+
+/-- Reachability and the native logarithmic space bound supply every representation hypothesis
+for the count-matrix reader at the standard polynomial radix. -/
+theorem coinCountWithSymbol_eq_configMatrix_of_reachable (c : ℕ) {input : List Bool}
+    (hs : machine.toNTM.RunsInSpace input (c * (Nat.log2 input.length + 1)))
+    {V : Finset (FiniteCfg k Bool State)}
+    (hV : ∀ v ∈ V, Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) v)
+    (x y : V) :
+    let B := radix (radixExponent State c) input.length
+    (coinCountWithSymbol machine B input.length (vertexID B x.val) (vertexID B y.val)
+      input[queryIndex (k := k) B (vertexID B x.val)]? : R) = machine.configMatrix R V x y := by
+  dsimp only
+  have hx := hV x x.property
+  have hy := hV y y.property
+  have hix : x.val.input = input := input_of_reachable hx
+  have hiy : y.val.input = input := input_of_reachable hy
+  simpa only [hix] using coinCountWithSymbol_eq_configMatrix machine x y (hix.trans hiy.symm)
+    (canonical_of_reachable machine hx) (canonical_of_reachable machine hy)
+    (fits_of_runsInSpace c hs hx) (fits_of_runsInSpace c hs hy)
+
+/-- The same reachable-view corollary for the live configuration matrix. -/
+theorem liveCoinCountWithSymbol_eq_liveConfigMatrix_of_reachable (c : ℕ) {input : List Bool}
+    (hs : machine.toNTM.RunsInSpace input (c * (Nat.log2 input.length + 1)))
+    {V : Finset (FiniteCfg k Bool State)}
+    (hV : ∀ v ∈ V, Relation.ReflTransGen machine.toNTM.ViewStep (machine.toNTM.initView input) v)
+    (x y : V) :
+    let B := radix (radixExponent State c) input.length
+    (liveCoinCountWithSymbol machine B input.length (vertexID B x.val) (vertexID B y.val)
+      input[queryIndex (k := k) B (vertexID B x.val)]? : R) = machine.liveConfigMatrix R V x y := by
+  dsimp only
+  have hx := hV x x.property
+  have hy := hV y y.property
+  have hix : x.val.input = input := input_of_reachable hx
+  have hiy : y.val.input = input := input_of_reachable hy
+  simpa only [hix] using
+    liveCoinCountWithSymbol_eq_liveConfigMatrix machine x y (hix.trans hiy.symm)
+      (canonical_of_reachable machine hx) (canonical_of_reachable machine hy)
+      (fits_of_runsInSpace c hs hx) (fits_of_runsInSpace c hs hy)
+
+end ConfigurationGraph
+
+end Turing.MultiTapePTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin.lean
new file mode 100644
index 000000000..1869f761e
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin.lean
@@ -0,0 +1,131 @@
+/-
+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.Routines
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.CoinTape
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Correctness
+
+/-!
+# Fair-coin transition counts on compact configuration IDs
+
+The nondeterministic compact graph records whether an edge exists. A fair-coin transition needs
+its multiplicity: two coincident branches still contribute two. `coinCountWithSymbol` adds the
+edge tests for the two fixed-coin machines. Each test reads the same supplied input symbol and
+uses the existing guarded radix arithmetic. Halting views are absorbing for this count;
+`liveCoinCountWithSymbol` instead gives them zero rows.
+
+The native space certificates charge the binary radix, input length, source and target IDs and
+one supplied symbol. The input itself is accessed only at `queryIndex`. The matrix interpretation
+is supplied in `Classes.LogSpace.Randomized.ConfigurationReader`.
+
+## Main definitions
+
+* `Turing.MultiTapePTM.ConfigurationGraph.coinCountWithSymbol`: the sum of the two coin edges.
+* `Turing.MultiTapePTM.ConfigurationGraph.liveCoinCountWithSymbol`: the count at running IDs.
+
+## Main results
+
+* `Turing.MultiTapePTM.ConfigurationGraph.coinCountWithSymbol_le_two`: every count is at most two.
+* `Turing.MultiTapePTM.ConfigurationGraph.coinCountWithSymbol_budget`,
+  `Turing.MultiTapePTM.ConfigurationGraph.liveCoinCountWithSymbol_budget`: native space bounds.
+
+This is a local implementation of the fair-coin configuration matrix, not an enumeration of its
+vertices or a time-layered matrix construction. It adds no estimator or derandomization claim.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM.ConfigurationGraph
+
+open MultiTapeNTM.ConfigurationGraph
+open Cslib.Turing MultiTapeTM ComputableInSpace
+
+variable {k : ℕ} {State : Type} [Fintype State]
+
+/-- The two fixed-coin edge predicates, counted separately even when their successors coincide.
+The compact graph guards invalid IDs and successor overflow; its halted vertices are absorbing. -/
+@[expose] noncomputable def coinCountWithSymbol (machine : MultiTapePTM k Bool State)
+    (B n u v : ℕ) (symbol : Option Bool) : ℕ :=
+  (edgeWithSymbol (machine.withCoin false).toTM.toMultiTapeNTM B n u v symbol).toNat +
+    (edgeWithSymbol (machine.withCoin true).toTM.toMultiTapeNTM B n u v symbol).toNat
+
+/-- The live transition count: rows whose control tag is halted are zero. -/
+@[expose] noncomputable def liveCoinCountWithSymbol (machine : MultiTapePTM k Bool State)
+    (B n u v : ℕ) (symbol : Option Bool) : ℕ :=
+  if readRegisters (k := k) B u .control = stateCode (none : Option State) then 0
+  else coinCountWithSymbol machine B n u v symbol
+
+/-- There are exactly two possible coin values, so the multiplicity is at most two. -/
+theorem coinCountWithSymbol_le_two (machine : MultiTapePTM k Bool State)
+    (B n u v : ℕ) (symbol : Option Bool) :
+    coinCountWithSymbol machine B n u v symbol ≤ 2 := by
+  unfold coinCountWithSymbol
+  cases edgeWithSymbol (machine.withCoin false).toTM.toMultiTapeNTM B n u v symbol <;>
+    cases edgeWithSymbol (machine.withCoin true).toTM.toMultiTapeNTM B n u v symbol <;> decide
+
+/-- An ID outside the bounded radix box has no outgoing coin edge. -/
+theorem coinCountWithSymbol_eq_zero_of_source_ge (machine : MultiTapePTM k Bool State)
+    {B n u v : ℕ} (hu : vertexBound (k := k) B ≤ u) (symbol : Option Bool) :
+    coinCountWithSymbol machine B n u v symbol = 0 := by
+  have h (bit : Bool) :
+      edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B n u v symbol = false := by
+    cases he : edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B n u v symbol with
+    | false => rfl
+    | true => exact False.elim ((not_lt_of_ge hu) (lt_vertexBound_of_edgeWithSymbol he).1)
+  simp [coinCountWithSymbol, h]
+
+/-- An ID outside the bounded radix box cannot be the target of a coin edge. -/
+theorem coinCountWithSymbol_eq_zero_of_target_ge (machine : MultiTapePTM k Bool State)
+    {B n u v : ℕ} (hv : vertexBound (k := k) B ≤ v) (symbol : Option Bool) :
+    coinCountWithSymbol machine B n u v symbol = 0 := by
+  have h (bit : Bool) :
+      edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B n u v symbol = false := by
+    cases he : edgeWithSymbol (machine.withCoin bit).toTM.toMultiTapeNTM B n u v symbol with
+    | false => rfl
+    | true => exact False.elim ((not_lt_of_ge hv) (lt_vertexBound_of_edgeWithSymbol he).2)
+  simp [coinCountWithSymbol, h]
+
+variable {α : Type} {enc : α ↪ List Bool} {S : α → ℕ}
+  {B n u v : α → ℕ} {symbol : α → Option Bool}
+
+/-- Count the two coin branches within any common native space budget for the short arguments. -/
+theorem coinCountWithSymbol_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 => coinCountWithSymbol machine (B a) (n a) (u a) (v a) (symbol a))
+      enc encNat S :=
+  budget_natAdd
+    (budget_finite Bool.toNat
+      (edgeWithSymbol_budget (machine.withCoin false).toTM.toMultiTapeNTM hB hn hu hv hs hin))
+    (budget_finite Bool.toNat
+      (edgeWithSymbol_budget (machine.withCoin true).toTM.toMultiTapeNTM hB hn hu hv hs hin))
+
+/-- Zeroing the halted rows preserves the same native space budget. -/
+theorem liveCoinCountWithSymbol_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 => liveCoinCountWithSymbol machine (B a) (n a) (u a) (v a) (symbol a))
+      enc encNat S := by
+  have hc : ComputableInSpace (fun a => readRegisters (k := k) (B a) (u a) .control)
+      enc encNat S :=
+    budget_comp_linear (component_inSpace (Register.control : Register k)) (budget_prod hB hu)
+  simpa only [liveCoinCountWithSymbol, decide_eq_true_eq] using
+    budget_ite (budget_natEq hc (budget_const (stateCode (none : Option State)) hin))
+      (budget_const 0 hin) (coinCountWithSymbol_budget machine hB hn hu hv hs hin)
+
+end Turing.MultiTapePTM.ConfigurationGraph
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Injective.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Injective.lean
new file mode 100644
index 000000000..5341a4f0b
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Injective.lean
@@ -0,0 +1,90 @@
+/-
+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.Correctness
+
+/-!
+# Compact configuration IDs identify canonical views
+
+The radix encoding stores the full input-free configuration except for the output, which it
+summarizes as empty, accepting, or rejecting. On views with already summarized output and a fixed
+input, fitting IDs are injective. This lets a local query on IDs represent an individual matrix
+entry, rather than an entire fiber of the encoding.
+
+## Main results
+
+* `Turing.MultiTapeNTM.ConfigurationGraph.stackCode_injective`: normalized ternary tape codes
+  distinguish stack tapes.
+* `Turing.MultiTapeNTM.ConfigurationGraph.vertexID_injective`: equal fitting IDs, on the same
+  input and with canonical output, identify the same view.
+-/
+
+public section
+
+namespace Turing.MultiTapeNTM.ConfigurationGraph
+
+open Cslib.Turing
+
+/-- The normalized stack representation has a unique ternary code. -/
+theorem stackCode_injective : Function.Injective stackCode := by
+  suffices h : ∀ n : ℕ, ∀ a b : StackTape Bool,
+      a.toList.length + b.toList.length = n → stackCode a = stackCode b → a = b from
+    fun a b hab => h _ a b rfl hab
+  intro n
+  induction n using Nat.strong_induction_on with
+  | ind n ih =>
+    intro a b hn hab
+    by_cases hz : n = 0
+    · have ha : a.toList = [] := List.length_eq_zero_iff.mp (by omega)
+      have hb : b.toList = [] := List.length_eq_zero_iff.mp (by omega)
+      exact StackTape.ext (ha.trans hb.symm)
+    · have hlt : a.tail.toList.length + b.tail.toList.length < n := by
+        simp only [StackTape.tail_toList, List.length_tail]
+        omega
+      apply (StackTape.eq_iff a b).mpr
+      refine ⟨symbolCode_injective ?_, ih _ hlt a.tail b.tail rfl ?_⟩
+      · rw [stackCode_head, stackCode_head, hab]
+      · rw [stackCode_tail, stackCode_tail, hab]
+
+private theorem outputClass_eq_of_outputCode_eq {a b : List Bool}
+    (h : outputCode a = outputCode b) : outputClass a = outputClass b := by
+  unfold outputClass
+  unfold outputCode at h
+  split_ifs at h ⊢ <;> simp_all
+
+variable {k : ℕ} {State : Type} [Fintype State]
+
+/-- The input-free registers distinguish views with the same input and canonical output. -/
+theorem registers_injective {a b : FiniteCfg k Bool State}
+    (hinput : a.input = b.input) (ha : outputClass a.output = a.output)
+    (hb : outputClass b.output = b.output) (h : registers a = registers b) : a = b := by
+  have hpos : a.inputPos.val = b.inputPos.val := congrFun h .inputPos
+  have hstate : a.state = b.state := stateCode_injective (congrFun h .control)
+  have hout : a.output = b.output :=
+    ha.symm.trans ((outputClass_eq_of_outputCode_eq (congrFun h .output)).trans hb)
+  have hwork : a.workTapes = b.workTapes := by
+    funext i
+    exact BiTape.ext (symbolCode_injective (congrFun h (.head i)))
+      (stackCode_injective (congrFun h (.left i)))
+      (stackCode_injective (congrFun h (.right i)))
+  apply coreCode_injective hinput
+  change encCore (a.inputPos.val, a.state, a.workTapes, a.output) =
+    encCore (b.inputPos.val, b.state, b.workTapes, b.output)
+  rw [hpos, hstate, hwork, hout]
+
+/-- Equal IDs determine fitting views with the same input and already summarized output. -/
+theorem vertexID_injective {B : ℕ} {a b : FiniteCfg k Bool State}
+    (hinput : a.input = b.input) (ha : outputClass a.output = a.output)
+    (hb : outputClass b.output = b.output)
+    (hfitA : Fits B (registers a)) (hfitB : Fits B (registers b))
+    (h : vertexID B a = vertexID B b) : a = b := by
+  apply registers_injective hinput ha hb
+  rw [← readRegisters_vertexID hfitA, ← readRegisters_vertexID hfitB, h]
+
+end Turing.MultiTapeNTM.ConfigurationGraph
diff --git a/ComplexityTests/FairCoinConfigurationReader.lean b/ComplexityTests/FairCoinConfigurationReader.lean
new file mode 100644
index 000000000..b5623a8ee
--- /dev/null
+++ b/ComplexityTests/FairCoinConfigurationReader.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
+-/
+
+import Complexity.Computability.Complexity.Classes.LogSpace.Randomized.ConfigurationReader
+
+/-!
+# Fair-coin compact-reader tests
+
+A zero-work-tape machine either outputs its coin or outputs true on both branches. The tests
+derive all representation hypotheses from its actual space bound and reachable configurations,
+then evaluate the matrix entries through the new local reader. They distinguish zero, one and
+two coin branches, and distinguish an absorbing halted row from the zero live row. Invalid IDs
+and a native space certificate on the exact binary query tuple are also checked.
+-/
+
+namespace ComplexityTests.FairCoinConfigurationReader
+
+open Cslib.Turing Turing MultiTapeTM
+open MultiTapeNTM.ConfigurationGraph MultiTapePTM.ConfigurationGraph
+
+/-- With `different = true`, output the coin; otherwise both branches output true. -/
+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 stopped (input : List Bool) (bit : Bool) : FiniteCfg 0 Bool Unit :=
+  ⟨input, none, 1, Fin.elim0, [bit]⟩
+
+private theorem viewCoinStep_start (different bit : Bool) (input : List Bool) :
+    (machine different).viewCoinStep ((machine different).toNTM.initView input) bit =
+      stopped input (if different then bit else true) := by
+  cases different <;> cases bit <;>
+    simp [MultiTapePTM.viewCoinStep, machine, MultiTapePTM.withCoin, MultiTapeMachine.toTM,
+      MultiTapeMachine.Action.emptyOracleEquiv,
+      MultiTapeNTM.initView, MultiTapePTM.toNTM, MultiTapePTM.branches, MultiTapeMachine.toNTM,
+      FiniteCfg.init, FiniteCfg.step, FiniteCfg.summarizeOutput, MultiTapeNTM.outputClass,
+      stopped, funext_iff]
+
+private theorem stopped_injective (input : List 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 stopped_ne_start (different bit : Bool) (input : List Bool) :
+    stopped input bit ≠ (machine different).toNTM.initView input := by
+  intro h
+  have hs := congrArg FiniteCfg.state h
+  cases hs
+
+private abbrev radixFor (input : List Bool) : ℕ := radix (radixExponent Unit 0) input.length
+
+private noncomputable def readCount (different : Bool) (input : List Bool)
+    (x y : FiniteCfg 0 Bool Unit) : ℕ :=
+  coinCountWithSymbol (machine different) (radixFor input) input.length
+    (vertexID (radixFor input) x) (vertexID (radixFor input) y)
+    input[queryIndex (k := 0) (radixFor input) (vertexID (radixFor input) x)]?
+
+private noncomputable def readLiveCount (different : Bool) (input : List Bool)
+    (x y : FiniteCfg 0 Bool Unit) : ℕ :=
+  liveCoinCountWithSymbol (machine different) (radixFor input) input.length
+    (vertexID (radixFor input) x) (vertexID (radixFor input) y)
+    input[queryIndex (k := 0) (radixFor input) (vertexID (radixFor input) x)]?
+
+private theorem reader_counts (different : Bool) (input : List Bool) :
+    readCount different input ((machine different).toNTM.initView input) (stopped input true) =
+        (if different then 1 else 2) ∧
+      readCount different input ((machine different).toNTM.initView input)
+        ((machine different).toNTM.initView input) = 0 ∧
+      readCount different input (stopped input true) (stopped input true) = 2 ∧
+      readLiveCount different input (stopped input true) (stopped input true) = 0 := by
+  classical
+  have hs := MultiTapeNTM.runsInSpace_zero_tapes (machine different).toNTM input 0
+  obtain ⟨V, hreach, hclosed, _⟩ := (machine different).exists_finset_reachable hs
+  have hinit : (machine different).toNTM.initView input ∈ V := (hreach _).mpr .refl
+  have hstop : stopped input true ∈ V := by
+    have h := hclosed _ hinit true
+    simp only [viewCoinStep_start, ite_self] at h
+    exact h
+  let x : V := ⟨(machine different).toNTM.initView input, hinit⟩
+  let y : V := ⟨stopped input true, hstop⟩
+  have hV v hv := (hreach v).mp hv
+  have hspace : (machine different).toNTM.RunsInSpace input
+      (0 * (Nat.log2 input.length + 1)) := by
+    rw [Nat.zero_mul]
+    exact hs
+  have hxy := coinCountWithSymbol_eq_configMatrix_of_reachable (R := ℕ)
+    (machine different) 0 hspace hV x y
+  have hxx := coinCountWithSymbol_eq_configMatrix_of_reachable (R := ℕ)
+    (machine different) 0 hspace hV x x
+  have hyy := coinCountWithSymbol_eq_configMatrix_of_reachable (R := ℕ)
+    (machine different) 0 hspace hV y y
+  have hlyy := liveCoinCountWithSymbol_eq_liveConfigMatrix_of_reachable (R := ℕ)
+    (machine different) 0 hspace hV y y
+  change readCount different input _ _ = _ at hxy hxx hyy
+  change readLiveCount different input _ _ = _ at hlyy
+  rw [hxy, hxx, hyy, hlyy]
+  refine ⟨?_, ?_, ?_, ?_⟩
+  · simp only [MultiTapePTM.configMatrix, Matrix.coinStepMatrix, Fintype.sum_bool, x, y,
+      viewCoinStep_start, (stopped_injective input).eq_iff]
+    cases different <;> decide
+  · simp [MultiTapePTM.configMatrix, Matrix.coinStepMatrix, x, viewCoinStep_start,
+      stopped_ne_start]
+  · simp [MultiTapePTM.configMatrix, Matrix.coinStepMatrix, MultiTapePTM.viewCoinStep, y, stopped]
+  · simp [MultiTapePTM.liveConfigMatrix, Matrix.liveCoinStepMatrix, y, stopped]
+
+-- The actual encoded reader sees one coin edge, including on the empty input boundary.
+example : readCount true [] ((machine true).toNTM.initView []) (stopped [] true) = 1 :=
+  (reader_counts true []).1
+
+-- Coincident successor branches contribute two, rather than one Boolean adjacency edge.
+example : readCount false [true, false] ((machine false).toNTM.initView [true, false])
+    (stopped [true, false] true) = 2 := (reader_counts false [true, false]).1
+
+-- There is no transition back to the initial running view.
+example (input : List Bool) :
+    readCount true input ((machine true).toNTM.initView input)
+      ((machine true).toNTM.initView input) = 0 := (reader_counts true input).2.1
+
+-- Halting is absorbing in the count matrix and has zero outgoing weight in the live matrix.
+example : readCount true [] (stopped [] true) (stopped [] true) = 2 ∧
+    readLiveCount true [] (stopped [] true) (stopped [] true) = 0 :=
+  (reader_counts true []).2.2
+
+-- Out-of-box IDs cannot create a spurious transition for either supplied input symbol.
+example (B n v : ℕ) (symbol : Option Bool) :
+    coinCountWithSymbol (machine true) B n (vertexBound (k := 0) B) v symbol = 0 :=
+  coinCountWithSymbol_eq_zero_of_source_ge _ (le_refl _) _
+
+example (B n u : ℕ) (symbol : Option Bool) :
+    coinCountWithSymbol (machine true) B n u (vertexBound (k := 0) B) symbol = 0 :=
+  coinCountWithSymbol_eq_zero_of_target_ge _ (le_refl _) _
+
+/-- The runtime query stores only its radix, input length, two IDs, and one supplied symbol. -/
+private abbrev encQuery : ℕ × ℕ × ℕ × ℕ × Option Bool ↪ List Bool :=
+  encPair encNat (encPair encNat (encPair encNat (encPair encNat (encOption encBool))))
+
+open ComputableInSpace in
+-- A concrete query on its exact binary argument encoding has a native linear-space certificate.
+example : ComputableInSpace
+    (fun a : ℕ × ℕ × ℕ × ℕ × Option Bool =>
+      liveCoinCountWithSymbol (machine true) a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2)
+    encQuery encNat (fun a => (encQuery a).length) := by
+  have hr₁ := snd encNat (encPair encNat (encPair encNat (encPair encNat (encOption encBool))))
+  have hr₂ := budget_comp_linear (snd _ _) hr₁
+  have hr₃ := budget_comp_linear (snd _ _) hr₂
+  exact liveCoinCountWithSymbol_budget (machine true) (fst _ _)
+    (budget_comp_linear (fst _ _) hr₁) (budget_comp_linear (fst _ _) hr₂)
+    (budget_comp_linear (fst _ _) hr₃) (budget_comp_linear (snd _ _) hr₃) (.refl _)
+
+end ComplexityTests.FairCoinConfigurationReader