feat(logspace): read fair-coin counts from framed inputs

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

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. -/

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

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