diff --git a/Complexitylib.lean b/Complexitylib.lean
index b0814aeb..0bb073c4 100644
--- a/Complexitylib.lean
+++ b/Complexitylib.lean
@@ -6,6 +6,7 @@ Authors: Samuel Schlesinger
 
 module
 public import Complexitylib.Models
+public import Complexitylib.Encoding
 public import Complexitylib.Asymptotics
 public import Complexitylib.TimeConstructible
 public import Complexitylib.Classes
diff --git a/Complexitylib/Classes/NP/Internal/PairBuildTM.lean b/Complexitylib/Classes/NP/Internal/PairBuildTM.lean
index 8b401373..a0bdde43 100644
--- a/Complexitylib/Classes/NP/Internal/PairBuildTM.lean
+++ b/Complexitylib/Classes/NP/Internal/PairBuildTM.lean
@@ -1023,7 +1023,7 @@ private theorem pairBuild_copyY_loop {k : ℕ} (yIdx pIdx : Fin k)
 /-- Helper: `pair (b :: xs) y = b :: b :: pair xs y`. -/
 private theorem pair_build_cons_eq (b : Bool) (xs y : List Bool) :
     pair (b :: xs) y = b :: b :: pair xs y := by
-  simp [pair, List.append_assoc]
+  simp [pair]
 
 /-- Shift lemma: accessing `pair (b :: xs) y` at index `k+2` is the same as
     accessing `pair xs y` at index `k`. -/
diff --git a/Complexitylib/Classes/PPoly/Advice.lean b/Complexitylib/Classes/PPoly/Advice.lean
index d9d3c2ae..e791f562 100644
--- a/Complexitylib/Classes/PPoly/Advice.lean
+++ b/Complexitylib/Classes/PPoly/Advice.lean
@@ -45,7 +45,7 @@ namespace Advice
 input. -/
 theorem fixedPrefix_append (a : Advice) (x : List Bool) :
     a.fixedPrefix x.length ++ x = advisedInput a x := by
-  simp [fixedPrefix, advisedInput, pair, List.append_assoc]
+  simp [fixedPrefix, advisedInput, pair]
 
 /-- The fixed-prefix bit string serializes to the self-delimiting advised
 machine input. -/
diff --git a/Complexitylib/Encoding.lean b/Complexitylib/Encoding.lean
new file mode 100644
index 00000000..20e12024
--- /dev/null
+++ b/Complexitylib/Encoding.lean
@@ -0,0 +1,22 @@
+/-
+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 Complexitylib.Encoding.Pairing
+public import Complexitylib.Encoding.Data
+public import Complexitylib.Encoding.DataEncode
+
+/-!
+# 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 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/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
new file mode 100644
index 00000000..f18be139
--- /dev/null
+++ b/Complexitylib/Encoding/Delimit.lean
@@ -0,0 +1,209 @@
+/-
+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 Mathlib.Data.List.Basic
+public import Mathlib.Data.Nat.Init
+public import Aesop.BuiltinRules
+public import Mathlib.Tactic.Attr.Core
+public import Mathlib.Tactic.Basic
+public import Mathlib.Tactic.Push
+public import Mathlib.Tactic.Widget.Calc
+public import Std.Tactic.BVDecide.Normalize.Prop
+
+/-!
+# 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 the
+machine-input pairing codec (`Complexitylib.Encoding.Pairing`) can build on it without import
+cycles.
+-/
+
+
+@[expose] public section
+
+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 c09dfea6..297ff174 100644
--- a/Complexitylib/Encoding/Pairing.lean
+++ b/Complexitylib/Encoding/Pairing.lean
@@ -5,6 +5,7 @@ Authors: Samuel Schlesinger
 -/
 
 module
+public import Complexitylib.Encoding.Delimit
 public import Mathlib.Data.Nat.Init
 public import Aesop.BuiltinRules
 public import Mathlib.Tactic.Attr.Core
@@ -17,9 +18,11 @@ public import Std.Tactic.BVDecide.Normalize.Prop
 # 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.
 -/
 
 
@@ -27,24 +30,11 @@ 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
@@ -54,7 +44,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]`. -/
@@ -101,55 +91,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.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.
diff --git a/Complexitylib/Models/TuringMachine/Subroutines/PairEmit/Internal.lean b/Complexitylib/Models/TuringMachine/Subroutines/PairEmit/Internal.lean
index 287298a8..c8799d0d 100644
--- a/Complexitylib/Models/TuringMachine/Subroutines/PairEmit/Internal.lean
+++ b/Complexitylib/Models/TuringMachine/Subroutines/PairEmit/Internal.lean
@@ -320,7 +320,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 a5c8e76f..2a9ac856 100644
--- a/Complexitylib/Models/TuringMachine/UTM/Internal/Init.lean
+++ b/Complexitylib/Models/TuringMachine/UTM/Internal/Init.lean
@@ -1276,7 +1276,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 02388b4a..8f2e58a7 100644
--- a/Complexitylib/SAT/ThreeSAT/Verifier.lean
+++ b/Complexitylib/SAT/ThreeSAT/Verifier.lean
@@ -97,7 +97,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) <;>