From f0fa322138783826aa6887356b737aa51435cd71 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 24 Jul 2026 10:33:38 -0700
Subject: [PATCH 1/5] feat(Classes): prove finitely-supported functions belong
 to FP
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Any function of the form `fun s => if s ∈ S then g s else []` with `S` a
finite set is polynomial-time computable: a work-tape-free lookup machine
hard-wires the finite table into its states, tracking viable prefixes of
`S` while scanning the input and then emitting the fixed output, all in
linear time. This gives the base case for assembling FP functions from
finitely many exceptional values.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Complexitylib/Classes/P.lean                  |   2 +
 Complexitylib/Classes/P/FinsetDomain.lean     |  37 ++
 .../Classes/P/FinsetDomain/Internal.lean      | 458 ++++++++++++++++++
 3 files changed, 497 insertions(+)
 create mode 100644 Complexitylib/Classes/P/FinsetDomain.lean
 create mode 100644 Complexitylib/Classes/P/FinsetDomain/Internal.lean

diff --git a/Complexitylib/Classes/P.lean b/Complexitylib/Classes/P.lean
index e5365bb1..af84b827 100644
--- a/Complexitylib/Classes/P.lean
+++ b/Complexitylib/Classes/P.lean
@@ -10,6 +10,7 @@ import Complexitylib.Classes.P.Composition
 import Complexitylib.Classes.P.PairWithInput
 import Complexitylib.Classes.P.Preimage
 import Complexitylib.Classes.P.UnaryLength
+import Complexitylib.Classes.P.FinsetDomain
 import Complexitylib.Models.TuringMachine.Subroutines.CopyOutput
 
 /-!
@@ -33,6 +34,7 @@ This file aggregates the definitions and theorems for P, FP, and PSPACE.
 - `mem_FP_pairWithInput` — an `FP` result can be paired with its original input
 - `mem_P_preimage` — `P` is closed under preimages of functions in `FP`
 - `unaryLength_mem_FP` — materializing the unary input length belongs to `FP`
+- `ite_mem_finset_mem_FP` — functions supported on a finite set belong to `FP`
 -/
 
 namespace Complexity
diff --git a/Complexitylib/Classes/P/FinsetDomain.lean b/Complexitylib/Classes/P/FinsetDomain.lean
new file mode 100644
index 00000000..b5a0eaff
--- /dev/null
+++ b/Complexitylib/Classes/P/FinsetDomain.lean
@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Complexitylib.Classes.P.FinsetDomain.Internal
+
+/-!
+# Finite-deviation functions are polynomial-time
+
+A function that agrees with the constant empty-output function on all but
+finitely many inputs is polynomial-time computable. Concretely, for any target
+function `g` and finite set `S`, the function `fun s => if s ∈ S then g s else []`
+belongs to `FP`: the finite lookup table can be hard-wired into the states of a
+Turing machine that decides membership in `S` while scanning the input and then
+emits the corresponding fixed output, all in linear time.
+
+This is the base case for building up polynomial-time functions — every function
+with finite support (relative to the empty output) is trivially in `FP`,
+regardless of how the values `g s` are chosen.
+
+## Main result
+
+- `ite_mem_finset_mem_FP` — `fun s => if s ∈ S then g s else []` belongs to `FP`
+-/
+
+namespace Complexity
+
+/-- A function that agrees with the constant empty-output function except on a
+finite set `S` — that is, `fun s => if s ∈ S then g s else []` — is computable in
+polynomial (indeed linear) time. The finite table of exceptional values is
+hard-wired into the lookup machine's states. -/
+theorem ite_mem_finset_mem_FP (g : List Bool → List Bool) (S : Finset (List Bool)) :
+    (fun s => if s ∈ S then g s else []) ∈ FP :=
+  ite_mem_finset_mem_FP_internal g S
+
+end Complexity
diff --git a/Complexitylib/Classes/P/FinsetDomain/Internal.lean b/Complexitylib/Classes/P/FinsetDomain/Internal.lean
new file mode 100644
index 00000000..bdd9eee6
--- /dev/null
+++ b/Complexitylib/Classes/P/FinsetDomain/Internal.lean
@@ -0,0 +1,458 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Mathlib.Data.Fintype.Sets
+import Mathlib.Data.Fintype.Sum
+import Mathlib.Data.Fintype.Option
+import Mathlib.Data.Finset.Lattice.Fold
+import Complexitylib.Classes.P.NormalForm
+import Complexitylib.Models.TuringMachine.Tape.Encoding
+import Complexitylib.Models.TuringMachine.Combinators
+
+/-!
+# Finite-domain lookup machine (internal)
+
+Construction and correctness of a deterministic Turing machine computing a
+function of the form `fun s => if s ∈ S then g s else []`, where `S` is a finite
+set of "inputs of interest" and `g` an arbitrary target function. Such a
+function differs from the constant empty-output function on only finitely many
+inputs, so it can be computed by a table lookup that runs in linear time.
+
+The machine has no work tapes. It works in two phases:
+
+* **Read phase.** It scans the read-only input tape left to right, tracking in
+  its finite state the prefix read so far — as long as that prefix is still a
+  prefix of some element of `S`; otherwise it enters a "dead" state. The output
+  head bumps off the left marker on the first step and then idles at cell one.
+* **Write phase.** On reaching the first input blank it knows exactly which
+  element of `S` (if any) the input was, hence which fixed output string to
+  produce. It writes that string onto the output tape, one symbol per step,
+  landing on the halting configuration.
+
+Since the read phase takes `|x|` steps and the write phase is bounded by the
+longest possible output, the runtime is linear.
+
+The public statement (`ite_mem_finset_mem_FP`) lives in
+`Complexitylib.Classes.P.FinsetDomain`.
+-/
+
+namespace Complexity
+
+namespace TM
+
+variable (g : List Bool → List Bool) (S : Finset (List Bool))
+
+/-! ## Prefix and output finsets -/
+
+/-- The finite set of all prefixes of elements of `S`. -/
+def prefixesFinset (S : Finset (List Bool)) : Finset (List Bool) :=
+  S.biUnion fun s => s.inits.toFinset
+
+theorem mem_prefixesFinset {p : List Bool} :
+    p ∈ prefixesFinset S ↔ ∃ s ∈ S, p <+: s := by
+  simp [prefixesFinset, List.mem_inits]
+
+theorem mem_prefixesFinset_self {s : List Bool} (hs : s ∈ S) :
+    s ∈ prefixesFinset S :=
+  (mem_prefixesFinset S).2 ⟨s, hs, List.prefix_rfl⟩
+
+theorem prefixesFinset_closed {p : List Bool} {a : Bool}
+    (h : p ++ [a] ∈ prefixesFinset S) : p ∈ prefixesFinset S := by
+  rw [mem_prefixesFinset] at *
+  obtain ⟨s, hs, hp⟩ := h
+  exact ⟨s, hs, (List.prefix_append p [a]).trans hp⟩
+
+/-- The possible output strings: `g s` for `s ∈ S`, together with `[]`. -/
+def outputsFinset (g : List Bool → List Bool) (S : Finset (List Bool)) :
+    Finset (List Bool) :=
+  insert [] (S.image g)
+
+/-- The reachable "remaining to write" states: suffixes of possible outputs. -/
+def writeSuffixesFinset (g : List Bool → List Bool) (S : Finset (List Bool)) :
+    Finset (List Bool) :=
+  (outputsFinset g S).biUnion fun c => c.tails.toFinset
+
+theorem mem_writeSuffixesFinset {w : List Bool} :
+    w ∈ writeSuffixesFinset g S ↔ ∃ c ∈ outputsFinset g S, w <:+ c := by
+  simp [writeSuffixesFinset, List.mem_tails]
+
+theorem nil_mem_writeSuffixesFinset :
+    ([] : List Bool) ∈ writeSuffixesFinset g S :=
+  (mem_writeSuffixesFinset g S).2 ⟨[], Finset.mem_insert_self _ _, List.nil_suffix⟩
+
+theorem writeSuffixesFinset_closed {a : Bool} {w : List Bool}
+    (h : a :: w ∈ writeSuffixesFinset g S) : w ∈ writeSuffixesFinset g S := by
+  rw [mem_writeSuffixesFinset] at *
+  obtain ⟨c, hc, hw⟩ := h
+  exact ⟨c, hc, (List.suffix_cons a w).trans hw⟩
+
+theorem output_mem_writeSuffixesFinset {input : List Bool} :
+    (if input ∈ S then g input else ([] : List Bool)) ∈ writeSuffixesFinset g S := by
+  rw [mem_writeSuffixesFinset]
+  refine ⟨_, ?_, List.suffix_refl _⟩
+  unfold outputsFinset
+  split
+  · exact Finset.mem_insert_of_mem (Finset.mem_image_of_mem g ‹_›)
+  · exact Finset.mem_insert_self _ _
+
+/-! ## The lookup machine -/
+
+/-- States of the lookup machine: either a read-phase state (an optional prefix,
+`none` being the "dead" state after diverging from every element of `S`), or a
+write-phase state (the output suffix still to be written), or the halt state. -/
+abbrev LookupState (g : List Bool → List Bool) (S : Finset (List Bool)) : Type :=
+  Option {p : List Bool // p ∈ prefixesFinset S} ⊕
+    {w : List Bool // w ∈ writeSuffixesFinset g S} ⊕ Unit
+
+instance : Fintype {p : List Bool // p ∈ prefixesFinset S} := Finset.Subtype.fintype _
+instance : Fintype {w : List Bool // w ∈ writeSuffixesFinset g S} := Finset.Subtype.fintype _
+
+instance : Fintype (LookupState g S) := by
+  unfold LookupState
+  infer_instance
+
+instance : DecidableEq (LookupState g S) := by
+  unfold LookupState
+  infer_instance
+
+/-- The read-phase state after consuming prefix `p`: the viable prefix `p` if it
+is still a prefix of some element of `S`, otherwise the dead state. -/
+def readState (p : List Bool) : LookupState g S :=
+  Sum.inl (if h : p ∈ prefixesFinset S then some ⟨p, h⟩ else none)
+
+/-- The write-phase state carrying output suffix `c`. -/
+def writeState (c : List Bool) (hc : c ∈ writeSuffixesFinset g S) : LookupState g S :=
+  Sum.inr (Sum.inl ⟨c, hc⟩)
+
+/-- The halt state. -/
+def haltState : LookupState g S := Sum.inr (Sum.inr ())
+
+/-- The lookup machine for `g` and `S`. See the module docstring for the
+construction. It has no work tapes. -/
+def lookupTM : TM 0 where
+  Q := LookupState g S
+  qstart := readState g S []
+  qhalt := haltState g S
+  δ := fun state iHead wHeads oHead =>
+    match state with
+    | Sum.inl rd =>
+      match iHead with
+      | Γ.blank =>
+        -- end of input: hand off to the write phase
+        ((match rd with
+          | some ⟨p, _⟩ =>
+            writeState g S (if p ∈ S then g p else [])
+              (output_mem_writeSuffixesFinset g S)
+          | none => writeState g S [] (nil_mem_writeSuffixesFinset g S)),
+         fun i => readBackWrite (wHeads i), readBackWrite oHead,
+         idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
+      | Γ.start =>
+        -- skip the left-end marker: move input right, keep the state
+        (Sum.inl rd,
+         fun i => readBackWrite (wHeads i), readBackWrite oHead,
+         Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
+      | Γ.zero =>
+        ((match rd with
+          | some ⟨p, _⟩ => readState g S (p ++ [false])
+          | none => Sum.inl none),
+         fun i => readBackWrite (wHeads i), readBackWrite oHead,
+         Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
+      | Γ.one =>
+        ((match rd with
+          | some ⟨p, _⟩ => readState g S (p ++ [true])
+          | none => Sum.inl none),
+         fun i => readBackWrite (wHeads i), readBackWrite oHead,
+         Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
+    | Sum.inr (Sum.inl ⟨wl, hw⟩) =>
+      match wl, hw with
+      | [], _ =>
+        (haltState g S,
+         fun i => readBackWrite (wHeads i), readBackWrite oHead,
+         idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
+      | a :: rest, hw =>
+        (writeState g S rest (writeSuffixesFinset_closed g S hw),
+         fun i => readBackWrite (wHeads i), Γw.ofBool a,
+         idleDir iHead, fun i => idleDir (wHeads i), Dir3.right)
+    | Sum.inr (Sum.inr ()) =>
+      (haltState g S,
+       fun i => readBackWrite (wHeads i), readBackWrite oHead,
+       idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
+  δ_right_of_start := by
+    intro state iHead wHeads oHead
+    match state with
+    | Sum.inl rd =>
+      match iHead with
+      | Γ.blank =>
+        exact ⟨fun h => absurd h (by decide), fun _ => idleDir_right_of_start,
+          idleDir_right_of_start⟩
+      | Γ.start =>
+        exact ⟨fun _ => rfl, fun _ => idleDir_right_of_start, idleDir_right_of_start⟩
+      | Γ.zero =>
+        exact ⟨fun h => absurd h (by decide), fun _ => idleDir_right_of_start,
+          idleDir_right_of_start⟩
+      | Γ.one =>
+        exact ⟨fun h => absurd h (by decide), fun _ => idleDir_right_of_start,
+          idleDir_right_of_start⟩
+    | Sum.inr (Sum.inl ⟨wl, hw⟩) =>
+      match wl, hw with
+      | [], _ =>
+        exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start,
+          idleDir_right_of_start⟩
+      | a :: rest, hw =>
+        exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start, fun _ => rfl⟩
+    | Sum.inr (Sum.inr ()) =>
+      exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start,
+        idleDir_right_of_start⟩
+
+/-! ## Correctness -/
+
+/-- Reading a Boolean symbol in the read phase advances the tracked prefix and
+moves the input head right. -/
+private theorem lookup_read_bit_step (p : List Bool) (b : Bool)
+    (c : Cfg 0 (lookupTM g S).Q)
+    (hstate : c.state = readState g S p)
+    (hread : c.input.read = Γ.ofBool b) :
+    (lookupTM g S).step c = some
+      { state := readState g S (p ++ [b])
+        input := c.input.move Dir3.right
+        work := fun i => (c.work i).writeAndMove (readBackWrite (c.work i).read)
+          (idleDir (c.work i).read)
+        output := c.output.writeAndMove (readBackWrite c.output.read)
+          (idleDir c.output.read) } := by
+  have hne : c.state ≠ (lookupTM g S).qhalt := by
+    rw [hstate, readState]; simp [lookupTM, haltState]
+  by_cases hp : p ∈ prefixesFinset S
+  · cases b <;>
+      simp [TM.step, lookupTM, hstate, hread, readState, haltState, dif_pos hp, Γ.ofBool]
+  · have hp' : p ++ [b] ∉ prefixesFinset S := fun h => hp (prefixesFinset_closed S h)
+    cases b <;>
+      simp [TM.step, lookupTM, hstate, hread, readState, haltState, dif_neg hp, dif_neg hp',
+        Γ.ofBool]
+
+/-- Writing back the (blank) symbol under an idle output head keeps the output
+tape an empty binary prefix. -/
+private theorem hasBinaryPrefix_idle {t : Tape} {bits : List Bool}
+    (h : t.HasBinaryPrefix bits) :
+    (t.writeAndMove (readBackWrite t.read) (idleDir t.read)).HasBinaryPrefix bits := by
+  have hread : t.read = Γ.blank := h.read_blank
+  have hne : t.read ≠ Γ.start := by rw [hread]; decide
+  rw [writeAndMove_readBack t hne]
+  have hstay : idleDir t.read = Dir3.stay := by rw [hread]; rfl
+  rw [hstay]
+  exact h
+
+/-- The read phase: from a config tracking prefix `x.take k` with the input head
+at `k + 1`, the machine consumes the remaining input in `|x| - k` steps, reaching
+the state that tracks the full input `x`. -/
+private theorem lookup_read_loop (x : List Bool) :
+    ∀ rem k (c : Cfg 0 (lookupTM g S).Q),
+      rem = x.length - k →
+      c.state = readState g S (x.take k) →
+      c.input.cells = (Tape.init (x.map Γ.ofBool)).cells →
+      c.input.head = k + 1 →
+      c.output.HasBinaryPrefix [] →
+      k ≤ x.length →
+      ∃ c',
+        (lookupTM g S).reachesIn rem c c' ∧
+        c'.state = readState g S x ∧
+        c'.input.cells = (Tape.init (x.map Γ.ofBool)).cells ∧
+        c'.input.head = x.length + 1 ∧
+        c'.output.HasBinaryPrefix [] := by
+  intro rem
+  induction rem with
+  | zero =>
+    intro k c hrem hstate hcells hhead houtput hk
+    have hk_eq : k = x.length := by omega
+    subst hk_eq
+    rw [List.take_length] at hstate
+    exact ⟨c, .zero, hstate, hcells, hhead, houtput⟩
+  | succ rem ih =>
+    intro k c hrem hstate hcells hhead houtput hk
+    have hk_lt : k < x.length := by omega
+    have hread : c.input.read = Γ.ofBool (x[k]'hk_lt) := by
+      simp [Tape.read, hhead, hcells, Tape.init_ofBool_cells_lt x k hk_lt]
+    have hstep := lookup_read_bit_step g S (x.take k) (x[k]'hk_lt) c hstate hread
+    set c1 : Cfg 0 (lookupTM g S).Q :=
+      { state := readState g S (x.take k ++ [x[k]'hk_lt])
+        input := c.input.move Dir3.right
+        work := fun i => (c.work i).writeAndMove (readBackWrite (c.work i).read)
+          (idleDir (c.work i).read)
+        output := c.output.writeAndMove (readBackWrite c.output.read)
+          (idleDir c.output.read) } with hc1
+    have htake : x.take k ++ [x[k]'hk_lt] = x.take (k + 1) := List.take_concat_get' x k hk_lt
+    have hstate1 : c1.state = readState g S (x.take (k + 1)) := by rw [hc1, htake]
+    have hcells1 : c1.input.cells = (Tape.init (x.map Γ.ofBool)).cells := by
+      simp [hc1, Tape.move_cells, hcells]
+    have hhead1 : c1.input.head = k + 1 + 1 := by simp [hc1, Tape.move, hhead]
+    have houtput1 : c1.output.HasBinaryPrefix [] := hasBinaryPrefix_idle houtput
+    obtain ⟨c', hreach, hstate', hcells', hhead', houtput'⟩ :=
+      ih (k + 1) c1 (by omega) hstate1 hcells1 hhead1 houtput1 (by omega)
+    exact ⟨c', .step hstep hreach, hstate', hcells', hhead', houtput'⟩
+
+/-- The first step skips the left-end markers: the input head advances to cell
+one over the input contents and the output head bumps off its marker. -/
+private theorem lookup_initial_step (x : List Bool) :
+    ∃ c0, (lookupTM g S).step ((lookupTM g S).initCfg x) = some c0 ∧
+      c0.state = readState g S [] ∧
+      c0.input.cells = (Tape.init (x.map Γ.ofBool)).cells ∧
+      c0.input.head = 1 ∧
+      c0.output.HasBinaryPrefix [] := by
+  set c0 : Cfg 0 (lookupTM g S).Q :=
+    { state := readState g S []
+      input := (Tape.init (x.map Γ.ofBool)).move Dir3.right
+      work := fun _ => (Tape.init []).move Dir3.right
+      output := (Tape.init ([] : List Γ)).move Dir3.right } with hc0
+  have hg : ((lookupTM g S).initCfg x).state ≠ (lookupTM g S).qhalt := by
+    simp [lookupTM, readState, haltState]
+  have hstep : (lookupTM g S).step ((lookupTM g S).initCfg x) = some c0 := by
+    simp only [TM.step, if_neg hg]
+    exact congrArg some (Cfg.ext rfl rfl (Subsingleton.elim _ _) rfl)
+  refine ⟨c0, hstep, rfl, ?_, ?_, ?_⟩
+  · rw [hc0]; simp [Tape.move_cells]
+  · rw [hc0]; simp [Tape.move]
+  · rw [hc0]; exact Tape.init_nil_move_right_hasBinaryPrefix_nil
+
+/-- The handoff step from read phase to write phase: on reaching the input blank
+the machine commits to writing the fixed output `if inp ∈ S then g inp else []`. -/
+private theorem lookup_handoff_step (inp : List Bool) (c : Cfg 0 (lookupTM g S).Q)
+    (hstate : c.state = readState g S inp)
+    (hread : c.input.read = Γ.blank)
+    (houtput : c.output.HasBinaryPrefix []) :
+    ∃ c', (lookupTM g S).step c = some c' ∧
+      c'.state = writeState g S (if inp ∈ S then g inp else [])
+        (output_mem_writeSuffixesFinset g S) ∧
+      c'.output.HasBinaryPrefix [] := by
+  set c1 : Cfg 0 (lookupTM g S).Q :=
+    { state := writeState g S (if inp ∈ S then g inp else [])
+        (output_mem_writeSuffixesFinset g S)
+      input := c.input.move (idleDir c.input.read)
+      work := fun i => (c.work i).writeAndMove (readBackWrite (c.work i).read)
+        (idleDir (c.work i).read)
+      output := c.output.writeAndMove (readBackWrite c.output.read)
+        (idleDir c.output.read) } with hc1
+  have hstep : (lookupTM g S).step c = some c1 := by
+    by_cases hp : inp ∈ prefixesFinset S
+    · simp [TM.step, lookupTM, hstate, hread, readState, writeState, haltState, dif_pos hp, hc1]
+    · have hpS : inp ∉ S := fun h => hp (mem_prefixesFinset_self S h)
+      simp [TM.step, lookupTM, hstate, hread, readState, writeState, haltState, dif_neg hp,
+        if_neg hpS, hc1]
+  refine ⟨c1, hstep, by rw [hc1], ?_⟩
+  rw [hc1]
+  exact hasBinaryPrefix_idle houtput
+
+/-- Writing one output symbol in the write phase extends the written prefix and
+advances to the remaining suffix. -/
+private theorem lookup_write_cons_step (a : Bool) (rest : List Bool)
+    (hw : a :: rest ∈ writeSuffixesFinset g S) (c : Cfg 0 (lookupTM g S).Q)
+    (hstate : c.state = writeState g S (a :: rest) hw) :
+    (lookupTM g S).step c = some
+      { state := writeState g S rest (writeSuffixesFinset_closed g S hw)
+        input := c.input.move (idleDir c.input.read)
+        work := fun i => (c.work i).writeAndMove (readBackWrite (c.work i).read)
+          (idleDir (c.work i).read)
+        output := c.output.writeAndMove (Γ.ofBool a) Dir3.right } := by
+  cases a <;> simp [TM.step, lookupTM, hstate, writeState, haltState, Γ.ofBool, Γw.ofBool]
+
+/-- The write phase: from a config whose output already holds `written` and whose
+state carries the remaining suffix `w`, the machine writes `w` and halts, in
+`|w| + 1` steps, leaving `written ++ w` on the output tape. -/
+private theorem lookup_write_loop (written : List Bool) :
+    ∀ (w : List Bool) (hw : w ∈ writeSuffixesFinset g S) (c : Cfg 0 (lookupTM g S).Q),
+      c.state = writeState g S w hw →
+      c.output.HasBinaryPrefix written →
+      ∃ c',
+        (lookupTM g S).reachesIn (w.length + 1) c c' ∧
+        (lookupTM g S).halted c' ∧
+        c'.output.HasBinaryPrefix (written ++ w) := by
+  intro w
+  induction w generalizing written with
+  | nil =>
+    intro hw c hstate houtput
+    have hne : c.state ≠ (lookupTM g S).qhalt := by
+      rw [hstate, writeState]; simp [lookupTM, haltState]
+    set c1 : Cfg 0 (lookupTM g S).Q :=
+      { state := haltState g S
+        input := c.input.move (idleDir c.input.read)
+        work := fun i => (c.work i).writeAndMove (readBackWrite (c.work i).read)
+          (idleDir (c.work i).read)
+        output := c.output.writeAndMove (readBackWrite c.output.read)
+          (idleDir c.output.read) } with hc1
+    have hstep : (lookupTM g S).step c = some c1 := by
+      simp [TM.step, lookupTM, hstate, writeState, haltState, hc1]
+    refine ⟨c1, .step hstep .zero, ?_, ?_⟩
+    · show c1.state = (lookupTM g S).qhalt
+      rw [hc1]; rfl
+    · rw [List.append_nil, hc1]
+      exact hasBinaryPrefix_idle houtput
+  | cons a rest ih =>
+    intro hw c hstate houtput
+    have hstep := lookup_write_cons_step g S a rest hw c hstate
+    set c1 : Cfg 0 (lookupTM g S).Q :=
+      { state := writeState g S rest (writeSuffixesFinset_closed g S hw)
+        input := c.input.move (idleDir c.input.read)
+        work := fun i => (c.work i).writeAndMove (readBackWrite (c.work i).read)
+          (idleDir (c.work i).read)
+        output := c.output.writeAndMove (Γ.ofBool a) Dir3.right } with hc1
+    have hout1 : c1.output.HasBinaryPrefix (written ++ [a]) := by
+      rw [hc1]; exact Tape.hasBinaryPrefix_write_bit a houtput
+    obtain ⟨c', hreach, hhalt, hout'⟩ :=
+      ih (written ++ [a]) (writeSuffixesFinset_closed g S hw) c1 rfl hout1
+    refine ⟨c', ?_, hhalt, ?_⟩
+    · have : rest.length + 1 + 1 = (a :: rest).length + 1 := by simp [List.length_cons]
+      rw [← this]
+      exact .step hstep hreach
+    · rwa [List.append_assoc, List.singleton_append] at hout'
+
+/-- The lookup machine computes `fun s => if s ∈ S then g s else []` within a
+linear time bound. -/
+theorem lookupTM_computesInTime :
+    (lookupTM g S).ComputesInTime (fun s => if s ∈ S then g s else [])
+      (fun m => m + (S.sup fun s => (g s).length) + 3) := by
+  intro x
+  obtain ⟨c0, hstep0, hst0, hcells0, hhead0, hout0⟩ := lookup_initial_step g S x
+  obtain ⟨c1, hreadloop, hst1, hcells1, hhead1, hout1⟩ :=
+    lookup_read_loop g S x x.length 0 c0 (by omega) hst0 hcells0 hhead0 hout0 (Nat.zero_le _)
+  have hread1_blank : c1.input.read = Γ.blank := by
+    rw [Tape.read, hhead1, hcells1, Tape.init_ofBool_cells_ge x x.length le_rfl]
+  obtain ⟨c2, hstep2, hst2, hout2⟩ := lookup_handoff_step g S x c1 hst1 hread1_blank hout1
+  set cval : List Bool := if x ∈ S then g x else [] with hcval
+  obtain ⟨c3, hwriteloop, hhalt3, hout3⟩ :=
+    lookup_write_loop g S [] cval (output_mem_writeSuffixesFinset g S) c2 hst2 hout2
+  have hlen : cval.length ≤ S.sup fun s => (g s).length := by
+    rw [hcval]
+    split
+    · exact Finset.le_sup (f := fun s => (g s).length) ‹x ∈ S›
+    · exact Nat.zero_le _
+  refine ⟨c3, x.length + cval.length + 3, by dsimp only; omega, ?_, hhalt3, ?_⟩
+  · have hreach :=
+      reachesIn.step hstep0
+        (reachesIn_trans (lookupTM g S) hreadloop
+          (reachesIn.step hstep2 hwriteloop))
+    have heq : x.length + (cval.length + 1 + 1) + 1 = x.length + cval.length + 3 := by omega
+    rwa [heq] at hreach
+  · have hres : c3.output.HasOutput cval := by
+      have h := hout3
+      rw [List.nil_append] at h
+      exact h.hasOutput
+    exact hres
+
+end TM
+
+open Polynomial in
+/-- Internal proof that a function supported on a finite set belongs to `FP`:
+the lookup machine's linear time bound is packaged as a degree-one polynomial. -/
+theorem ite_mem_finset_mem_FP_internal (g : List Bool → List Bool) (S : Finset (List Bool)) :
+    (fun s => if s ∈ S then g s else []) ∈ FP := by
+  rw [mem_FP_iff_computesInTime_polynomial]
+  refine ⟨0, TM.lookupTM g S, X + C ((S.sup fun s => (g s).length) + 3), ?_⟩
+  have heval : (X + C ((S.sup fun s => (g s).length) + 3)).eval
+      = fun m : ℕ => m + (S.sup fun s => (g s).length) + 3 := by
+    funext m
+    simp only [eval_add, eval_X, eval_C]
+    omega
+  rw [heval]
+  exact TM.lookupTM_computesInTime g S
+
+end Complexity

From 763fc956bd82d4a096ca3e7d504ad3d7d820b43d Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 24 Jul 2026 10:57:02 -0700
Subject: [PATCH 2/5] refactor state

---
 .../Classes/P/FinsetDomain/Internal.lean      | 75 ++++++++-----------
 1 file changed, 33 insertions(+), 42 deletions(-)

diff --git a/Complexitylib/Classes/P/FinsetDomain/Internal.lean b/Complexitylib/Classes/P/FinsetDomain/Internal.lean
index bdd9eee6..70e4fc3b 100644
--- a/Complexitylib/Classes/P/FinsetDomain/Internal.lean
+++ b/Complexitylib/Classes/P/FinsetDomain/Internal.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bolton Bailey
 -/
 import Mathlib.Data.Fintype.Sets
-import Mathlib.Data.Fintype.Sum
 import Mathlib.Data.Fintype.Option
 import Mathlib.Data.Finset.Lattice.Fold
 import Complexitylib.Classes.P.NormalForm
@@ -99,35 +98,31 @@ theorem output_mem_writeSuffixesFinset {input : List Bool} :
 
 /-! ## The lookup machine -/
 
-/-- States of the lookup machine: either a read-phase state (an optional prefix,
-`none` being the "dead" state after diverging from every element of `S`), or a
-write-phase state (the output suffix still to be written), or the halt state. -/
-abbrev LookupState (g : List Bool → List Bool) (S : Finset (List Bool)) : Type :=
-  Option {p : List Bool // p ∈ prefixesFinset S} ⊕
-    {w : List Bool // w ∈ writeSuffixesFinset g S} ⊕ Unit
-
 instance : Fintype {p : List Bool // p ∈ prefixesFinset S} := Finset.Subtype.fintype _
 instance : Fintype {w : List Bool // w ∈ writeSuffixesFinset g S} := Finset.Subtype.fintype _
 
-instance : Fintype (LookupState g S) := by
-  unfold LookupState
-  infer_instance
-
-instance : DecidableEq (LookupState g S) := by
-  unfold LookupState
-  infer_instance
+/-- States of the lookup machine. -/
+inductive LookupState (g : List Bool → List Bool) (S : Finset (List Bool)) : Type where
+  /-- Read phase: the viable prefix consumed so far, `none` being the "dead"
+  state after diverging from every element of `S`. -/
+  | read (p : Option {p : List Bool // p ∈ prefixesFinset S}) : LookupState g S
+  /-- Write phase: the output suffix still to be written. -/
+  | write (w : {w : List Bool // w ∈ writeSuffixesFinset g S}) : LookupState g S
+  /-- The halt state. -/
+  | halt : LookupState g S
+  deriving DecidableEq, Fintype
 
 /-- The read-phase state after consuming prefix `p`: the viable prefix `p` if it
 is still a prefix of some element of `S`, otherwise the dead state. -/
 def readState (p : List Bool) : LookupState g S :=
-  Sum.inl (if h : p ∈ prefixesFinset S then some ⟨p, h⟩ else none)
+  .read (if h : p ∈ prefixesFinset S then some ⟨p, h⟩ else none)
 
 /-- The write-phase state carrying output suffix `c`. -/
 def writeState (c : List Bool) (hc : c ∈ writeSuffixesFinset g S) : LookupState g S :=
-  Sum.inr (Sum.inl ⟨c, hc⟩)
+  .write ⟨c, hc⟩
 
 /-- The halt state. -/
-def haltState : LookupState g S := Sum.inr (Sum.inr ())
+def haltState : LookupState g S := .halt
 
 /-- The lookup machine for `g` and `S`. See the module docstring for the
 construction. It has no work tapes. -/
@@ -137,7 +132,7 @@ def lookupTM : TM 0 where
   qhalt := haltState g S
   δ := fun state iHead wHeads oHead =>
     match state with
-    | Sum.inl rd =>
+    | .read rd =>
       match iHead with
       | Γ.blank =>
         -- end of input: hand off to the write phase
@@ -150,39 +145,37 @@ def lookupTM : TM 0 where
          idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
       | Γ.start =>
         -- skip the left-end marker: move input right, keep the state
-        (Sum.inl rd,
+        (.read rd,
          fun i => readBackWrite (wHeads i), readBackWrite oHead,
          Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
       | Γ.zero =>
         ((match rd with
           | some ⟨p, _⟩ => readState g S (p ++ [false])
-          | none => Sum.inl none),
+          | none => .read none),
          fun i => readBackWrite (wHeads i), readBackWrite oHead,
          Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
       | Γ.one =>
         ((match rd with
           | some ⟨p, _⟩ => readState g S (p ++ [true])
-          | none => Sum.inl none),
+          | none => .read none),
          fun i => readBackWrite (wHeads i), readBackWrite oHead,
          Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
-    | Sum.inr (Sum.inl ⟨wl, hw⟩) =>
-      match wl, hw with
-      | [], _ =>
-        (haltState g S,
-         fun i => readBackWrite (wHeads i), readBackWrite oHead,
-         idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
-      | a :: rest, hw =>
-        (writeState g S rest (writeSuffixesFinset_closed g S hw),
-         fun i => readBackWrite (wHeads i), Γw.ofBool a,
-         idleDir iHead, fun i => idleDir (wHeads i), Dir3.right)
-    | Sum.inr (Sum.inr ()) =>
+    | .write ⟨[], _⟩ =>
+      (haltState g S,
+       fun i => readBackWrite (wHeads i), readBackWrite oHead,
+       idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
+    | .write ⟨a :: rest, hw⟩ =>
+      (writeState g S rest (writeSuffixesFinset_closed g S hw),
+       fun i => readBackWrite (wHeads i), Γw.ofBool a,
+       idleDir iHead, fun i => idleDir (wHeads i), Dir3.right)
+    | .halt =>
       (haltState g S,
        fun i => readBackWrite (wHeads i), readBackWrite oHead,
        idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
   δ_right_of_start := by
     intro state iHead wHeads oHead
     match state with
-    | Sum.inl rd =>
+    | .read rd =>
       match iHead with
       | Γ.blank =>
         exact ⟨fun h => absurd h (by decide), fun _ => idleDir_right_of_start,
@@ -195,14 +188,12 @@ def lookupTM : TM 0 where
       | Γ.one =>
         exact ⟨fun h => absurd h (by decide), fun _ => idleDir_right_of_start,
           idleDir_right_of_start⟩
-    | Sum.inr (Sum.inl ⟨wl, hw⟩) =>
-      match wl, hw with
-      | [], _ =>
-        exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start,
-          idleDir_right_of_start⟩
-      | a :: rest, hw =>
-        exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start, fun _ => rfl⟩
-    | Sum.inr (Sum.inr ()) =>
+    | .write ⟨[], _⟩ =>
+      exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start,
+        idleDir_right_of_start⟩
+    | .write ⟨a :: rest, hw⟩ =>
+      exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start, fun _ => rfl⟩
+    | .halt =>
       exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start,
         idleDir_right_of_start⟩
 

From bb825c55c88894d69b7c7a1b4607ecba01784635 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 24 Jul 2026 20:00:36 -0700
Subject: [PATCH 3/5] change namespace

---
 Complexitylib/Classes/P/FinsetDomain/Internal.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Complexitylib/Classes/P/FinsetDomain/Internal.lean b/Complexitylib/Classes/P/FinsetDomain/Internal.lean
index 70e4fc3b..fbe03d3e 100644
--- a/Complexitylib/Classes/P/FinsetDomain/Internal.lean
+++ b/Complexitylib/Classes/P/FinsetDomain/Internal.lean
@@ -39,7 +39,7 @@ The public statement (`ite_mem_finset_mem_FP`) lives in
 
 namespace Complexity
 
-namespace TM
+namespace TM.FinsetDomain
 
 variable (g : List Bool → List Bool) (S : Finset (List Bool))
 
@@ -429,7 +429,7 @@ theorem lookupTM_computesInTime :
       exact h.hasOutput
     exact hres
 
-end TM
+end TM.FinsetDomain
 
 open Polynomial in
 /-- Internal proof that a function supported on a finite set belongs to `FP`:
@@ -437,13 +437,13 @@ the lookup machine's linear time bound is packaged as a degree-one polynomial. -
 theorem ite_mem_finset_mem_FP_internal (g : List Bool → List Bool) (S : Finset (List Bool)) :
     (fun s => if s ∈ S then g s else []) ∈ FP := by
   rw [mem_FP_iff_computesInTime_polynomial]
-  refine ⟨0, TM.lookupTM g S, X + C ((S.sup fun s => (g s).length) + 3), ?_⟩
+  refine ⟨0, TM.FinsetDomain.lookupTM g S, X + C ((S.sup fun s => (g s).length) + 3), ?_⟩
   have heval : (X + C ((S.sup fun s => (g s).length) + 3)).eval
       = fun m : ℕ => m + (S.sup fun s => (g s).length) + 3 := by
     funext m
     simp only [eval_add, eval_X, eval_C]
     omega
   rw [heval]
-  exact TM.lookupTM_computesInTime g S
+  exact TM.FinsetDomain.lookupTM_computesInTime g S
 
 end Complexity

From 72a6905ce9bab0fb80a7062733ba15e71cf10225 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 25 Jul 2026 07:38:54 -0700
Subject: [PATCH 4/5] prefixes refactor

---
 .../Classes/P/FinsetDomain/Internal.lean      | 104 +++++++-----------
 Complexitylib/Mathlib/FinsetPrefixes.lean     |  67 +++++++++++
 2 files changed, 108 insertions(+), 63 deletions(-)
 create mode 100644 Complexitylib/Mathlib/FinsetPrefixes.lean

diff --git a/Complexitylib/Classes/P/FinsetDomain/Internal.lean b/Complexitylib/Classes/P/FinsetDomain/Internal.lean
index fbe03d3e..3fc642e2 100644
--- a/Complexitylib/Classes/P/FinsetDomain/Internal.lean
+++ b/Complexitylib/Classes/P/FinsetDomain/Internal.lean
@@ -6,6 +6,7 @@ Authors: Bolton Bailey
 import Mathlib.Data.Fintype.Sets
 import Mathlib.Data.Fintype.Option
 import Mathlib.Data.Finset.Lattice.Fold
+import Complexitylib.Mathlib.FinsetPrefixes
 import Complexitylib.Classes.P.NormalForm
 import Complexitylib.Models.TuringMachine.Tape.Encoding
 import Complexitylib.Models.TuringMachine.Combinators
@@ -43,54 +44,24 @@ namespace TM.FinsetDomain
 
 variable (g : List Bool → List Bool) (S : Finset (List Bool))
 
-/-! ## Prefix and output finsets -/
+/-! ## Output finset
 
-/-- The finite set of all prefixes of elements of `S`. -/
-def prefixesFinset (S : Finset (List Bool)) : Finset (List Bool) :=
-  S.biUnion fun s => s.inits.toFinset
-
-theorem mem_prefixesFinset {p : List Bool} :
-    p ∈ prefixesFinset S ↔ ∃ s ∈ S, p <+: s := by
-  simp [prefixesFinset, List.mem_inits]
-
-theorem mem_prefixesFinset_self {s : List Bool} (hs : s ∈ S) :
-    s ∈ prefixesFinset S :=
-  (mem_prefixesFinset S).2 ⟨s, hs, List.prefix_rfl⟩
-
-theorem prefixesFinset_closed {p : List Bool} {a : Bool}
-    (h : p ++ [a] ∈ prefixesFinset S) : p ∈ prefixesFinset S := by
-  rw [mem_prefixesFinset] at *
-  obtain ⟨s, hs, hp⟩ := h
-  exact ⟨s, hs, (List.prefix_append p [a]).trans hp⟩
+The read phase tracks membership in `S.prefixes` and the write phase tracks
+membership in `(outputsFinset g S).suffixes`; both finsets come from the
+generic `Finset.prefixes`/`Finset.suffixes` API. -/
 
 /-- The possible output strings: `g s` for `s ∈ S`, together with `[]`. -/
 def outputsFinset (g : List Bool → List Bool) (S : Finset (List Bool)) :
     Finset (List Bool) :=
   insert [] (S.image g)
 
-/-- The reachable "remaining to write" states: suffixes of possible outputs. -/
-def writeSuffixesFinset (g : List Bool → List Bool) (S : Finset (List Bool)) :
-    Finset (List Bool) :=
-  (outputsFinset g S).biUnion fun c => c.tails.toFinset
-
-theorem mem_writeSuffixesFinset {w : List Bool} :
-    w ∈ writeSuffixesFinset g S ↔ ∃ c ∈ outputsFinset g S, w <:+ c := by
-  simp [writeSuffixesFinset, List.mem_tails]
-
-theorem nil_mem_writeSuffixesFinset :
-    ([] : List Bool) ∈ writeSuffixesFinset g S :=
-  (mem_writeSuffixesFinset g S).2 ⟨[], Finset.mem_insert_self _ _, List.nil_suffix⟩
-
-theorem writeSuffixesFinset_closed {a : Bool} {w : List Bool}
-    (h : a :: w ∈ writeSuffixesFinset g S) : w ∈ writeSuffixesFinset g S := by
-  rw [mem_writeSuffixesFinset] at *
-  obtain ⟨c, hc, hw⟩ := h
-  exact ⟨c, hc, (List.suffix_cons a w).trans hw⟩
-
-theorem output_mem_writeSuffixesFinset {input : List Bool} :
-    (if input ∈ S then g input else ([] : List Bool)) ∈ writeSuffixesFinset g S := by
-  rw [mem_writeSuffixesFinset]
-  refine ⟨_, ?_, List.suffix_refl _⟩
+theorem nil_mem_suffixes_outputsFinset :
+    ([] : List Bool) ∈ (outputsFinset g S).suffixes :=
+  Finset.nil_mem_suffixes ⟨[], Finset.mem_insert_self _ _⟩
+
+theorem output_mem_suffixes_outputsFinset {input : List Bool} :
+    (if input ∈ S then g input else ([] : List Bool)) ∈ (outputsFinset g S).suffixes := by
+  refine Finset.mem_suffixes_self ?_
   unfold outputsFinset
   split
   · exact Finset.mem_insert_of_mem (Finset.mem_image_of_mem g ‹_›)
@@ -98,16 +69,22 @@ theorem output_mem_writeSuffixesFinset {input : List Bool} :
 
 /-! ## The lookup machine -/
 
-instance : Fintype {p : List Bool // p ∈ prefixesFinset S} := Finset.Subtype.fintype _
-instance : Fintype {w : List Bool // w ∈ writeSuffixesFinset g S} := Finset.Subtype.fintype _
+instance : Fintype {p : List Bool // p ∈ S.prefixes} := Finset.Subtype.fintype _
+instance : Fintype {w : List Bool // w ∈ (outputsFinset g S).suffixes} :=
+  Finset.Subtype.fintype _
 
 /-- States of the lookup machine. -/
 inductive LookupState (g : List Bool → List Bool) (S : Finset (List Bool)) : Type where
   /-- Read phase: the viable prefix consumed so far, `none` being the "dead"
-  state after diverging from every element of `S`. -/
-  | read (p : Option {p : List Bool // p ∈ prefixesFinset S}) : LookupState g S
+  state after diverging from every element of `S`.
+
+  TODO: Avoid use of Option, make a separate constructor for the dead state.
+  Also, instead of passing a subtype as arg, pass the value and proof of membership
+  separately, so that the proof can be used in the transition function.
+  -/
+  | read (p : Option {p : List Bool // p ∈ S.prefixes}) : LookupState g S
   /-- Write phase: the output suffix still to be written. -/
-  | write (w : {w : List Bool // w ∈ writeSuffixesFinset g S}) : LookupState g S
+  | write (w : {w : List Bool // w ∈ (outputsFinset g S).suffixes}) : LookupState g S
   /-- The halt state. -/
   | halt : LookupState g S
   deriving DecidableEq, Fintype
@@ -115,10 +92,10 @@ inductive LookupState (g : List Bool → List Bool) (S : Finset (List Bool)) : T
 /-- The read-phase state after consuming prefix `p`: the viable prefix `p` if it
 is still a prefix of some element of `S`, otherwise the dead state. -/
 def readState (p : List Bool) : LookupState g S :=
-  .read (if h : p ∈ prefixesFinset S then some ⟨p, h⟩ else none)
+  .read (if h : p ∈ S.prefixes then some ⟨p, h⟩ else none)
 
 /-- The write-phase state carrying output suffix `c`. -/
-def writeState (c : List Bool) (hc : c ∈ writeSuffixesFinset g S) : LookupState g S :=
+def writeState (c : List Bool) (hc : c ∈ (outputsFinset g S).suffixes) : LookupState g S :=
   .write ⟨c, hc⟩
 
 /-- The halt state. -/
@@ -139,8 +116,8 @@ def lookupTM : TM 0 where
         ((match rd with
           | some ⟨p, _⟩ =>
             writeState g S (if p ∈ S then g p else [])
-              (output_mem_writeSuffixesFinset g S)
-          | none => writeState g S [] (nil_mem_writeSuffixesFinset g S)),
+              (output_mem_suffixes_outputsFinset g S)
+          | none => writeState g S [] (nil_mem_suffixes_outputsFinset g S)),
          fun i => readBackWrite (wHeads i), readBackWrite oHead,
          idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
       | Γ.start =>
@@ -165,7 +142,7 @@ def lookupTM : TM 0 where
        fun i => readBackWrite (wHeads i), readBackWrite oHead,
        idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
     | .write ⟨a :: rest, hw⟩ =>
-      (writeState g S rest (writeSuffixesFinset_closed g S hw),
+      (writeState g S rest (Finset.mem_suffixes_of_suffix (List.suffix_cons a rest) hw),
        fun i => readBackWrite (wHeads i), Γw.ofBool a,
        idleDir iHead, fun i => idleDir (wHeads i), Dir3.right)
     | .halt =>
@@ -214,10 +191,11 @@ private theorem lookup_read_bit_step (p : List Bool) (b : Bool)
           (idleDir c.output.read) } := by
   have hne : c.state ≠ (lookupTM g S).qhalt := by
     rw [hstate, readState]; simp [lookupTM, haltState]
-  by_cases hp : p ∈ prefixesFinset S
+  by_cases hp : p ∈ S.prefixes
   · cases b <;>
       simp [TM.step, lookupTM, hstate, hread, readState, haltState, dif_pos hp, Γ.ofBool]
-  · have hp' : p ++ [b] ∉ prefixesFinset S := fun h => hp (prefixesFinset_closed S h)
+  · have hp' : p ++ [b] ∉ S.prefixes := fun h =>
+      hp (Finset.mem_prefixes_of_prefix (List.prefix_append p [b]) h)
     cases b <;>
       simp [TM.step, lookupTM, hstate, hread, readState, haltState, dif_neg hp, dif_neg hp',
         Γ.ofBool]
@@ -313,20 +291,20 @@ private theorem lookup_handoff_step (inp : List Bool) (c : Cfg 0 (lookupTM g S).
     (houtput : c.output.HasBinaryPrefix []) :
     ∃ c', (lookupTM g S).step c = some c' ∧
       c'.state = writeState g S (if inp ∈ S then g inp else [])
-        (output_mem_writeSuffixesFinset g S) ∧
+        (output_mem_suffixes_outputsFinset g S) ∧
       c'.output.HasBinaryPrefix [] := by
   set c1 : Cfg 0 (lookupTM g S).Q :=
     { state := writeState g S (if inp ∈ S then g inp else [])
-        (output_mem_writeSuffixesFinset g S)
+        (output_mem_suffixes_outputsFinset g S)
       input := c.input.move (idleDir c.input.read)
       work := fun i => (c.work i).writeAndMove (readBackWrite (c.work i).read)
         (idleDir (c.work i).read)
       output := c.output.writeAndMove (readBackWrite c.output.read)
         (idleDir c.output.read) } with hc1
   have hstep : (lookupTM g S).step c = some c1 := by
-    by_cases hp : inp ∈ prefixesFinset S
+    by_cases hp : inp ∈ S.prefixes
     · simp [TM.step, lookupTM, hstate, hread, readState, writeState, haltState, dif_pos hp, hc1]
-    · have hpS : inp ∉ S := fun h => hp (mem_prefixesFinset_self S h)
+    · have hpS : inp ∉ S := fun h => hp (Finset.mem_prefixes_self h)
       simp [TM.step, lookupTM, hstate, hread, readState, writeState, haltState, dif_neg hp,
         if_neg hpS, hc1]
   refine ⟨c1, hstep, by rw [hc1], ?_⟩
@@ -336,10 +314,10 @@ private theorem lookup_handoff_step (inp : List Bool) (c : Cfg 0 (lookupTM g S).
 /-- Writing one output symbol in the write phase extends the written prefix and
 advances to the remaining suffix. -/
 private theorem lookup_write_cons_step (a : Bool) (rest : List Bool)
-    (hw : a :: rest ∈ writeSuffixesFinset g S) (c : Cfg 0 (lookupTM g S).Q)
+    (hw : a :: rest ∈ (outputsFinset g S).suffixes) (c : Cfg 0 (lookupTM g S).Q)
     (hstate : c.state = writeState g S (a :: rest) hw) :
     (lookupTM g S).step c = some
-      { state := writeState g S rest (writeSuffixesFinset_closed g S hw)
+      { state := writeState g S rest (Finset.mem_suffixes_of_suffix (List.suffix_cons a rest) hw)
         input := c.input.move (idleDir c.input.read)
         work := fun i => (c.work i).writeAndMove (readBackWrite (c.work i).read)
           (idleDir (c.work i).read)
@@ -350,7 +328,7 @@ private theorem lookup_write_cons_step (a : Bool) (rest : List Bool)
 state carries the remaining suffix `w`, the machine writes `w` and halts, in
 `|w| + 1` steps, leaving `written ++ w` on the output tape. -/
 private theorem lookup_write_loop (written : List Bool) :
-    ∀ (w : List Bool) (hw : w ∈ writeSuffixesFinset g S) (c : Cfg 0 (lookupTM g S).Q),
+    ∀ (w : List Bool) (hw : w ∈ (outputsFinset g S).suffixes) (c : Cfg 0 (lookupTM g S).Q),
       c.state = writeState g S w hw →
       c.output.HasBinaryPrefix written →
       ∃ c',
@@ -381,7 +359,7 @@ private theorem lookup_write_loop (written : List Bool) :
     intro hw c hstate houtput
     have hstep := lookup_write_cons_step g S a rest hw c hstate
     set c1 : Cfg 0 (lookupTM g S).Q :=
-      { state := writeState g S rest (writeSuffixesFinset_closed g S hw)
+      { state := writeState g S rest (Finset.mem_suffixes_of_suffix (List.suffix_cons a rest) hw)
         input := c.input.move (idleDir c.input.read)
         work := fun i => (c.work i).writeAndMove (readBackWrite (c.work i).read)
           (idleDir (c.work i).read)
@@ -389,7 +367,7 @@ private theorem lookup_write_loop (written : List Bool) :
     have hout1 : c1.output.HasBinaryPrefix (written ++ [a]) := by
       rw [hc1]; exact Tape.hasBinaryPrefix_write_bit a houtput
     obtain ⟨c', hreach, hhalt, hout'⟩ :=
-      ih (written ++ [a]) (writeSuffixesFinset_closed g S hw) c1 rfl hout1
+      ih (written ++ [a]) (Finset.mem_suffixes_of_suffix (List.suffix_cons a rest) hw) c1 rfl hout1
     refine ⟨c', ?_, hhalt, ?_⟩
     · have : rest.length + 1 + 1 = (a :: rest).length + 1 := by simp [List.length_cons]
       rw [← this]
@@ -410,7 +388,7 @@ theorem lookupTM_computesInTime :
   obtain ⟨c2, hstep2, hst2, hout2⟩ := lookup_handoff_step g S x c1 hst1 hread1_blank hout1
   set cval : List Bool := if x ∈ S then g x else [] with hcval
   obtain ⟨c3, hwriteloop, hhalt3, hout3⟩ :=
-    lookup_write_loop g S [] cval (output_mem_writeSuffixesFinset g S) c2 hst2 hout2
+    lookup_write_loop g S [] cval (output_mem_suffixes_outputsFinset g S) c2 hst2 hout2
   have hlen : cval.length ≤ S.sup fun s => (g s).length := by
     rw [hcval]
     split
diff --git a/Complexitylib/Mathlib/FinsetPrefixes.lean b/Complexitylib/Mathlib/FinsetPrefixes.lean
new file mode 100644
index 00000000..f3ae5f15
--- /dev/null
+++ b/Complexitylib/Mathlib/FinsetPrefixes.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Mathlib.Data.Finset.Union
+import Mathlib.Data.List.Infix
+
+/-!
+# Finsets of prefixes and suffixes
+
+For a finite set `S` of lists, `Finset.prefixes S` is the finite set of all
+prefixes of elements of `S`, and `Finset.suffixes S` the finite set of all
+suffixes of elements of `S`. The two operations have dual APIs: membership
+characterizations (`mem_prefixes`/`mem_suffixes`), self-membership, and
+closure under taking further prefixes/suffixes.
+
+This file lives in `Complexitylib/Mathlib/` because it extends a Mathlib
+type in its home namespace — the sanctioned exception to the `Complexity`
+root-namespace rule. Its contents are candidates for upstreaming to Mathlib.
+-/
+
+namespace Finset
+
+variable {α : Type*} [DecidableEq α] {S : Finset (List α)}
+
+/-- The finite set of all prefixes of elements of `S`. -/
+def prefixes (S : Finset (List α)) : Finset (List α) :=
+  S.biUnion fun s => s.inits.toFinset
+
+/-- The finite set of all suffixes of elements of `S`. -/
+def suffixes (S : Finset (List α)) : Finset (List α) :=
+  S.biUnion fun s => s.tails.toFinset
+
+theorem mem_prefixes {p : List α} : p ∈ S.prefixes ↔ ∃ s ∈ S, p <+: s := by
+  simp [prefixes, List.mem_inits]
+
+theorem mem_suffixes {w : List α} : w ∈ S.suffixes ↔ ∃ s ∈ S, w <:+ s := by
+  simp [suffixes, List.mem_tails]
+
+theorem mem_prefixes_self {s : List α} (hs : s ∈ S) : s ∈ S.prefixes :=
+  mem_prefixes.2 ⟨s, hs, List.prefix_rfl⟩
+
+theorem mem_suffixes_self {s : List α} (hs : s ∈ S) : s ∈ S.suffixes :=
+  mem_suffixes.2 ⟨s, hs, List.suffix_rfl⟩
+
+theorem nil_mem_prefixes (hS : S.Nonempty) : ([] : List α) ∈ S.prefixes :=
+  let ⟨s, hs⟩ := hS
+  mem_prefixes.2 ⟨s, hs, List.nil_prefix⟩
+
+theorem nil_mem_suffixes (hS : S.Nonempty) : ([] : List α) ∈ S.suffixes :=
+  let ⟨s, hs⟩ := hS
+  mem_suffixes.2 ⟨s, hs, List.nil_suffix⟩
+
+/-- `S.prefixes` is downward closed under taking prefixes. -/
+theorem mem_prefixes_of_prefix {p q : List α} (hpq : p <+: q) (hq : q ∈ S.prefixes) :
+    p ∈ S.prefixes := by
+  obtain ⟨s, hs, hqs⟩ := mem_prefixes.1 hq
+  exact mem_prefixes.2 ⟨s, hs, hpq.trans hqs⟩
+
+/-- `S.suffixes` is downward closed under taking suffixes. -/
+theorem mem_suffixes_of_suffix {w v : List α} (hwv : w <:+ v) (hv : v ∈ S.suffixes) :
+    w ∈ S.suffixes := by
+  obtain ⟨s, hs, hvs⟩ := mem_suffixes.1 hv
+  exact mem_suffixes.2 ⟨s, hs, hwv.trans hvs⟩
+
+end Finset

From 21ebb892f774abbd5b1f5a60ed821a5c0507c741 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 25 Jul 2026 07:45:26 -0700
Subject: [PATCH 5/5] refactor states

---
 .../Classes/P/FinsetDomain/Internal.lean      | 123 +++++++++++++-----
 1 file changed, 88 insertions(+), 35 deletions(-)

diff --git a/Complexitylib/Classes/P/FinsetDomain/Internal.lean b/Complexitylib/Classes/P/FinsetDomain/Internal.lean
index 3fc642e2..b14cd854 100644
--- a/Complexitylib/Classes/P/FinsetDomain/Internal.lean
+++ b/Complexitylib/Classes/P/FinsetDomain/Internal.lean
@@ -75,32 +75,57 @@ instance : Fintype {w : List Bool // w ∈ (outputsFinset g S).suffixes} :=
 
 /-- States of the lookup machine. -/
 inductive LookupState (g : List Bool → List Bool) (S : Finset (List Bool)) : Type where
-  /-- Read phase: the viable prefix consumed so far, `none` being the "dead"
-  state after diverging from every element of `S`.
-
-  TODO: Avoid use of Option, make a separate constructor for the dead state.
-  Also, instead of passing a subtype as arg, pass the value and proof of membership
-  separately, so that the proof can be used in the transition function.
-  -/
-  | read (p : Option {p : List Bool // p ∈ S.prefixes}) : LookupState g S
+  /-- Read phase: the viable prefix consumed so far, carried together with the
+  proof that it is a prefix of some element of `S`, so that the transition
+  function can use the proof directly. -/
+  | read (p : List Bool) (hp : p ∈ S.prefixes) : LookupState g S
+  /-- Read phase, dead state: the input read so far has diverged from every
+  element of `S`. -/
+  | dead : LookupState g S
   /-- Write phase: the output suffix still to be written. -/
-  | write (w : {w : List Bool // w ∈ (outputsFinset g S).suffixes}) : LookupState g S
+  | write (w : List Bool) (hw : w ∈ (outputsFinset g S).suffixes) : LookupState g S
   /-- The halt state. -/
   | halt : LookupState g S
-  deriving DecidableEq, Fintype
+
+/-- `LookupState` as a sum of two finite subtypes and two extra states. This
+equivalence supplies the `DecidableEq` and `Fintype` instances, which cannot be
+derived because the `read`/`write` constructors have dependent fields. -/
+private def lookupStateEquiv :
+    LookupState g S ≃
+      (Option {p : List Bool // p ∈ S.prefixes} ⊕
+        Option {w : List Bool // w ∈ (outputsFinset g S).suffixes}) where
+  toFun
+    | .read p hp => .inl (some ⟨p, hp⟩)
+    | .dead => .inl none
+    | .write w hw => .inr (some ⟨w, hw⟩)
+    | .halt => .inr none
+  invFun
+    | .inl (some ⟨p, hp⟩) => .read p hp
+    | .inl none => .dead
+    | .inr (some ⟨w, hw⟩) => .write w hw
+    | .inr none => .halt
+  left_inv s := by cases s <;> rfl
+  right_inv s := by rcases s with (_ | ⟨p, hp⟩) | (_ | ⟨w, hw⟩) <;> rfl
+
+instance : DecidableEq (LookupState g S) := (lookupStateEquiv g S).decidableEq
+instance : Fintype (LookupState g S) := Fintype.ofEquiv _ (lookupStateEquiv g S).symm
 
 /-- The read-phase state after consuming prefix `p`: the viable prefix `p` if it
 is still a prefix of some element of `S`, otherwise the dead state. -/
 def readState (p : List Bool) : LookupState g S :=
-  .read (if h : p ∈ S.prefixes then some ⟨p, h⟩ else none)
+  if h : p ∈ S.prefixes then .read p h else .dead
 
 /-- The write-phase state carrying output suffix `c`. -/
 def writeState (c : List Bool) (hc : c ∈ (outputsFinset g S).suffixes) : LookupState g S :=
-  .write ⟨c, hc⟩
+  .write c hc
 
 /-- The halt state. -/
 def haltState : LookupState g S := .halt
 
+theorem readState_ne_haltState (p : List Bool) : readState g S p ≠ haltState g S := by
+  rw [readState, haltState]
+  split <;> simp
+
 /-- The lookup machine for `g` and `S`. See the module docstring for the
 construction. It has no work tapes. -/
 def lookupTM : TM 0 where
@@ -109,39 +134,51 @@ def lookupTM : TM 0 where
   qhalt := haltState g S
   δ := fun state iHead wHeads oHead =>
     match state with
-    | .read rd =>
+    | .read p hp =>
       match iHead with
       | Γ.blank =>
         -- end of input: hand off to the write phase
-        ((match rd with
-          | some ⟨p, _⟩ =>
-            writeState g S (if p ∈ S then g p else [])
-              (output_mem_suffixes_outputsFinset g S)
-          | none => writeState g S [] (nil_mem_suffixes_outputsFinset g S)),
+        (writeState g S (if p ∈ S then g p else [])
+           (output_mem_suffixes_outputsFinset g S),
          fun i => readBackWrite (wHeads i), readBackWrite oHead,
          idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
       | Γ.start =>
         -- skip the left-end marker: move input right, keep the state
-        (.read rd,
+        (.read p hp,
          fun i => readBackWrite (wHeads i), readBackWrite oHead,
          Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
       | Γ.zero =>
-        ((match rd with
-          | some ⟨p, _⟩ => readState g S (p ++ [false])
-          | none => .read none),
+        (readState g S (p ++ [false]),
          fun i => readBackWrite (wHeads i), readBackWrite oHead,
          Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
       | Γ.one =>
-        ((match rd with
-          | some ⟨p, _⟩ => readState g S (p ++ [true])
-          | none => .read none),
+        (readState g S (p ++ [true]),
+         fun i => readBackWrite (wHeads i), readBackWrite oHead,
+         Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
+    | .dead =>
+      match iHead with
+      | Γ.blank =>
+        -- end of input: no element of `S` matched, write the empty output
+        (writeState g S [] (nil_mem_suffixes_outputsFinset g S),
+         fun i => readBackWrite (wHeads i), readBackWrite oHead,
+         idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
+      | Γ.start =>
+        (.dead,
          fun i => readBackWrite (wHeads i), readBackWrite oHead,
          Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
-    | .write ⟨[], _⟩ =>
+      | Γ.zero =>
+        (.dead,
+         fun i => readBackWrite (wHeads i), readBackWrite oHead,
+         Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
+      | Γ.one =>
+        (.dead,
+         fun i => readBackWrite (wHeads i), readBackWrite oHead,
+         Dir3.right, fun i => idleDir (wHeads i), idleDir oHead)
+    | .write [] _ =>
       (haltState g S,
        fun i => readBackWrite (wHeads i), readBackWrite oHead,
        idleDir iHead, fun i => idleDir (wHeads i), idleDir oHead)
-    | .write ⟨a :: rest, hw⟩ =>
+    | .write (a :: rest) hw =>
       (writeState g S rest (Finset.mem_suffixes_of_suffix (List.suffix_cons a rest) hw),
        fun i => readBackWrite (wHeads i), Γw.ofBool a,
        idleDir iHead, fun i => idleDir (wHeads i), Dir3.right)
@@ -152,7 +189,20 @@ def lookupTM : TM 0 where
   δ_right_of_start := by
     intro state iHead wHeads oHead
     match state with
-    | .read rd =>
+    | .read p hp =>
+      match iHead with
+      | Γ.blank =>
+        exact ⟨fun h => absurd h (by decide), fun _ => idleDir_right_of_start,
+          idleDir_right_of_start⟩
+      | Γ.start =>
+        exact ⟨fun _ => rfl, fun _ => idleDir_right_of_start, idleDir_right_of_start⟩
+      | Γ.zero =>
+        exact ⟨fun h => absurd h (by decide), fun _ => idleDir_right_of_start,
+          idleDir_right_of_start⟩
+      | Γ.one =>
+        exact ⟨fun h => absurd h (by decide), fun _ => idleDir_right_of_start,
+          idleDir_right_of_start⟩
+    | .dead =>
       match iHead with
       | Γ.blank =>
         exact ⟨fun h => absurd h (by decide), fun _ => idleDir_right_of_start,
@@ -165,10 +215,10 @@ def lookupTM : TM 0 where
       | Γ.one =>
         exact ⟨fun h => absurd h (by decide), fun _ => idleDir_right_of_start,
           idleDir_right_of_start⟩
-    | .write ⟨[], _⟩ =>
+    | .write [] _ =>
       exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start,
         idleDir_right_of_start⟩
-    | .write ⟨a :: rest, hw⟩ =>
+    | .write (a :: rest) hw =>
       exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start, fun _ => rfl⟩
     | .halt =>
       exact ⟨idleDir_right_of_start, fun _ => idleDir_right_of_start,
@@ -190,7 +240,7 @@ private theorem lookup_read_bit_step (p : List Bool) (b : Bool)
         output := c.output.writeAndMove (readBackWrite c.output.read)
           (idleDir c.output.read) } := by
   have hne : c.state ≠ (lookupTM g S).qhalt := by
-    rw [hstate, readState]; simp [lookupTM, haltState]
+    rw [hstate]; exact readState_ne_haltState g S p
   by_cases hp : p ∈ S.prefixes
   · cases b <;>
       simp [TM.step, lookupTM, hstate, hread, readState, haltState, dif_pos hp, Γ.ofBool]
@@ -273,11 +323,14 @@ private theorem lookup_initial_step (x : List Bool) :
       input := (Tape.init (x.map Γ.ofBool)).move Dir3.right
       work := fun _ => (Tape.init []).move Dir3.right
       output := (Tape.init ([] : List Γ)).move Dir3.right } with hc0
-  have hg : ((lookupTM g S).initCfg x).state ≠ (lookupTM g S).qhalt := by
-    simp [lookupTM, readState, haltState]
+  have hg : ((lookupTM g S).initCfg x).state ≠ (lookupTM g S).qhalt :=
+    readState_ne_haltState g S []
   have hstep : (lookupTM g S).step ((lookupTM g S).initCfg x) = some c0 := by
-    simp only [TM.step, if_neg hg]
-    exact congrArg some (Cfg.ext rfl rfl (Subsingleton.elim _ _) rfl)
+    by_cases h : ([] : List Bool) ∈ S.prefixes
+    · simp only [TM.step, hc0, lookupTM, readState, dif_pos h]
+      exact congrArg some (Cfg.ext rfl rfl (Subsingleton.elim _ _) rfl)
+    · simp only [TM.step, hc0, lookupTM, readState, dif_neg h]
+      exact congrArg some (Cfg.ext rfl rfl (Subsingleton.elim _ _) rfl)
   refine ⟨c0, hstep, rfl, ?_, ?_, ?_⟩
   · rw [hc0]; simp [Tape.move_cells]
   · rw [hc0]; simp [Tape.move]