From 0cd989d04013b4547c9b8d19768e359c85c6fdc9 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 24 Jul 2026 12:53:38 -0700
Subject: [PATCH 1/4] feat(Classes): define the polynomial hierarchy
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Define certificate quantifiers over the pair codec (polyExistsLang /
polyForallLang and their class operators), the levels SigmaP / PiP by
the standard recursion through complement classes, and PH as their
union. Prove quantifier and class-level complement duality,
monotonicity, the recursion laws, and level inclusions, the latter
conditional on the single machine-engineering seam `pairFst ∈ FP`
(first-component pair decoding), isolated as a hypothesis following the
WitnessNTMConstruction pattern. Ported from leanprover/cslib#192,
re-proved against this library's machine model and Set-based languages.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Complexitylib/Classes.lean    |   1 +
 Complexitylib/Classes/PH.lean | 299 ++++++++++++++++++++++++++++++++++
 2 files changed, 300 insertions(+)
 create mode 100644 Complexitylib/Classes/PH.lean

diff --git a/Complexitylib/Classes.lean b/Complexitylib/Classes.lean
index dc8ceb19..560697cd 100644
--- a/Complexitylib/Classes.lean
+++ b/Complexitylib/Classes.lean
@@ -58,6 +58,7 @@ import Complexitylib.Classes.Randomized.PPoly
 import Complexitylib.Classes.Pairing
 import Complexitylib.Classes.FNP
 import Complexitylib.Classes.NP.Witness
+import Complexitylib.Classes.PH
 import Complexitylib.Classes.NP.Reduction
 import Complexitylib.Classes.L
 import Complexitylib.Classes.L.PolynomialTime
diff --git a/Complexitylib/Classes/PH.lean b/Complexitylib/Classes/PH.lean
new file mode 100644
index 00000000..12ec6727
--- /dev/null
+++ b/Complexitylib/Classes/PH.lean
@@ -0,0 +1,299 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Complexitylib.Classes.Containments
+import Complexitylib.Encoding.Pairing
+import Mathlib.Algebra.Polynomial.Eval.Defs
+
+/-!
+# The polynomial hierarchy
+
+This file defines the polynomial hierarchy via certificate quantifiers, following
+the quantified-formula definition (Arora–Barak Definition 5.4, stated over the
+library's `pair` codec): `polyExistsLang p L` holds of `x` when some witness `w`
+of length at most `p.eval |x|` puts the encoded pair `pair x w` in `L`, and
+`polyForallLang p L` requires this of every such witness. Lifting these to class
+operators gives the levels `SigmaP 0 = P`, `SigmaP (n + 1) =
+polyExistsClass (PiP n)`, `PiP n = complClass (SigmaP n)`, and their union `PH`.
+
+The level inclusions `SigmaP n ⊆ SigmaP (n + 1)` and `PiP n ⊆ PiP (n + 1)` are
+proved relative to a single machine-engineering seam, stated as the hypothesis
+`pairFst ∈ FP`: decoding the first component of a canonical pair is
+polynomial-time computable. This follows the interface-isolation pattern of
+`Complexitylib.Classes.NP.Witness` — every set-theoretic consequence is proved
+unconditionally here, and the one remaining TM construction can land later
+without touching this file's statements. All other results are unconditional.
+
+## Main definitions
+
+- `polyExistsLang`, `polyForallLang` — witness quantifiers on languages
+- `polyExistsClass`, `polyForallClass` — the induced operators on classes
+- `pairFst` — first-component decoder for the pairing codec
+- `SigmaP`, `PiP`, `PH` — the hierarchy levels and their union
+
+## Main results
+
+- `compl_polyExistsLang` / `compl_polyForallLang` — quantifier duality
+- `complClass_polyExistsClass` / `complClass_polyForallClass` — class duality
+- `complClass_P` — `P` is closed under language complement, as a class equation
+- `SigmaP_zero`, `PiP_zero`, `SigmaP_succ`, `PiP_succ` — recursion laws
+- `P_subset_polyExistsClass_P` / `P_subset_polyForallClass_P` — base inclusions
+  (given `pairFst ∈ FP`)
+- `SigmaP_subset_SigmaP_succ` / `PiP_subset_PiP_succ` — level inclusions
+  (given `pairFst ∈ FP`)
+- `SigmaP_subset_PH`, `P_subset_PH`
+
+## TODO
+
+- Implement the `pairFst ∈ FP` seam: split the input with a
+  `pairSplitCoreTM`-style scanner and copy the decoded first component to the
+  output tape, packaging the result as `TM.ComputesInTime`.
+- Relate `SigmaP 1` to the NTM-based `NP` through the witness characterization
+  interface in `Complexitylib.Classes.NP.Witness`.
+-/
+
+namespace Complexity
+
+/-! ## Witness quantifiers on languages -/
+
+/-- The language of inputs `x` admitting a witness `w` of length at most
+`p.eval |x|` such that the encoded pair `pair x w` lies in `L`. -/
+def polyExistsLang (p : Polynomial ℕ) (L : Language) : Language :=
+  {x | ∃ w, w.length ≤ p.eval x.length ∧ pair x w ∈ L}
+
+/-- The language of inputs `x` such that every witness `w` of length at most
+`p.eval |x|` puts the encoded pair `pair x w` in `L`. -/
+def polyForallLang (p : Polynomial ℕ) (L : Language) : Language :=
+  {x | ∀ w, w.length ≤ p.eval x.length → pair x w ∈ L}
+
+/-- Membership in `polyExistsLang` unfolds to a bounded existential. -/
+@[simp] theorem mem_polyExistsLang {p : Polynomial ℕ} {L : Language} {x : List Bool} :
+    x ∈ polyExistsLang p L ↔ ∃ w, w.length ≤ p.eval x.length ∧ pair x w ∈ L :=
+  Iff.rfl
+
+/-- Membership in `polyForallLang` unfolds to a bounded universal. -/
+@[simp] theorem mem_polyForallLang {p : Polynomial ℕ} {L : Language} {x : List Bool} :
+    x ∈ polyForallLang p L ↔ ∀ w, w.length ≤ p.eval x.length → pair x w ∈ L :=
+  Iff.rfl
+
+/-- Complementing a bounded existential yields a bounded universal over the
+complement: some-witness failure is all-witness exclusion. -/
+theorem compl_polyExistsLang (p : Polynomial ℕ) (L : Language) :
+    (polyExistsLang p L)ᶜ = polyForallLang p Lᶜ := by
+  ext x
+  simp [polyExistsLang, polyForallLang]
+
+/-- Complementing a bounded universal yields a bounded existential over the
+complement. -/
+theorem compl_polyForallLang (p : Polynomial ℕ) (L : Language) :
+    (polyForallLang p L)ᶜ = polyExistsLang p Lᶜ := by
+  ext x
+  simp [polyExistsLang, polyForallLang]
+
+/-! ## Quantifier operators on classes -/
+
+/-- The class of languages expressible as a polynomially-bounded existential
+over some language of `C`. -/
+def polyExistsClass (C : Set Language) : Set Language :=
+  {L | ∃ (p : Polynomial ℕ), ∃ L' ∈ C, L = polyExistsLang p L'}
+
+/-- The class of languages expressible as a polynomially-bounded universal
+over some language of `C`. -/
+def polyForallClass (C : Set Language) : Set Language :=
+  {L | ∃ (p : Polynomial ℕ), ∃ L' ∈ C, L = polyForallLang p L'}
+
+/-- `polyExistsClass` is monotone in the base class. -/
+theorem polyExistsClass_mono {C D : Set Language} (h : C ⊆ D) :
+    polyExistsClass C ⊆ polyExistsClass D := by
+  rintro L ⟨p, L', hL', rfl⟩
+  exact ⟨p, L', h hL', rfl⟩
+
+/-- `polyForallClass` is monotone in the base class. -/
+theorem polyForallClass_mono {C D : Set Language} (h : C ⊆ D) :
+    polyForallClass C ⊆ polyForallClass D := by
+  rintro L ⟨p, L', hL', rfl⟩
+  exact ⟨p, L', h hL', rfl⟩
+
+/-- `complClass` is monotone. -/
+theorem complClass_mono {C D : Set Language} (h : C ⊆ D) :
+    complClass C ⊆ complClass D :=
+  fun _ hL => h hL
+
+/-- Class-level quantifier duality: the complement class of a bounded
+existential class is the bounded universal class over the complement class. -/
+theorem complClass_polyExistsClass (C : Set Language) :
+    complClass (polyExistsClass C) = polyForallClass (complClass C) := by
+  ext L
+  simp only [mem_complClass, polyExistsClass, polyForallClass, Set.mem_setOf_eq]
+  constructor
+  · rintro ⟨p, L', hL', hEq⟩
+    refine ⟨p, L'ᶜ, by simpa [mem_complClass, compl_compl] using hL', ?_⟩
+    rw [← compl_compl L, hEq, compl_polyExistsLang]
+  · rintro ⟨p, L', hL', rfl⟩
+    exact ⟨p, L'ᶜ, hL', by rw [compl_polyForallLang]⟩
+
+/-- Class-level quantifier duality: the complement class of a bounded universal
+class is the bounded existential class over the complement class. -/
+theorem complClass_polyForallClass (C : Set Language) :
+    complClass (polyForallClass C) = polyExistsClass (complClass C) := by
+  ext L
+  simp only [mem_complClass, polyExistsClass, polyForallClass, Set.mem_setOf_eq]
+  constructor
+  · rintro ⟨p, L', hL', hEq⟩
+    refine ⟨p, L'ᶜ, by simpa [mem_complClass, compl_compl] using hL', ?_⟩
+    rw [← compl_compl L, hEq, compl_polyForallLang]
+  · rintro ⟨p, L', hL', rfl⟩
+    exact ⟨p, L'ᶜ, hL', by rw [compl_polyExistsLang]⟩
+
+/-! ## The pair decoder seam -/
+
+/-- Decode the first component of a canonical pair, returning `[]` on malformed
+inputs. Statements below take the hypothesis `pairFst ∈ FP` — the one remaining
+machine construction of this development (see the module docstring). -/
+def pairFst (z : List Bool) : List Bool :=
+  ((unpair? z).map Prod.fst).getD []
+
+/-- `pairFst` recovers the first component of a canonical pair. -/
+@[simp] theorem pairFst_pair (x y : List Bool) : pairFst (pair x y) = x := by
+  simp [pairFst]
+
+/-! ## Base inclusions -/
+
+/-- `P` is closed under complement, stated as a class equation. -/
+theorem complClass_P : complClass P = P := by
+  ext L
+  exact ⟨fun h => compl_compl L ▸ P_compl h, fun h => P_compl h⟩
+
+/-- Every language of `P` is a bounded existential over `P`: take the zero
+witness bound, so the only witness is `[]`, and decide `pair x []` by decoding
+the first component and running the original decider. -/
+theorem P_subset_polyExistsClass_P (hpair : pairFst ∈ FP) :
+    P ⊆ polyExistsClass P := by
+  intro L hL
+  refine ⟨0, pairFst ⁻¹' L, mem_P_preimage hpair hL, ?_⟩
+  ext x
+  simp only [mem_polyExistsLang, Polynomial.eval_zero, Nat.le_zero,
+    List.length_eq_zero_iff, Set.mem_preimage]
+  constructor
+  · intro hx
+    exact ⟨[], rfl, by simpa using hx⟩
+  · rintro ⟨w, rfl, hmem⟩
+    simpa using hmem
+
+/-- Every language of `P` is a bounded universal over `P`: with the zero
+witness bound the only witness is `[]`, decided as in
+`P_subset_polyExistsClass_P`. -/
+theorem P_subset_polyForallClass_P (hpair : pairFst ∈ FP) :
+    P ⊆ polyForallClass P := by
+  intro L hL
+  refine ⟨0, pairFst ⁻¹' L, mem_P_preimage hpair hL, ?_⟩
+  ext x
+  simp only [mem_polyForallLang, Polynomial.eval_zero, Nat.le_zero,
+    List.length_eq_zero_iff, Set.mem_preimage]
+  constructor
+  · rintro hx w rfl
+    simpa using hx
+  · intro h
+    simpa using h [] rfl
+
+/-! ## The hierarchy -/
+
+/-- The Σ levels of the polynomial hierarchy: `SigmaP 0 = P` and
+`SigmaP (n + 1)` is a bounded existential over the complement class of
+`SigmaP n` (that is, over `PiP n`). -/
+def SigmaP : ℕ → Set Language
+  | 0 => P
+  | n + 1 => polyExistsClass (complClass (SigmaP n))
+
+/-- The Π levels of the polynomial hierarchy: `PiP n` is the complement class
+of `SigmaP n`. -/
+def PiP (n : ℕ) : Set Language :=
+  complClass (SigmaP n)
+
+/-- The polynomial hierarchy: the union of all Σ levels. -/
+def PH : Set Language :=
+  ⋃ n : ℕ, SigmaP n
+
+/-- The zeroth Σ level is `P`. -/
+@[simp] theorem SigmaP_zero : SigmaP 0 = P := rfl
+
+/-- The complement class of a Σ level is the corresponding Π level. -/
+@[simp] theorem complClass_SigmaP (n : ℕ) : complClass (SigmaP n) = PiP n := rfl
+
+/-- The complement class of a Π level is the corresponding Σ level. -/
+@[simp] theorem complClass_PiP (n : ℕ) : complClass (PiP n) = SigmaP n := by
+  rw [PiP, complClass_complClass]
+
+/-- The zeroth Π level is `P`, since `P` is closed under complement. -/
+@[simp] theorem PiP_zero : PiP 0 = P := by
+  rw [PiP, SigmaP_zero, complClass_P]
+
+/-- Recursion law for Σ levels: `SigmaP (n + 1)` is a bounded existential over
+`PiP n`. -/
+theorem SigmaP_succ (n : ℕ) : SigmaP (n + 1) = polyExistsClass (PiP n) := rfl
+
+/-- Recursion law for Π levels: `PiP (n + 1)` is a bounded universal over
+`SigmaP n`. -/
+theorem PiP_succ (n : ℕ) : PiP (n + 1) = polyForallClass (SigmaP n) := by
+  rw [PiP]
+  show complClass (polyExistsClass (complClass (SigmaP n))) = _
+  rw [complClass_polyExistsClass, complClass_complClass]
+
+/-- The first Σ level is the bounded existential closure of `P` — the
+certificate form of `NP`. -/
+theorem SigmaP_one : SigmaP 1 = polyExistsClass P := by
+  rw [SigmaP_succ, PiP_zero]
+
+/-- The first Π level is the bounded universal closure of `P` — the
+certificate form of `coNP`. -/
+theorem PiP_one : PiP 1 = polyForallClass P := by
+  rw [PiP_succ, SigmaP_zero]
+
+/-! ## Level inclusions -/
+
+/-- Both level inclusions, proved simultaneously by induction: the base case is
+the pair of base inclusions of `P`, and each successor case is monotonicity of
+the opposite quantifier applied to the other component. -/
+private theorem piP_sigmaP_subset_succ (hpair : pairFst ∈ FP) (n : ℕ) :
+    PiP n ⊆ PiP (n + 1) ∧ SigmaP n ⊆ SigmaP (n + 1) := by
+  induction n with
+  | zero =>
+    constructor
+    · rw [PiP_zero, PiP_one]
+      exact P_subset_polyForallClass_P hpair
+    · rw [SigmaP_zero, SigmaP_one]
+      exact P_subset_polyExistsClass_P hpair
+  | succ n ih =>
+    constructor
+    · rw [PiP_succ, PiP_succ]
+      exact polyForallClass_mono ih.2
+    · rw [SigmaP_succ, SigmaP_succ]
+      exact polyExistsClass_mono ih.1
+
+/-- Each Σ level is contained in the next. -/
+theorem SigmaP_subset_SigmaP_succ (hpair : pairFst ∈ FP) (n : ℕ) :
+    SigmaP n ⊆ SigmaP (n + 1) :=
+  (piP_sigmaP_subset_succ hpair n).2
+
+/-- Each Π level is contained in the next. -/
+theorem PiP_subset_PiP_succ (hpair : pairFst ∈ FP) (n : ℕ) :
+    PiP n ⊆ PiP (n + 1) :=
+  (piP_sigmaP_subset_succ hpair n).1
+
+/-! ## PH -/
+
+/-- Membership in `PH` is membership in some Σ level. -/
+theorem mem_PH_iff {L : Language} : L ∈ PH ↔ ∃ n : ℕ, L ∈ SigmaP n :=
+  Set.mem_iUnion
+
+/-- Every Σ level is contained in the hierarchy. -/
+theorem SigmaP_subset_PH (n : ℕ) : SigmaP n ⊆ PH :=
+  fun _ h => Set.mem_iUnion.mpr ⟨n, h⟩
+
+/-- `P` is contained in the polynomial hierarchy. -/
+theorem P_subset_PH : P ⊆ PH :=
+  SigmaP_subset_PH 0
+
+end Complexity

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

From 1ce6597810916585c8e4c644ab71ec80af905663 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 13 Aug 2026 19:06:10 -0700
Subject: [PATCH 3/4] fix(Encoding): expose `DataEncode.bitstringEncode` for
 its `rfl` lemmas

`dev` de-exposed `Encoding/DataEncode.lean` as part of the module-interface
minimization, but this branch adds `bitstringEncode` together with
`bitstringEncode_def` and `bitstringEncode_injective`, both of which need
the definition's body to typecheck. Expose the single definition rather
than re-exposing the whole module.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Complexitylib/Encoding/DataEncode.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Complexitylib/Encoding/DataEncode.lean b/Complexitylib/Encoding/DataEncode.lean
index f8b20e81..9e613af3 100644
--- a/Complexitylib/Encoding/DataEncode.lean
+++ b/Complexitylib/Encoding/DataEncode.lean
@@ -107,7 +107,7 @@ instance : DataEncode ℕ where
 /-- 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 :=
+@[expose] def DataEncode.bitstringEncode {α : Type} [DataEncode α] (a : α) : List Bool :=
   (DataEncode.encode a).toBits
 
 lemma DataEncode.bitstringEncode_def {α : Type} [DataEncode α] (a : α) :

From 64ac47d84532d92f3d6e9560913f358c6099fd5e Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 13 Aug 2026 22:01:49 -0700
Subject: [PATCH 4/4] refactor(Encoding): move the rose-tree `Data` type into
 the encoding layer

`Data` and the `DataEncode` typeclass are machine-independent: `Data` is the
rose tree the RTM operates on, but it is also the target every `DataEncode`
instance encodes into, so it does not belong under `Models/RoseTreeMachine/`.

Move `Models/RoseTreeMachine/Data.lean` to `Encoding/Data.lean` and
`Models/RoseTreeMachine/DataEncode.lean` to `Encoding/DataEncode.lean`, and
repoint the three import statements that referred to the old paths.

Nothing else changes. `Encoding/Data.lean` is byte-identical to the file it
replaces; `Encoding/DataEncode.lean` differs only in its own import of
`Data`. Namespaces, module docs, comments and declarations are all untouched,
so the `Complexity.RoseTreeMachine` namespace is preserved for now.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Complexitylib/{Models/RoseTreeMachine => Encoding}/Data.lean  | 0
 .../{Models/RoseTreeMachine => Encoding}/DataEncode.lean      | 2 +-
 Complexitylib/Models.lean                                     | 4 ++--
 Complexitylib/Models/RoseTreeMachine/Prog.lean                | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)
 rename Complexitylib/{Models/RoseTreeMachine => Encoding}/Data.lean (100%)
 rename Complexitylib/{Models/RoseTreeMachine => Encoding}/DataEncode.lean (98%)

diff --git a/Complexitylib/Models/RoseTreeMachine/Data.lean b/Complexitylib/Encoding/Data.lean
similarity index 100%
rename from Complexitylib/Models/RoseTreeMachine/Data.lean
rename to Complexitylib/Encoding/Data.lean
diff --git a/Complexitylib/Models/RoseTreeMachine/DataEncode.lean b/Complexitylib/Encoding/DataEncode.lean
similarity index 98%
rename from Complexitylib/Models/RoseTreeMachine/DataEncode.lean
rename to Complexitylib/Encoding/DataEncode.lean
index d2409157..6059428c 100644
--- a/Complexitylib/Models/RoseTreeMachine/DataEncode.lean
+++ b/Complexitylib/Encoding/DataEncode.lean
@@ -5,7 +5,7 @@ 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
 
diff --git a/Complexitylib/Models.lean b/Complexitylib/Models.lean
index ae8ecc48..fdb7abca 100644
--- a/Complexitylib/Models.lean
+++ b/Complexitylib/Models.lean
@@ -67,8 +67,8 @@ 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.Encoding.Data
+public import Complexitylib.Encoding.DataEncode
 public import Complexitylib.Models.RoseTreeMachine.Prog
 
 /-!
diff --git a/Complexitylib/Models/RoseTreeMachine/Prog.lean b/Complexitylib/Models/RoseTreeMachine/Prog.lean
index 73adbc2e..6af0b6f7 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