From 9a501f505dd0bc8003d582dd90ffeb9b6e9de8a7 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 26 Jul 2026 17:39:58 -0700
Subject: [PATCH 1/2] some error with this run

---
 Complexitylib.lean                            |   1 +
 Complexitylib/Encoding.lean                   |  18 ++
 Complexitylib/Encoding/Bitstring.lean         | 229 ++++++++++++++++++
 Complexitylib/Encoding/Delimit.lean           | 199 +++++++++++++++
 Complexitylib/Encoding/Pairing.lean           |  82 ++-----
 .../Subroutines/PairEmit/Internal.lean        |   2 +-
 .../TuringMachine/UTM/Internal/Init.lean      |   2 +-
 Complexitylib/SAT/ThreeSAT/Verifier.lean      |   2 +-
 8 files changed, 464 insertions(+), 71 deletions(-)
 create mode 100644 Complexitylib/Encoding.lean
 create mode 100644 Complexitylib/Encoding/Bitstring.lean
 create mode 100644 Complexitylib/Encoding/Delimit.lean

diff --git a/Complexitylib.lean b/Complexitylib.lean
index 7126b70d..8ee51993 100644
--- a/Complexitylib.lean
+++ b/Complexitylib.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 import Complexitylib.Models
+import Complexitylib.Encoding
 import Complexitylib.Asymptotics
 import Complexitylib.TimeConstructible
 import Complexitylib.Classes
diff --git a/Complexitylib/Encoding.lean b/Complexitylib/Encoding.lean
new file mode 100644
index 00000000..1e468b40
--- /dev/null
+++ b/Complexitylib/Encoding.lean
@@ -0,0 +1,18 @@
+/-
+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.Encoding.Delimit
+import Complexitylib.Encoding.Pairing
+import Complexitylib.Encoding.Bitstring
+
+/-!
+# Encodings
+
+Aggregation module for the machine-independent encoding layer: the shared
+self-delimiting block framing and its parsers
+(`Complexitylib.Encoding.Delimit`), the pairing codec used by machine inputs
+(`Complexitylib.Encoding.Pairing`), and the `BitstringEncoding` typeclass with
+instances for common types (`Complexitylib.Encoding.Bitstring`).
+-/
diff --git a/Complexitylib/Encoding/Bitstring.lean b/Complexitylib/Encoding/Bitstring.lean
new file mode 100644
index 00000000..79a8edef
--- /dev/null
+++ b/Complexitylib/Encoding/Bitstring.lean
@@ -0,0 +1,229 @@
+/-
+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.Encoding.Delimit
+import Mathlib.Computability.Encoding
+import Mathlib.Data.PNat.Defs
+import Mathlib.Algebra.Field.Rat
+
+/-!
+# Bitstring Encoding Typeclass
+
+This file provides a typeclass-inferrable version of Mathlib's `Computability.Encoding`,
+specialized to the alphabet `Bool`.
+
+Making it a `class` makes it easier to quickly ask if a function is computable in polynomial
+time, without having to explicitly pass around the encoding.
+
+The idea of this class is to set up instances for common types like `Bool`, `ℕ`, `ℤ`, `ℚ`,
+and instance derivations for product and list types, so that the resulting instance for any
+common type will be polytime-transcodable with any other reasonable binary encoding of that
+type.
+
+Thus, while it may not be obvious without looking carefully which of several essentially
+equivalent encodings of a type is being used, we can at least be sure that for functions
+between types with `BitstringEncoding` instances, questions of polynomial-time computability
+are well-defined, in the sense that the formalization will capture the intended meaning.
+
+Multipartite data is concatenated out of *self-delimiting blocks*, framed by the single
+delimiting operation `Complexity.delimit` from `Complexitylib.Encoding.Delimit` (each payload
+bit doubled, terminated by the separator `[false, true]`) and parsed back by its `unpair?` —
+the same framing underlying the machine-input pairing codec `Complexity.pair`
+(`pair x y = delimit x ++ y`) of `Complexitylib.Encoding.Pairing`.
+
+This layer is deliberately independent of the machine model. The type `Bitstring` below is
+unrelated to the fixed-length `BitString n := Fin n → Bool` used by the circuit layers.
+-/
+
+namespace Complexity
+
+/-- A canonical encoding of a type as bitstrings (`List Bool`).
+
+This is a class version of Mathlib's (bundled) `Computability.Encoding`, specialized to the
+alphabet `Bool`. -/
+class BitstringEncoding (α : Type*) where
+  /-- The encoding function. -/
+  encode : α → List Bool
+  /-- The decoding function; `none` on bitstrings that encode nothing. -/
+  decode : List Bool → Option α
+  /-- Decoding is a left inverse of encoding. -/
+  decode_encode : ∀ x, decode (encode x) = some x
+
+attribute [simp] BitstringEncoding.decode_encode
+
+namespace BitstringEncoding
+
+variable {α β : Type*}
+
+theorem encode_injective [BitstringEncoding α] :
+    Function.Injective (encode : α → List Bool) := fun _ _ h =>
+  Option.some_injective _ (by rw [← decode_encode, ← decode_encode, h])
+
+/-- Transport a `BitstringEncoding` along an injection `f` with partial inverse `g`. -/
+@[reducible]
+def ofLeftInverse [BitstringEncoding β] (f : α → β) (g : β → Option α)
+    (h : ∀ x, g (f x) = some x) : BitstringEncoding α where
+  encode a := encode (f a)
+  decode l := (decode l).bind g
+  decode_encode a := by simp [h]
+
+/- ## Ground instances -/
+
+/-- `ℕ` is encoded by its (little-endian) binary representation, as in
+`Computability.encodeNat`. -/
+instance : BitstringEncoding ℕ where
+  encode := Computability.encodeNat
+  decode l := some (Computability.decodeNat l)
+  decode_encode n := congrArg some (Computability.decode_encodeNat n)
+
+/-- `Bool` is encoded as a singleton bitstring. -/
+instance : BitstringEncoding Bool where
+  encode b := [b]
+  decode l := match l with
+    | [b] => some b
+    | _ => none
+  decode_encode _ := rfl
+
+/-- `Unit` is encoded as the empty bitstring. This is the tensor unit for the pair encoding:
+`encode ((), x) = false :: true :: encode x` and `encode (x, ()) = delimit (encode x)`. -/
+instance : BitstringEncoding Unit where
+  encode _ := []
+  decode l := match l with
+    | [] => some ()
+    | _ => none
+  decode_encode _ := rfl
+
+/-- Decode every block in a list of bitstrings, failing if any block fails to decode.
+
+(This is `List.mapM decode` in the `Option` monad, written out by hand so that it works
+for `α` in any universe.) -/
+def decodeAll [BitstringEncoding α] : List (List Bool) → Option (List α)
+  | [] => some []
+  | b :: t =>
+    match decode b, decodeAll t with
+    | some a, some l => some (a :: l)
+    | _, _ => none
+
+@[simp]
+theorem decodeAll_map_encode [BitstringEncoding α] (l : List α) :
+    decodeAll (l.map encode) = some l := by
+  induction l with
+  | nil => rfl
+  | cons a t ih => simp [decodeAll, ih]
+
+/- ## Derived instances -/
+
+/-- An encoding of `Option α` is obtained encoding `none` as the empty bitstring
+and `some a` as the encoding of `a` prefixed by a `true`. -/
+instance [BitstringEncoding α] : BitstringEncoding (Option α) where
+  encode
+    | none => []
+    | some a => true :: encode a
+  decode input :=
+    match input with
+    | [] => some none
+    | true :: rest => (decode rest).map some
+    | false :: _ => none
+  decode_encode
+    | none => rfl
+    | some a => by simp
+
+/-- Decode a bitstring as a pair: parse one self-delimiting block off the front for the first
+component, and decode the remainder as the second. This is the `decode` of the `α × β` instance,
+given as a standalone definition so that it can be unfolded and reasoned about by name. -/
+def decodePair [BitstringEncoding α] [BitstringEncoding β] (input : List Bool) :
+    Option (α × β) :=
+  match unpair? input with
+  | none => none
+  | some (block, rest) =>
+    match decode block, decode rest with
+    | some a, some b => some (a, b)
+    | _, _ => none
+
+/-- A pair is encoded as a self-delimiting block for the first component followed by the
+encoding of the second — the same layout as the machine-input pairing codec
+`Complexity.pair`. -/
+instance [BitstringEncoding α] [BitstringEncoding β] : BitstringEncoding (α × β) where
+  encode p := delimit (encode p.1) ++ encode p.2
+  decode := decodePair
+  decode_encode p := by simp [decodePair]
+
+theorem decode_prod_eq_decodePair [BitstringEncoding α] [BitstringEncoding β] :
+    (decode : List Bool → Option (α × β)) = decodePair := rfl
+
+/-- A list is encoded as the concatenation of self-delimiting blocks for its elements. -/
+instance [BitstringEncoding α] : BitstringEncoding (List α) where
+  encode l := ((l.map encode).map delimit).flatten
+  decode input :=
+    match undelimitBlocks input with
+    | none => none
+    | some blocks => decodeAll blocks
+  decode_encode l := by
+    rw [undelimitBlocks_flatten_delimit (l.map encode)]
+    exact decodeAll_map_encode l
+
+/-- A subtype inherits the encoding of the ambient type; decoding additionally checks the
+defining predicate. This yields encodings for `ℕ+` and friends for free. -/
+instance {p : α → Prop} [BitstringEncoding α] [DecidablePred p] :
+    BitstringEncoding (Subtype p) where
+  encode x := encode x.val
+  decode input := (decode input).bind fun a => if h : p a then some ⟨a, h⟩ else none
+  decode_encode x := by simp [x.property]
+
+/-- `ℕ+` is encoded as the subtype `{n : ℕ // 0 < n}` it is defined to be. -/
+instance : BitstringEncoding ℕ+ :=
+  inferInstanceAs (BitstringEncoding {n : ℕ // 0 < n})
+
+/-- `ℤ` is encoded via the pair `(n.toNat, (-n).toNat)` (one component is always `0`). -/
+instance : BitstringEncoding ℤ :=
+  ofLeftInverse (fun n : ℤ => (n.toNat, (-n).toNat))
+    (fun p => some ((p.1 : ℤ) - (p.2 : ℤ))) (fun n => congrArg some (by dsimp only; omega))
+
+/-- `ℚ` is encoded as its (reduced) numerator-denominator pair. -/
+instance : BitstringEncoding ℚ :=
+  ofLeftInverse (fun q : ℚ => (q.num, q.den))
+    (fun p => some ((p.1 : ℚ) / (p.2 : ℚ))) (fun q => by simp [Rat.num_div_den])
+
+end BitstringEncoding
+
+/-- A bitstring: definitionally `List Bool`, but kept as a distinct (semireducible) type-level
+name so that it can carry the identity `BitstringEncoding` without overlapping the generic
+`List α` instance.
+
+Data that is conceptually a raw bitstring should be typed as `Bitstring`, and is encoded as
+itself; a `List Bool` that is conceptually a list which happens to contain booleans keeps the
+generic self-delimiting list encoding (four bits per element). Because `Bitstring` is not
+reducible, instance search never sees through it, so the two encodings cannot be confused: a
+lemma about the generic `List α` encoding instantiated at `α := Bool` and a lemma about
+`Bitstring` can never silently disagree about which encoding is meant.
+
+(Not to be confused with the fixed-length `BitString n := Fin n → Bool` of the circuit
+layers.) -/
+def Bitstring : Type := List Bool
+
+/-- A bitstring is encoded as itself. -/
+instance : BitstringEncoding Bitstring where
+  encode := id
+  decode := some
+  decode_encode _ := rfl
+
+/-- Convert a `List Bool` to a `Bitstring`. Definitionally the identity; useful for stating
+lemmas that mix the two types without relying on definitional unfolding. -/
+def Bitstring.ofList (l : List Bool) : Bitstring := l
+
+/-- Convert a `Bitstring` to a `List Bool`. Definitionally the identity. -/
+def Bitstring.toList (l : Bitstring) : List Bool := l
+
+namespace BitstringEncoding
+
+@[simp]
+theorem encode_ofList (l : List Bool) : encode (Bitstring.ofList l) = l := rfl
+
+theorem decode_bitstring (l : List Bool) :
+    (decode l : Option Bitstring) = some (Bitstring.ofList l) := rfl
+
+end BitstringEncoding
+
+end Complexity
diff --git a/Complexitylib/Encoding/Delimit.lean b/Complexitylib/Encoding/Delimit.lean
new file mode 100644
index 00000000..7290535f
--- /dev/null
+++ b/Complexitylib/Encoding/Delimit.lean
@@ -0,0 +1,199 @@
+/-
+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.List.Basic
+import Mathlib.Data.Nat.Init
+import Lean.Elab.Tactic.Omega
+
+/-!
+# Self-delimiting blocks
+
+To concatenate binary strings into a single binary string, each piece must announce its own
+end. This file defines the library's single framing operation and its parsers:
+
+- `delimit` frames a payload: each payload bit is doubled (`false ↦ [false, false]`,
+  `true ↦ [true, true]`) and the block is terminated by the separator `[false, true]`,
+  which no run of doubled bits can produce.
+- `unpair?` parses one block off the front of the input, returning the payload and the
+  remaining suffix (`none` on malformed input). It is named for its role in the pairing
+  codec `Complexity.pair` (see `Complexitylib.Encoding.Pairing`), which is
+  `pair x y = delimit x ++ y`.
+- `undelimitBlock`, `takeFirstBlock`, `hasBlock`, `tagBlock`, and `undelimitBlocks` are the
+  total helper functions machines compute when working with framed data.
+
+This file deliberately has no dependency on the machine or complexity-class layers, so both
+the machine-input pairing codec (`Complexitylib.Encoding.Pairing`) and the encoding layer
+(`Complexitylib.Encoding.Bitstring`) can build on it without import cycles.
+-/
+
+namespace Complexity
+
+/-- Frame a binary string as a self-delimiting block: each payload bit is doubled
+    (`false ↦ [false, false]`, `true ↦ [true, true]`) and the block is terminated by the
+    separator `[false, true]`, which no run of doubled bits can produce. -/
+def delimit (x : List Bool) : List Bool :=
+  (x.flatMap fun b => [b, b]) ++ [false, true]
+
+@[simp] theorem delimit_nil : delimit [] = [false, true] := rfl
+
+@[simp] theorem delimit_cons (b : Bool) (l : List Bool) :
+    delimit (b :: l) = b :: b :: delimit l := by
+  simp [delimit]
+
+@[simp] theorem delimit_length (l : List Bool) : (delimit l).length = 2 * l.length + 2 := by
+  induction l with
+  | nil => rfl
+  | cons b l ih => simp only [delimit_cons, List.length_cons, ih]; omega
+
+/-- Parse one self-delimiting block off the front of the input. It scans doubled bits until
+    the first separator `[false, true]`, returning the decoded payload together with the
+    remaining suffix. Invalid doubled prefixes return `none`. -/
+def unpair? : List Bool → Option (List Bool × List Bool)
+  | [] => none
+  | false :: true :: y => some ([], y)
+  | false :: false :: z =>
+      Option.map (fun (xy : List Bool × List Bool) => (false :: xy.1, xy.2)) (unpair? z)
+  | true :: true :: z =>
+      Option.map (fun (xy : List Bool × List Bool) => (true :: xy.1, xy.2)) (unpair? z)
+  | _ => none
+
+/-- `unpair?` reads back the framing written by `delimit`: parsing one block off the front
+    of any input recovers the payload and the remaining suffix. -/
+@[simp] theorem unpair?_delimit_append (x y : List Bool) :
+    unpair? (delimit x ++ y) = some (x, y) := by
+  induction x with
+  | nil => simp [unpair?]
+  | cons b x ih => cases b <;> simp [unpair?, ih]
+
+/-- Soundness of the parser: a successful parse decomposes the input as the parsed payload's
+    framing followed by the leftover suffix. -/
+theorem eq_delimit_append_of_unpair?_eq_some :
+    ∀ {z x y : List Bool}, unpair? z = some (x, y) → z = delimit x ++ y
+  | [], _, _, h => by simp [unpair?] at h
+  | [b], _, _, h => by cases b <;> simp [unpair?] at h
+  | false :: true :: rest, x, y, h => by
+    simp only [unpair?, Option.some.injEq, Prod.mk.injEq] at h
+    obtain ⟨rfl, rfl⟩ := h
+    rfl
+  | false :: false :: rest, x, y, h => by
+    simp only [unpair?, Option.map_eq_some_iff] at h
+    obtain ⟨⟨p₁, p₂⟩, hp, heq⟩ := h
+    obtain ⟨rfl, rfl⟩ : false :: p₁ = x ∧ p₂ = y := by simpa [Prod.ext_iff] using heq
+    simp only [eq_delimit_append_of_unpair?_eq_some hp, delimit_cons, List.cons_append]
+  | true :: true :: rest, x, y, h => by
+    simp only [unpair?, Option.map_eq_some_iff] at h
+    obtain ⟨⟨p₁, p₂⟩, hp, heq⟩ := h
+    obtain ⟨rfl, rfl⟩ : true :: p₁ = x ∧ p₂ = y := by simpa [Prod.ext_iff] using heq
+    simp only [eq_delimit_append_of_unpair?_eq_some hp, delimit_cons, List.cons_append]
+  | true :: false :: rest, _, _, h => by simp [unpair?] at h
+
+/- ## Total block helpers -/
+
+/-- Strip the framing of a single self-delimiting block, returning its payload. On `delimit P`
+this returns `P`. Unlike `unpair?`, this is total: it ignores any data trailing the first block
+and maps malformed input to `[]`. -/
+def undelimitBlock : List Bool → List Bool
+  | false :: true :: _ => []
+  | false :: false :: rest => false :: undelimitBlock rest
+  | true :: _ :: rest => true :: undelimitBlock rest
+  | _ => []
+
+@[simp]
+theorem undelimitBlock_delimit (P : List Bool) :
+    undelimitBlock (delimit P) = P := by
+  induction P with
+  | nil => rfl
+  | cons b P ih => cases b <;> simp [undelimitBlock, ih]
+
+/-- Keep the leading self-delimiting block of a bitstring, dropping everything after it. On a
+pair encoding `delimit x ++ w` this returns `delimit x`. -/
+def takeFirstBlock : List Bool → List Bool
+  | false :: true :: _ => [false, true]
+  | false :: false :: rest => false :: false :: takeFirstBlock rest
+  | true :: c :: rest => true :: c :: takeFirstBlock rest
+  | l => l
+
+@[simp]
+theorem takeFirstBlock_delimit_append (P Q : List Bool) :
+    takeFirstBlock (delimit P ++ Q) = delimit P := by
+  induction P with
+  | nil => rfl
+  | cons b P ih => cases b <;> simp [takeFirstBlock, ih]
+
+/-- Does the bitstring begin with a well-formed self-delimiting block? -/
+def hasBlock : List Bool → Bool
+  | false :: true :: _ => true
+  | false :: false :: rest => hasBlock rest
+  | true :: true :: rest => hasBlock rest
+  | _ => false
+
+theorem hasBlock_eq_isSome_unpair? :
+    ∀ l : List Bool, hasBlock l = (unpair? l).isSome
+  | [] => rfl
+  | [b] => by cases b <;> rfl
+  | false :: true :: _ => rfl
+  | false :: false :: rest => by
+    simp only [hasBlock, unpair?, hasBlock_eq_isSome_unpair? rest]
+    cases unpair? rest <;> rfl
+  | true :: true :: rest => by
+    simp only [hasBlock, unpair?, hasBlock_eq_isSome_unpair? rest]
+    cases unpair? rest <;> rfl
+  | true :: false :: _ => rfl
+
+/-- Tag a bitstring with a leading `true` if it begins with a well-formed self-delimiting
+block, and return the empty bitstring otherwise. On pair encodings this computes
+`encode ∘ decode`. -/
+def tagBlock (l : List Bool) : List Bool :=
+  bif hasBlock l then true :: l else []
+
+/- ## Parsing a sequence of blocks -/
+
+/-- Parse a sequence of self-delimiting blocks, using `fuel` to bound the number of blocks.
+
+This is the auxiliary, fuel-carrying implementation of `undelimitBlocks`; since every block
+is nonempty, `input.length` is always enough fuel. -/
+def undelimitBlocksAux : ℕ → List Bool → Option (List (List Bool))
+  | _, [] => some []
+  | 0, _ :: _ => none
+  | fuel + 1, input => do
+    let (block, rest) ← unpair? input
+    let blocks ← undelimitBlocksAux fuel rest
+    return block :: blocks
+
+/-- Parse a sequence of self-delimiting blocks off the front of the input.
+
+Since every block is nonempty, `input.length` bounds the number of blocks, so it always
+suffices as fuel for `undelimitBlocksAux`. -/
+def undelimitBlocks (input : List Bool) : Option (List (List Bool)) :=
+  undelimitBlocksAux input.length input
+
+theorem length_le_length_flatten_delimit (l : List (List Bool)) :
+    l.length ≤ ((l.map delimit).flatten).length := by
+  induction l with
+  | nil => simp
+  | cons b t ih =>
+    simp only [List.map_cons, List.flatten_cons, List.length_append, List.length_cons,
+      delimit_length]
+    omega
+
+private theorem undelimitBlocksAux_flatten_delimit (l : List (List Bool)) :
+    ∀ fuel, l.length ≤ fuel → undelimitBlocksAux fuel ((l.map delimit).flatten) = some l := by
+  induction l with
+  | nil => intro fuel _; cases fuel <;> rfl
+  | cons b t ih =>
+    intro fuel hfuel
+    rw [List.length_cons] at hfuel
+    obtain ⟨fuel, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    obtain ⟨hd, tl, hcons⟩ : ∃ hd tl, delimit b ++ (t.map delimit).flatten = hd :: tl := by
+      cases b <;> exact ⟨_, _, rfl⟩
+    simp only [List.map_cons, List.flatten_cons, hcons, undelimitBlocksAux]
+    rw [← hcons, unpair?_delimit_append]
+    simp [ih fuel (by omega)]
+
+theorem undelimitBlocks_flatten_delimit (l : List (List Bool)) :
+    undelimitBlocks ((l.map delimit).flatten) = some l :=
+  undelimitBlocksAux_flatten_delimit l _ (length_le_length_flatten_delimit l)
+
+end Complexity
diff --git a/Complexitylib/Encoding/Pairing.lean b/Complexitylib/Encoding/Pairing.lean
index 68070786..0625e5cd 100644
--- a/Complexitylib/Encoding/Pairing.lean
+++ b/Complexitylib/Encoding/Pairing.lean
@@ -3,39 +3,26 @@ Copyright (c) 2025 Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
-import Mathlib.Data.List.Basic
-import Mathlib.Data.Nat.Init
-import Lean.Elab.Tactic.Omega
+import Complexitylib.Encoding.Delimit
 
 /-!
 # Pairing binary strings
 
 This file defines the low-level self-delimiting pairing codec used by machine
-inputs throughout Complexitylib. It deliberately has no dependency on the
-machine or complexity-class layers, so parsers and encoders can reuse it
-without introducing an import cycle.
+inputs throughout Complexitylib: `pair x y = delimit x ++ y`, framed by the
+shared delimiting operation of `Complexitylib.Encoding.Delimit` and parsed
+back by its `unpair?`. It deliberately has no dependency on the machine or
+complexity-class layers, so parsers and encoders can reuse it without
+introducing an import cycle.
 -/
 
 namespace Complexity
 
-/-- Encode a pair of binary strings as a single binary string.
-    Each bit of `x` is doubled (`false ↦ [false, false]`, `true ↦ [true, true]`),
-    followed by the separator `[false, true]`, followed by `y` verbatim.
+/-- Encode a pair of binary strings as a single binary string: the self-delimiting block
+    `delimit x` followed by `y` verbatim. `unpair?` is the partial inverse.
     This encoding is injective and computable in linear time. -/
 def pair (x y : List Bool) : List Bool :=
-  (x.flatMap fun b => [b, b]) ++ [false, true] ++ y
-
-/-- Partial inverse to `pair`. It scans doubled bits until the first
-    separator `[false, true]`, returning the decoded left component together
-    with the remaining suffix. Invalid doubled prefixes return `none`. -/
-def unpair? : List Bool → Option (List Bool × List Bool)
-  | [] => none
-  | false :: true :: y => some ([], y)
-  | false :: false :: z =>
-      Option.map (fun (xy : List Bool × List Bool) => (false :: xy.1, xy.2)) (unpair? z)
-  | true :: true :: z =>
-      Option.map (fun (xy : List Bool × List Bool) => (true :: xy.1, xy.2)) (unpair? z)
-  | _ => none
+  delimit x ++ y
 
 private theorem pair_nil_eq (y : List Bool) :
     pair [] y = false :: true :: y := by
@@ -45,7 +32,7 @@ private theorem pair_nil_eq (y : List Bool) :
     doubled bit `b, b`. -/
 theorem pair_cons_eq (b : Bool) (x y : List Bool) :
     pair (b :: x) y = b :: b :: pair x y := by
-  simp [pair, List.append_assoc]
+  simp [pair]
 
 /-- `|pair x y| = 2·|x| + 2 + |y|`. The `2·|x|` comes from doubling every
     bit of `x`; the `+2` is the separator `[false, true]`. -/
@@ -92,55 +79,14 @@ theorem pair_inj {x₁ x₂ : List Bool} {y₁ y₂ : List Bool}
 /-- `unpair?` is a left inverse of `pair`: decoding an encoded pair
     recovers exactly its two components. -/
 @[simp] theorem unpair?_pair (x y : List Bool) :
-    unpair? (pair x y) = some (x, y) := by
-  induction x with
-  | nil =>
-    simp [unpair?, pair_nil_eq]
-  | cons b xs ih =>
-    rw [pair_cons_eq]
-    cases b <;> simp [unpair?, ih]
+    unpair? (pair x y) = some (x, y) :=
+  unpair?_delimit_append x y
 
 /-- Soundness of the decoder: if `unpair?` succeeds on `z`, producing `(x, y)`,
     then `z` was exactly the encoding `pair x y`. -/
 theorem eq_pair_of_unpair?_eq_some {z x y : List Bool} (h : unpair? z = some (x, y)) :
-    z = pair x y := by
-  have hsound :
-      ∀ z x y, unpair? z = some (x, y) → z = pair x y := by
-    intro z x y h
-    induction hlen : z.length using Nat.strong_induction_on generalizing z x y with
-    | h n ih =>
-        cases z with
-        | nil =>
-            simp [unpair?] at h
-        | cons a z1 =>
-            cases z1 with
-            | nil =>
-                cases a <;> simp [unpair?] at h
-            | cons b z2 =>
-                cases a
-                · cases b
-                  · simp [unpair?] at h
-                    rcases h with ⟨x', htail, rfl⟩
-                    have hz2lt : z2.length < n := by
-                      rw [← hlen]
-                      have : z2.length < z2.length + 1 + 1 := by omega
-                      exact this
-                    have hz2 : z2 = pair x' y := ih z2.length hz2lt z2 x' y htail rfl
-                    simpa [pair_cons_eq] using congrArg (fun t => false :: false :: t) hz2
-                  · simp [unpair?] at h
-                    rcases h with ⟨rfl, rfl⟩
-                    simp [pair_nil_eq]
-                · cases b
-                  · simp [unpair?] at h
-                  · simp [unpair?] at h
-                    rcases h with ⟨x', htail, rfl⟩
-                    have hz2lt : z2.length < n := by
-                      rw [← hlen]
-                      have : z2.length < z2.length + 1 + 1 := by omega
-                      exact this
-                    have hz2 : z2 = pair x' y := ih z2.length hz2lt z2 x' y htail rfl
-                    simpa [pair_cons_eq] using congrArg (fun t => true :: true :: t) hz2
-  exact hsound z x y h
+    z = pair x y :=
+  eq_delimit_append_of_unpair?_eq_some h
 
 /-- `unpair? z` returns `some (x, y)` if and only if `z = pair x y`,
     characterizing exactly which strings are valid pair encodings. -/
diff --git a/Complexitylib/Models/TuringMachine/Subroutines/PairEmit/Internal.lean b/Complexitylib/Models/TuringMachine/Subroutines/PairEmit/Internal.lean
index a24dc7e3..8a2413cc 100644
--- a/Complexitylib/Models/TuringMachine/Subroutines/PairEmit/Internal.lean
+++ b/Complexitylib/Models/TuringMachine/Subroutines/PairEmit/Internal.lean
@@ -315,7 +315,7 @@ theorem pairInputWorkTM_reachesIn_internal {n : ℕ}
   · intro i hi
     rw [hwork₂]
     exact hother₁ i hi
-  · simpa [pair, doubled, List.append_assoc] using houtput₂
+  · simpa [pair, delimit, doubled, List.append_assoc] using houtput₂
 
 /-- Internal compact Hoare contract for pair emission. -/
 theorem pairInputWorkTM_hoareTime_internal {n : ℕ}
diff --git a/Complexitylib/Models/TuringMachine/UTM/Internal/Init.lean b/Complexitylib/Models/TuringMachine/UTM/Internal/Init.lean
index fc48baad..0531c637 100644
--- a/Complexitylib/Models/TuringMachine/UTM/Internal/Init.lean
+++ b/Complexitylib/Models/TuringMachine/UTM/Internal/Init.lean
@@ -1270,7 +1270,7 @@ private theorem initTM_hoareTime_core (α x : List Bool) {c₁ : Cfg 6 initTM.Q}
       (c'.work 5).HoldsExact [] ∧ (c'.work 5).head = 1 ∧
       c'.output.cells = (Tape.init []).cells ∧ c'.output.head = 1 := by
   have hP : pair α x = (α.flatMap fun b => [b, b]) ++ false :: true :: x := by
-    simp [pair]
+    simp [pair, delimit]
   have hwf := Tape.StartInvariant.init_ofBool (pair α x)
   have hblank1 : (Tape.init []).cells 1 = Γ.blank := Tape.init_nil_cells_succ 0
   have hwo₁ : ∀ i, (c₁.work i).read ≠ Γ.start ∧ 1 ≤ (c₁.work i).head := by
diff --git a/Complexitylib/SAT/ThreeSAT/Verifier.lean b/Complexitylib/SAT/ThreeSAT/Verifier.lean
index 6f85ed7a..76f4893d 100644
--- a/Complexitylib/SAT/ThreeSAT/Verifier.lean
+++ b/Complexitylib/SAT/ThreeSAT/Verifier.lean
@@ -94,7 +94,7 @@ left component belongs to the exact-3 syntax language. -/
     pair z witness ∈ language ↔ z ∈ Syntax.language := by
   change accept ((pair z witness).foldl step initial) = true ↔
     Syntax.accept (z.foldl Syntax.bitStep Syntax.bitStart) = true
-  rw [pair, List.foldl_append, List.foldl_append]
+  rw [pair, delimit, List.foldl_append, List.foldl_append]
   simp only [initial]
   rw [foldl_doubled]
   cases hsyntax : Syntax.accept (z.foldl Syntax.bitStep Syntax.bitStart) <;>

From 7733c9d2b7a9059f58b61f8272bf26e539cdc42d Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 1 Aug 2026 09:31:14 -0700
Subject: [PATCH 2/2] list bool encoding for data

---
 Complexitylib/Encoding.lean                   |   8 +-
 Complexitylib/Encoding/Bitstring.lean         | 234 ------------------
 Complexitylib/Encoding/Data.lean              | 232 +++++++++++++++++
 .../DataEncode.lean                           |  29 ++-
 Complexitylib/Encoding/Delimit.lean           |   6 +-
 Complexitylib/Models.lean                     |   2 -
 .../Models/RoseTreeMachine/Data.lean          | 128 ----------
 .../Models/RoseTreeMachine/Prog.lean          |   5 +-
 8 files changed, 266 insertions(+), 378 deletions(-)
 delete mode 100644 Complexitylib/Encoding/Bitstring.lean
 create mode 100644 Complexitylib/Encoding/Data.lean
 rename Complexitylib/{Models/RoseTreeMachine => Encoding}/DataEncode.lean (69%)
 delete mode 100644 Complexitylib/Models/RoseTreeMachine/Data.lean

diff --git a/Complexitylib/Encoding.lean b/Complexitylib/Encoding.lean
index 89101f59..20e12024 100644
--- a/Complexitylib/Encoding.lean
+++ b/Complexitylib/Encoding.lean
@@ -7,7 +7,8 @@ Authors: Bolton Bailey
 module
 public import Complexitylib.Encoding.Delimit
 public import Complexitylib.Encoding.Pairing
-public import Complexitylib.Encoding.Bitstring
+public import Complexitylib.Encoding.Data
+public import Complexitylib.Encoding.DataEncode
 
 /-!
 # Encodings
@@ -15,6 +16,7 @@ public import Complexitylib.Encoding.Bitstring
 Aggregation module for the machine-independent encoding layer: the shared
 self-delimiting block framing and its parsers
 (`Complexitylib.Encoding.Delimit`), the pairing codec used by machine inputs
-(`Complexitylib.Encoding.Pairing`), and the `BitstringEncoding` typeclass with
-instances for common types (`Complexitylib.Encoding.Bitstring`).
+(`Complexitylib.Encoding.Pairing`), and the rose-tree `Data` type
+(`Complexitylib.Encoding.Data`) together with the `DataEncode` typeclass and its
+derived bitstring encoding (`Complexitylib.Encoding.DataEncode`).
 -/
diff --git a/Complexitylib/Encoding/Bitstring.lean b/Complexitylib/Encoding/Bitstring.lean
deleted file mode 100644
index 2fe88cfe..00000000
--- a/Complexitylib/Encoding/Bitstring.lean
+++ /dev/null
@@ -1,234 +0,0 @@
-/-
-Copyright (c) 2026 Bolton Bailey. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Bolton Bailey
--/
-
-module
-public import Complexitylib.Encoding.Delimit
-public import Mathlib.Computability.Encoding
-public import Mathlib.Data.PNat.Defs
-public import Mathlib.Algebra.Field.Rat
-
-/-!
-# Bitstring Encoding Typeclass
-
-This file provides a typeclass-inferrable version of Mathlib's `Computability.Encoding`,
-specialized to the alphabet `Bool`.
-
-Making it a `class` makes it easier to quickly ask if a function is computable in polynomial
-time, without having to explicitly pass around the encoding.
-
-The idea of this class is to set up instances for common types like `Bool`, `ℕ`, `ℤ`, `ℚ`,
-and instance derivations for product and list types, so that the resulting instance for any
-common type will be polytime-transcodable with any other reasonable binary encoding of that
-type.
-
-Thus, while it may not be obvious without looking carefully which of several essentially
-equivalent encodings of a type is being used, we can at least be sure that for functions
-between types with `BitstringEncoding` instances, questions of polynomial-time computability
-are well-defined, in the sense that the formalization will capture the intended meaning.
-
-Multipartite data is concatenated out of *self-delimiting blocks*, framed by the single
-delimiting operation `Complexity.delimit` from `Complexitylib.Encoding.Delimit` (each payload
-bit doubled, terminated by the separator `[false, true]`) and parsed back by its `unpair?` —
-the same framing underlying the machine-input pairing codec `Complexity.pair`
-(`pair x y = delimit x ++ y`) of `Complexitylib.Encoding.Pairing`.
-
-This layer is deliberately independent of the machine model. The type `Bitstring` below is
-unrelated to the fixed-length `BitString n := Fin n → Bool` used by the circuit layers.
--/
-
-
-@[expose] public section
-
-namespace Complexity
-
-/-- A canonical encoding of a type as bitstrings (`List Bool`).
-
-This is a class version of Mathlib's (bundled) `Computability.Encoding`, specialized to the
-alphabet `Bool`. -/
-class BitstringEncoding (α : Type*) where
-  /-- The encoding function. -/
-  encode : α → List Bool
-  /-- The decoding function; `none` on bitstrings that encode nothing. -/
-  decode : List Bool → Option α
-  /-- Decoding is a left inverse of encoding. -/
-  decode_encode : ∀ x, decode (encode x) = some x
-
-attribute [simp] BitstringEncoding.decode_encode
-
-namespace BitstringEncoding
-
-variable {α β : Type*}
-
-theorem encode_injective [BitstringEncoding α] :
-    Function.Injective (encode : α → List Bool) := fun _ _ h =>
-  Option.some_injective _ (by rw [← decode_encode, ← decode_encode, h])
-
-/-- Transport a `BitstringEncoding` along an injection `f` with partial inverse `g`. -/
-@[reducible]
-def ofLeftInverse [BitstringEncoding β] (f : α → β) (g : β → Option α)
-    (h : ∀ x, g (f x) = some x) : BitstringEncoding α where
-  encode a := encode (f a)
-  decode l := (decode l).bind g
-  decode_encode a := by simp [h]
-
-/- ## Ground instances -/
-
-/-- `ℕ` is encoded by its (little-endian) binary representation, as in
-`Computability.encodeNat`. -/
-instance : BitstringEncoding ℕ where
-  encode := Computability.encodeNat
-  decode l := some (Computability.decodeNat l)
-  decode_encode n := congrArg some (Computability.decode_encodeNat n)
-
-/-- `Bool` is encoded as a singleton bitstring. -/
-instance : BitstringEncoding Bool where
-  encode b := [b]
-  decode l := match l with
-    | [b] => some b
-    | _ => none
-  decode_encode _ := rfl
-
-/-- `Unit` is encoded as the empty bitstring. This is the tensor unit for the pair encoding:
-`encode ((), x) = false :: true :: encode x` and `encode (x, ()) = delimit (encode x)`. -/
-instance : BitstringEncoding Unit where
-  encode _ := []
-  decode l := match l with
-    | [] => some ()
-    | _ => none
-  decode_encode _ := rfl
-
-/-- Decode every block in a list of bitstrings, failing if any block fails to decode.
-
-(This is `List.mapM decode` in the `Option` monad, written out by hand so that it works
-for `α` in any universe.) -/
-def decodeAll [BitstringEncoding α] : List (List Bool) → Option (List α)
-  | [] => some []
-  | b :: t =>
-    match decode b, decodeAll t with
-    | some a, some l => some (a :: l)
-    | _, _ => none
-
-@[simp]
-theorem decodeAll_map_encode [BitstringEncoding α] (l : List α) :
-    decodeAll (l.map encode) = some l := by
-  induction l with
-  | nil => rfl
-  | cons a t ih => simp [decodeAll, ih]
-
-/- ## Derived instances -/
-
-/-- An encoding of `Option α` is obtained encoding `none` as the empty bitstring
-and `some a` as the encoding of `a` prefixed by a `true`. -/
-instance [BitstringEncoding α] : BitstringEncoding (Option α) where
-  encode
-    | none => []
-    | some a => true :: encode a
-  decode input :=
-    match input with
-    | [] => some none
-    | true :: rest => (decode rest).map some
-    | false :: _ => none
-  decode_encode
-    | none => rfl
-    | some a => by simp
-
-/-- Decode a bitstring as a pair: parse one self-delimiting block off the front for the first
-component, and decode the remainder as the second. This is the `decode` of the `α × β` instance,
-given as a standalone definition so that it can be unfolded and reasoned about by name. -/
-def decodePair [BitstringEncoding α] [BitstringEncoding β] (input : List Bool) :
-    Option (α × β) :=
-  match unpair? input with
-  | none => none
-  | some (block, rest) =>
-    match decode block, decode rest with
-    | some a, some b => some (a, b)
-    | _, _ => none
-
-/-- A pair is encoded as a self-delimiting block for the first component followed by the
-encoding of the second — the same layout as the machine-input pairing codec
-`Complexity.pair`. -/
-instance [BitstringEncoding α] [BitstringEncoding β] : BitstringEncoding (α × β) where
-  encode p := delimit (encode p.1) ++ encode p.2
-  decode := decodePair
-  decode_encode p := by simp [decodePair]
-
-theorem decode_prod_eq_decodePair [BitstringEncoding α] [BitstringEncoding β] :
-    (decode : List Bool → Option (α × β)) = decodePair := rfl
-
-/-- A list is encoded as the concatenation of self-delimiting blocks for its elements. -/
-instance [BitstringEncoding α] : BitstringEncoding (List α) where
-  encode l := ((l.map encode).map delimit).flatten
-  decode input :=
-    match undelimitBlocks input with
-    | none => none
-    | some blocks => decodeAll blocks
-  decode_encode l := by
-    rw [undelimitBlocks_flatten_delimit (l.map encode)]
-    exact decodeAll_map_encode l
-
-/-- A subtype inherits the encoding of the ambient type; decoding additionally checks the
-defining predicate. This yields encodings for `ℕ+` and friends for free. -/
-instance {p : α → Prop} [BitstringEncoding α] [DecidablePred p] :
-    BitstringEncoding (Subtype p) where
-  encode x := encode x.val
-  decode input := (decode input).bind fun a => if h : p a then some ⟨a, h⟩ else none
-  decode_encode x := by simp [x.property]
-
-/-- `ℕ+` is encoded as the subtype `{n : ℕ // 0 < n}` it is defined to be. -/
-instance : BitstringEncoding ℕ+ :=
-  inferInstanceAs (BitstringEncoding {n : ℕ // 0 < n})
-
-/-- `ℤ` is encoded via the pair `(n.toNat, (-n).toNat)` (one component is always `0`). -/
-instance : BitstringEncoding ℤ :=
-  ofLeftInverse (fun n : ℤ => (n.toNat, (-n).toNat))
-    (fun p => some ((p.1 : ℤ) - (p.2 : ℤ))) (fun n => congrArg some (by dsimp only; omega))
-
-/-- `ℚ` is encoded as its (reduced) numerator-denominator pair. -/
-instance : BitstringEncoding ℚ :=
-  ofLeftInverse (fun q : ℚ => (q.num, q.den))
-    (fun p => some ((p.1 : ℚ) / (p.2 : ℚ))) (fun q => by simp [Rat.num_div_den])
-
-end BitstringEncoding
-
-/-- A bitstring: definitionally `List Bool`, but kept as a distinct (semireducible) type-level
-name so that it can carry the identity `BitstringEncoding` without overlapping the generic
-`List α` instance.
-
-Data that is conceptually a raw bitstring should be typed as `Bitstring`, and is encoded as
-itself; a `List Bool` that is conceptually a list which happens to contain booleans keeps the
-generic self-delimiting list encoding (four bits per element). Because `Bitstring` is not
-reducible, instance search never sees through it, so the two encodings cannot be confused: a
-lemma about the generic `List α` encoding instantiated at `α := Bool` and a lemma about
-`Bitstring` can never silently disagree about which encoding is meant.
-
-(Not to be confused with the fixed-length `BitString n := Fin n → Bool` of the circuit
-layers.) -/
-def Bitstring : Type := List Bool
-
-/-- A bitstring is encoded as itself. -/
-instance : BitstringEncoding Bitstring where
-  encode := id
-  decode := some
-  decode_encode _ := rfl
-
-/-- Convert a `List Bool` to a `Bitstring`. Definitionally the identity; useful for stating
-lemmas that mix the two types without relying on definitional unfolding. -/
-def Bitstring.ofList (l : List Bool) : Bitstring := l
-
-/-- Convert a `Bitstring` to a `List Bool`. Definitionally the identity. -/
-def Bitstring.toList (l : Bitstring) : List Bool := l
-
-namespace BitstringEncoding
-
-@[simp]
-theorem encode_ofList (l : List Bool) : encode (Bitstring.ofList l) = l := rfl
-
-theorem decode_bitstring (l : List Bool) :
-    (decode l : Option Bitstring) = some (Bitstring.ofList l) := rfl
-
-end BitstringEncoding
-
-end Complexity
diff --git a/Complexitylib/Encoding/Data.lean b/Complexitylib/Encoding/Data.lean
new file mode 100644
index 00000000..65c0f604
--- /dev/null
+++ b/Complexitylib/Encoding/Data.lean
@@ -0,0 +1,232 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+public import Aesop.BuiltinRules
+public import Mathlib.Data.Nat.Notation
+public import Mathlib.Data.List.Basic
+public import Mathlib.Tactic.Finiteness.Attr
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.ToAdditive
+public import Mathlib.Tactic.ToDual
+
+/-!
+# The rose-tree `Data` type
+
+This file contains the rose-tree data structure `Data`, a general-purpose container into which
+most of Lean's data structures can be encoded (see `Complexitylib.Encoding.DataEncode`). It is
+the internal data structure operated on by the rose tree machine (RTM), but it lives in the
+machine-independent encoding layer because it is also used as a target for encodings.
+
+## Main definitions and notations
+
+- `Data` - the main data structure
+- `Data.size` - the size of a `Data` object when encoded using parentheses; complexity results
+  use this size as the main measure.
+- `Data.toBits` - a parenthesized (balanced-bracket) serialization into `List Bool`, with length
+  equal to `Data.size`, and injective (`Data.toBits_injective`).
+- `Data.recL` - the main recursion principle for `Data`
+- `Data.inductionL` - the main induction principle for `Data`
+
+-/
+
+
+@[expose] public section
+
+namespace Complexity
+
+/-- Rose-tree data structure, it allows us to encode most of Lean's data structures in a
+"natural" manner -/
+inductive Data where
+  | l : List Data → Data
+deriving Repr
+
+mutual
+  /-- Decidable equality for `Data`, defined jointly with `Data.listDecEq`. -/
+  def Data.decEq : ∀ (a b : Data), Decidable (a = b)
+    | .l xs, .l ys =>
+      match Data.listDecEq xs ys with
+      | isTrue h => isTrue (congrArg Data.l h)
+      | isFalse h => isFalse fun heq => h (Data.l.inj heq)
+  /-- Decidable equality for `List Data`, defined jointly with `Data.decEq`. -/
+  def Data.listDecEq : ∀ (xs ys : List Data), Decidable (xs = ys)
+    | [], [] => isTrue rfl
+    | [], _ :: _ => isFalse (by simp)
+    | _ :: _, [] => isFalse (by simp)
+    | x :: xs, y :: ys =>
+      match Data.decEq x y, Data.listDecEq xs ys with
+      | isTrue hxy, isTrue hxys => isTrue (congrArg₂ List.cons hxy hxys)
+      | isFalse hxy, _ => isFalse fun h => hxy (List.cons.inj h).1
+      | _, isFalse hxys => isFalse fun h => hxys (List.cons.inj h).2
+end
+
+instance : DecidableEq Data := Data.decEq
+instance : BEq Data := inferInstance
+instance : LawfulBEq Data := inferInstance
+
+/-- The empty `Data` node, `Data.l []`. -/
+abbrev Data.empty := Data.l []
+
+
+/-- The list of children of a `Data` node. -/
+@[scoped grind =]
+def Data.asList
+  | Data.l xs => xs
+
+@[scoped grind =]
+lemma Data.asList_empty : Data.empty.asList = [] := by rfl
+
+@[simp, scoped grind =]
+lemma Data.asList_l (d : Data) : Data.l d.asList = d := by simp [Data.asList]; grind
+
+@[simp, scoped grind =]
+lemma Data.l_asList (xs : List Data) : (Data.l xs).asList = xs := by simp [Data.asList]
+
+/-- The encoding length of `d`, relevant for complexity.
+This is the encoded size assuming an encoding into parenthesized expressions. -/
+def Data.size : Data → ℕ
+  | Data.l xs => 2 + (xs.map Data.size |>.sum)
+
+@[simp]
+lemma Data.size_le {d : Data} : 0 < d.size := by
+  obtain ⟨xs⟩ := d
+  grind [Data.size]
+
+@[simp, scoped grind =]
+lemma Data.size_empty : Data.empty.size = 2 := by simp [Data.empty, Data.size]
+
+@[simp, scoped grind =]
+lemma Data.cons_size {h : Data} {t : List Data} :
+    (Data.l (h :: t)).size = h.size + (Data.l t).size := by
+  simp [Data.size]
+  grind
+
+lemma Data.size_lt_of_mem {c : Data} {xs : List Data} (hc : c ∈ xs) :
+    c.size < (Data.l xs).size := by
+  induction xs with
+  | nil => simp at hc
+  | cons a as ih =>
+    rw [Data.cons_size]
+    rcases List.mem_cons.1 hc with h | h
+    · subst h; have := @Data.size_le (Data.l as); omega
+    · have := ih h; omega
+
+/-- Recursion principle for `Data`. -/
+@[elab_as_elim]
+def Data.recL {motive : Data → Sort*}
+    (nil : motive (Data.l []))
+    (cons : ∀ (x : Data) (xs : List Data),
+      motive x → motive (Data.l xs) → motive (Data.l (x :: xs))) :
+    ∀ d, motive d
+  | .l [] => nil
+  | .l (x :: xs) =>
+      cons x xs (Data.recL nil cons x) (Data.recL nil cons (.l xs))
+
+/-- Induction principle for `Data`, the `Prop`-valued companion to `Data.recL`. -/
+@[elab_as_elim]
+theorem Data.inductionL {motive : Data → Prop}
+    (nil : motive (Data.l []))
+    (cons : ∀ (x : Data) (xs : List Data),
+      motive x → motive (Data.l xs) → motive (Data.l (x :: xs)))
+    (d : Data) : motive d :=
+  Data.recL nil cons d
+
+/-! ## Bitstring serialization
+
+`Data.toBits` serializes a `Data` value into a `List Bool` using a parenthesized
+(balanced-bracket) encoding: `false` opens a node, its children are serialized in order, and
+`true` closes the node. This matches `Data.size` exactly (`Data.length_toBits`) and is injective
+(`Data.toBits_injective`), so any `DataEncode` instance yields an injective bitstring encoding
+(see `Complexitylib.Encoding.DataEncode`). -/
+
+/-- Serialize `Data` into a bitstring with a parenthesized (balanced-bracket) encoding: `false`
+opens a node, the children are serialized in order, and `true` closes the node. -/
+def Data.toBits : Data → List Bool
+  | Data.l xs => false :: ((xs.map Data.toBits).flatten ++ [true])
+
+lemma Data.toBits_l (xs : List Data) :
+    (Data.l xs).toBits = false :: ((xs.map Data.toBits).flatten ++ [true]) := by
+  rw [Data.toBits]
+
+@[simp]
+lemma Data.length_toBits (d : Data) : d.toBits.length = d.size := by
+  induction d using Data.inductionL with
+  | nil => simp [Data.toBits]
+  | cons x xs ihx ihxs =>
+    simp only [Data.toBits, Data.size, List.map_cons, List.flatten_cons, List.length_cons,
+      List.length_append, List.length_flatten, List.map_map] at *
+    grind
+
+/-- One step of the stack-based `Data.fromBits` parser. The state is a stack of frames, each a
+list of the sibling nodes completed so far at that nesting depth (outermost frame at the bottom).
+Reading `false` opens a new (empty) frame; reading `true` closes the top frame into a `Data.l`
+node and appends it to its parent. `none` is a permanent failure state (an unmatched `true`). -/
+def Data.fromBitsStep : Option (List (List Data)) → Bool → Option (List (List Data))
+  | none, _ => none
+  | some stack, false => some ([] :: stack)
+  | some stack, true =>
+    match stack with
+    | kids :: parent :: rest => some ((parent ++ [Data.l kids]) :: rest)
+    | _ => none
+
+/-- Decode a bitstring produced by `Data.toBits` back into a `Data` value, or `none` if it is not
+a valid single serialization. This is a left inverse of `Data.toBits` (`Data.fromBits_toBits`). -/
+def Data.fromBits (bits : List Bool) : Option Data :=
+  match bits.foldl Data.fromBitsStep (some [[]]) with
+  | some [[d]] => some d
+  | _ => none
+
+/-- Running `Data.fromBitsStep` over `d.toBits` appends the decoded `d` to the top frame of the
+stack, leaving the rest of the stack untouched. This is the key lemma behind
+`Data.fromBits_toBits`. -/
+theorem Data.foldl_fromBitsStep_toBits :
+    ∀ (d : Data) (top : List Data) (rest : List (List Data)),
+      d.toBits.foldl Data.fromBitsStep (some (top :: rest)) = some ((top ++ [d]) :: rest) := by
+  -- Strong induction on the size of `d`, so that each child (strictly smaller) can appeal to the
+  -- inductive hypothesis while a plain list induction consumes the children in order.
+  have key : ∀ (n : ℕ) (d : Data) (top : List Data) (rest : List (List Data)),
+      d.size ≤ n →
+      d.toBits.foldl Data.fromBitsStep (some (top :: rest)) = some ((top ++ [d]) :: rest) := by
+    intro n
+    induction n using Nat.strongRecOn with
+    | ind n IH =>
+      rintro ⟨xs⟩ top rest hsz
+      -- Consuming the flattened children appends them, in order, to the current frame.
+      have L : ∀ (xs : List Data) (cur : List Data) (rest : List (List Data)),
+          (∀ c ∈ xs, c.size < n) →
+          (xs.map Data.toBits).flatten.foldl Data.fromBitsStep (some (cur :: rest))
+            = some ((cur ++ xs) :: rest) := by
+        intro xs
+        induction xs with
+        | nil => intro cur rest _; simp
+        | cons c cs ihcs =>
+          intro cur rest hlt
+          have hc : c.size < n := hlt c (List.mem_cons_self ..)
+          simp only [List.map_cons, List.flatten_cons, List.foldl_append]
+          rw [IH c.size hc c cur rest (Nat.le_refl _),
+            ihcs (cur ++ [c]) rest (fun c' hc' => hlt c' (List.mem_cons_of_mem _ hc'))]
+          simp
+      rw [Data.toBits_l]
+      simp only [List.foldl_cons, List.foldl_append, Data.fromBitsStep]
+      rw [L xs [] (top :: rest) (fun c hc => Nat.lt_of_lt_of_le (Data.size_lt_of_mem hc) hsz)]
+      simp
+  intro d top rest
+  exact key d.size d top rest (Nat.le_refl _)
+
+/-- `Data.fromBits` recovers any value serialized by `Data.toBits`. -/
+@[simp]
+theorem Data.fromBits_toBits (d : Data) : Data.fromBits d.toBits = some d := by
+  simp only [Data.fromBits, Data.foldl_fromBitsStep_toBits, List.nil_append]
+
+/-- `Data.toBits` is injective: the parenthesized serialization determines the value. This follows
+from `Data.fromBits` being a left inverse. -/
+theorem Data.toBits_injective : Function.Injective Data.toBits := by
+  intro a b h
+  have := Data.fromBits_toBits a
+  rw [h, Data.fromBits_toBits b] at this
+  exact Option.some.inj this.symm
+
+end Complexity
diff --git a/Complexitylib/Models/RoseTreeMachine/DataEncode.lean b/Complexitylib/Encoding/DataEncode.lean
similarity index 69%
rename from Complexitylib/Models/RoseTreeMachine/DataEncode.lean
rename to Complexitylib/Encoding/DataEncode.lean
index 91bcf703..b1e81b25 100644
--- a/Complexitylib/Models/RoseTreeMachine/DataEncode.lean
+++ b/Complexitylib/Encoding/DataEncode.lean
@@ -5,19 +5,23 @@ Authors: Christian Reitwiessner
 -/
 
 module
-public import Complexitylib.Models.RoseTreeMachine.Data
+public import Complexitylib.Encoding.Data
 public import Mathlib.Data.Nat.Bits
 public import Mathlib.Data.List.Basic
 
 /-!
 # Encodings into `Data`
 
-This file defines the class that is used to encode arbitrary data structures into `Data`,
-so that RTMs (rose tree machines) can operate on them.
+This file defines the class that is used to encode arbitrary data structures into `Data`
+(`Complexitylib.Encoding.Data`), so that RTMs (rose tree machines) can operate on them.
 
 Instances are provided for convenience for `Data` itself, `Bool`, `List α`, `Option α`, `α × β`,
-and `ℕ` (binary encoding via `List Bool`)
+and `ℕ` (binary encoding via `List Bool`).
 
+Every `DataEncode` instance also yields a *bitstring* encoding `DataEncode.bitstringEncode`, by
+serializing the target `Data` value with `Data.toBits`. Since both the `DataEncode` instance and
+`Data.toBits` are injective, `bitstringEncode` is injective too
+(`DataEncode.bitstringEncode_injective`).
 -/
 
 
@@ -25,8 +29,6 @@ and `ℕ` (binary encoding via `List Bool`)
 
 namespace Complexity
 
-namespace RoseTreeMachine
-
 /-- Encoding of types into `Data`. -/
 class DataEncode (α : Type) where
   /-- Encode a value of `α` as `Data`. -/
@@ -102,6 +104,19 @@ instance : DataEncode ℕ where
     have := congrArg (List.foldr (fun b acc => Nat.bit b acc) 0) hb
     simpa [hrec] using this
 
-end RoseTreeMachine
+/-- Encode a value into a bitstring (`List Bool`) by first encoding it into `Data` and then
+serializing that with the parenthesized `Data.toBits`. This is the class-inferrable bitstring
+encoding available for any type with a `DataEncode` instance. -/
+def DataEncode.bitstringEncode {α : Type} [DataEncode α] (a : α) : List Bool :=
+  (DataEncode.encode a).toBits
+
+lemma DataEncode.bitstringEncode_def {α : Type} [DataEncode α] (a : α) :
+    DataEncode.bitstringEncode a = (DataEncode.encode a).toBits := rfl
+
+/-- The bitstring encoding is injective: distinct values yield distinct bitstrings. This composes
+the injectivity of the `DataEncode` instance with that of `Data.toBits`. -/
+theorem DataEncode.bitstringEncode_injective {α : Type} [DataEncode α] :
+    Function.Injective (DataEncode.bitstringEncode (α := α)) :=
+  Data.toBits_injective.comp DataEncode.h_inj
 
 end Complexity
diff --git a/Complexitylib/Encoding/Delimit.lean b/Complexitylib/Encoding/Delimit.lean
index ffb897e2..f18be139 100644
--- a/Complexitylib/Encoding/Delimit.lean
+++ b/Complexitylib/Encoding/Delimit.lean
@@ -30,9 +30,9 @@ end. This file defines the library's single framing operation and its parsers:
 - `undelimitBlock`, `takeFirstBlock`, `hasBlock`, `tagBlock`, and `undelimitBlocks` are the
   total helper functions machines compute when working with framed data.
 
-This file deliberately has no dependency on the machine or complexity-class layers, so both
-the machine-input pairing codec (`Complexitylib.Encoding.Pairing`) and the encoding layer
-(`Complexitylib.Encoding.Bitstring`) can build on it without import cycles.
+This file deliberately has no dependency on the machine or complexity-class layers, so the
+machine-input pairing codec (`Complexitylib.Encoding.Pairing`) can build on it without import
+cycles.
 -/
 
 
diff --git a/Complexitylib/Models.lean b/Complexitylib/Models.lean
index ae8ecc48..e1b5323f 100644
--- a/Complexitylib/Models.lean
+++ b/Complexitylib/Models.lean
@@ -67,8 +67,6 @@ public import Complexitylib.Models.TuringMachine.UTM.ClockedUtm
 public import Complexitylib.Models.TuringMachine.UTM.HierarchySupport
 public import Complexitylib.Models.TuringMachine.UTM.Diagonal
 public import Complexitylib.Models.RandomAccessMachine
-public import Complexitylib.Models.RoseTreeMachine.Data
-public import Complexitylib.Models.RoseTreeMachine.DataEncode
 public import Complexitylib.Models.RoseTreeMachine.Prog
 
 /-!
diff --git a/Complexitylib/Models/RoseTreeMachine/Data.lean b/Complexitylib/Models/RoseTreeMachine/Data.lean
deleted file mode 100644
index 6fb2959b..00000000
--- a/Complexitylib/Models/RoseTreeMachine/Data.lean
+++ /dev/null
@@ -1,128 +0,0 @@
-/-
-Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Christian Reitwiessner
--/
-
-module
-public import Aesop.BuiltinRules
-public import Mathlib.Data.Nat.Notation
-public import Mathlib.Tactic.Finiteness.Attr
-public import Mathlib.Tactic.Push
-public import Mathlib.Tactic.ToAdditive
-public import Mathlib.Tactic.ToDual
-
-/-!
-# Main internal data type for the rose tree machine (RTM)
-
-This file contains the main internal data structure for the RTM, `Data`, a rose tree.
-
-## Main definitions and notations
-
-- `Data` - the main data structure
-- `Data.size` - the size of a `Data` object when encoded using parentheses, complexity results
-  use this size as the main measure.
-- `Data.recL` - the main recursion principle for `Data`
-- `Data.inductionL` - the main induction principle for `Data`
-
--/
-
-
-@[expose] public section
-
-namespace Complexity
-
-namespace RoseTreeMachine
-
-/-- Rose-tree data structure, it allows us to encode most of Lean's data structures in a
-"natural" manner -/
-inductive Data where
-  | l : List Data → Data
-deriving Repr
-
-mutual
-  /-- Decidable equality for `Data`, defined jointly with `Data.listDecEq`. -/
-  def Data.decEq : ∀ (a b : Data), Decidable (a = b)
-    | .l xs, .l ys =>
-      match Data.listDecEq xs ys with
-      | isTrue h => isTrue (congrArg Data.l h)
-      | isFalse h => isFalse fun heq => h (Data.l.inj heq)
-  /-- Decidable equality for `List Data`, defined jointly with `Data.decEq`. -/
-  def Data.listDecEq : ∀ (xs ys : List Data), Decidable (xs = ys)
-    | [], [] => isTrue rfl
-    | [], _ :: _ => isFalse (by simp)
-    | _ :: _, [] => isFalse (by simp)
-    | x :: xs, y :: ys =>
-      match Data.decEq x y, Data.listDecEq xs ys with
-      | isTrue hxy, isTrue hxys => isTrue (congrArg₂ List.cons hxy hxys)
-      | isFalse hxy, _ => isFalse fun h => hxy (List.cons.inj h).1
-      | _, isFalse hxys => isFalse fun h => hxys (List.cons.inj h).2
-end
-
-instance : DecidableEq Data := Data.decEq
-instance : BEq Data := inferInstance
-instance : LawfulBEq Data := inferInstance
-
-/-- The empty `Data` node, `Data.l []`. -/
-abbrev Data.empty := Data.l []
-
-
-/-- The list of children of a `Data` node. -/
-@[scoped grind =]
-def Data.asList
-  | Data.l xs => xs
-
-@[scoped grind =]
-lemma Data.asList_empty : Data.empty.asList = [] := by rfl
-
-@[simp, scoped grind =]
-lemma Data.asList_l (d : Data) : Data.l d.asList = d := by simp [Data.asList]; grind
-
-@[simp, scoped grind =]
-lemma Data.l_asList (xs : List Data) : (Data.l xs).asList = xs := by simp [Data.asList]
-
-/-- The encoding length of `d`, relevant for complexity.
-This is the encoded size assuming an encoding into parenthesized expressions. -/
-def Data.size : Data → ℕ
-  | Data.l xs => 2 + (xs.map Data.size |>.sum)
-
-@[simp]
-lemma Data.size_le {d : Data} : 0 < d.size := by
-  obtain ⟨xs⟩ := d
-  grind [Data.size]
-
-@[simp, scoped grind =]
-lemma Data.size_empty : Data.empty.size = 2 := by simp [Data.empty, Data.size]
-
-@[simp, scoped grind =]
-lemma Data.cons_size {h : Data} {t : List Data} :
-    (Data.l (h :: t)).size = h.size + (Data.l t).size := by
-  simp [Data.size]
-  grind
-
-/-- Recursion principle for `Data`. -/
-@[elab_as_elim]
-def Data.recL {motive : Data → Sort*}
-    (nil : motive (Data.l []))
-    (cons : ∀ (x : Data) (xs : List Data),
-      motive x → motive (Data.l xs) → motive (Data.l (x :: xs))) :
-    ∀ d, motive d
-  | .l [] => nil
-  | .l (x :: xs) =>
-      cons x xs (Data.recL nil cons x) (Data.recL nil cons (.l xs))
-
-/-- Induction principle for `Data`, the `Prop`-valued companion to `Data.recL`. -/
-@[elab_as_elim]
-theorem Data.inductionL {motive : Data → Prop}
-    (nil : motive (Data.l []))
-    (cons : ∀ (x : Data) (xs : List Data),
-      motive x → motive (Data.l xs) → motive (Data.l (x :: xs)))
-    (d : Data) : motive d :=
-  Data.recL nil cons d
-
-/-- Index of a tape cell used by the rose tree machine's execution model. -/
-abbrev TapeIndex := ℕ
-
-end RoseTreeMachine
-
-end Complexity
diff --git a/Complexitylib/Models/RoseTreeMachine/Prog.lean b/Complexitylib/Models/RoseTreeMachine/Prog.lean
index 73adbc2e..606a9246 100644
--- a/Complexitylib/Models/RoseTreeMachine/Prog.lean
+++ b/Complexitylib/Models/RoseTreeMachine/Prog.lean
@@ -5,7 +5,7 @@ Authors: Christian Reitwiessner
 -/
 
 module
-public import Complexitylib.Models.RoseTreeMachine.DataEncode
+public import Complexitylib.Encoding.DataEncode
 public import Mathlib.Order.Lattice
 public import Std.Tactic.BVDecide.Normalize.Prop
 
@@ -36,6 +36,9 @@ namespace Complexity
 
 namespace RoseTreeMachine
 
+/-- Index of a tape cell used by the rose tree machine's execution model. -/
+abbrev TapeIndex := ℕ
+
 /--
 Prog is the syntax representation of a functional language that has a resource consumption
 model which is compatible to that of a Turing machine.