diff --git a/Complexitylib/Classes.lean b/Complexitylib/Classes.lean
index 16b608d..40e2844 100644
--- a/Complexitylib/Classes.lean
+++ b/Complexitylib/Classes.lean
@@ -10,3 +10,5 @@ import Complexitylib.Classes.L
 import Complexitylib.Classes.Exponential
 import Complexitylib.Classes.DTISP
 import Complexitylib.Classes.Containments
+import Complexitylib.Classes.BitEncodable
+import Complexitylib.Classes.PPTComputable
diff --git a/Complexitylib/Classes/BitEncodable.lean b/Complexitylib/Classes/BitEncodable.lean
new file mode 100644
index 0000000..d5756cc
--- /dev/null
+++ b/Complexitylib/Classes/BitEncodable.lean
@@ -0,0 +1,61 @@
+import Complexitylib.Classes.Pairing
+
+/-!
+# Bit-string encoding typeclass
+
+`BitEncodable α` provides a specification-level mapping between a type `α` and `List Bool`,
+used to state that a Turing machine's bit-string I/O corresponds to a Lean function operating
+on abstract types. The encoding carries **no computational obligation** — it is purely a
+correspondence used in the *statements* of PPT predicates, not in any executed code.
+
+## Main definitions
+
+- `BitEncodable` — typeclass with `encode : α → List Bool`, `decode : List Bool → α`,
+  and a roundtrip proof
+- Instances for `Unit`, `List Bool`, `Prod`, `Option`
+-/
+
+/-- Specification-level encoding of a type as bit strings.
+    Used to relate Turing machine I/O to Lean functions on abstract types.
+    The `decode` function is total: it returns a default value for invalid inputs.
+    Only the roundtrip property `decode (encode a) = a` is required. -/
+class BitEncodable (α : Type) where
+  /-- Encode a value as a bit string. -/
+  encode : α → List Bool
+  /-- Decode a bit string to a value. Returns a default for invalid inputs. -/
+  decode : List Bool → α
+  /-- Decoding an encoded value recovers the original. -/
+  roundtrip : ∀ a, decode (encode a) = a
+
+namespace BitEncodable
+
+instance unit : BitEncodable Unit where
+  encode _ := []
+  decode _ := ()
+  roundtrip _ := rfl
+
+instance listBool : BitEncodable (List Bool) where
+  encode := id
+  decode := id
+  roundtrip _ := rfl
+
+/-- Encode `Option (List Bool)` as a bit string: `none ↦ [false]`,
+    `some x ↦ true :: x`. -/
+instance optionListBool : BitEncodable (Option (List Bool)) where
+  encode
+    | none => [false]
+    | some x => true :: x
+  decode
+    | [] => none
+    | false :: _ => none
+    | true :: x => some x
+  roundtrip a := by cases a <;> simp
+
+instance prod [BitEncodable α] [BitEncodable β] : BitEncodable (α × β) where
+  encode := fun (a, b) => pair (BitEncodable.encode a) (BitEncodable.encode b)
+  decode := fun bits =>
+    let (l, r) := unpair bits
+    (BitEncodable.decode l, BitEncodable.decode r)
+  roundtrip := fun (a, b) => by simp [unpair_pair, BitEncodable.roundtrip]
+
+end BitEncodable
diff --git a/Complexitylib/Classes/PPTComputable.lean b/Complexitylib/Classes/PPTComputable.lean
new file mode 100644
index 0000000..19b8869
--- /dev/null
+++ b/Complexitylib/Classes/PPTComputable.lean
@@ -0,0 +1,33 @@
+import Complexitylib.Models.TuringMachine
+import Complexitylib.Asymptotics
+import Mathlib.Probability.ProbabilityMassFunction.Basic
+
+/-!
+# PPT-computable randomized functions
+
+This file defines `PPTComputable`, a predicate asserting that a randomized function
+`List Bool → PMF (List Bool)` is computable by a probabilistic polynomial-time
+Turing machine. This bridges the gap between Lean-level probabilistic functions
+(using `PMF`) and the NTM computation model (using `outputCount`).
+
+## Main definitions
+
+- `PPTComputable` — a randomized function is PPT-computable if there exists a PPT NTM
+  whose output distribution matches the function on all inputs
+-/
+
+open Complexity
+
+/-- A randomized function `f : List Bool → PMF (List Bool)` is **PPT-computable**
+    if there exists a PPT NTM whose output distribution matches `f` on all inputs.
+
+    The output distribution of the NTM with time bound `T` is given by
+    `outputCount x T y / 2^T`, which must equal `(f x) y` for all inputs `x`
+    and outputs `y`. The time bound `T` must be polynomial: `T =O (· ^ d)`
+    for some degree `d`. -/
+def PPTComputable (f : List Bool → PMF (List Bool)) : Prop :=
+  ∃ (k : ℕ) (tm : NTM k) (T : ℕ → ℕ) (d : ℕ),
+    T =O (· ^ d) ∧
+    tm.AllPathsHaltIn T ∧
+    ∀ x y,
+      (↑(tm.outputCount x (T x.length) y) : ENNReal) / ↑(2 ^ (T x.length)) = (f x) y
diff --git a/Complexitylib/Classes/Pairing.lean b/Complexitylib/Classes/Pairing.lean
index a9be014..28d3110 100644
--- a/Complexitylib/Classes/Pairing.lean
+++ b/Complexitylib/Classes/Pairing.lean
@@ -17,14 +17,38 @@ search-problem classes.
 def pair (x y : List Bool) : List Bool :=
   (x.flatMap fun b => [b, b]) ++ [false, true] ++ y
 
-private theorem pair_nil_eq (y : List Bool) :
+@[simp]
+theorem pair_nil_eq (y : List Bool) :
     pair [] y = false :: true :: y := by
   simp [pair]
 
-private theorem pair_cons_eq (b : Bool) (x y : List Bool) :
+@[simp]
+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]
 
+/-- Decode a paired binary string back into two components.
+    Left inverse of `pair`: `unpair (pair x y) = (x, y)`.
+    Returns `([], [])` for strings not in the image of `pair`. -/
+def unpair : List Bool → List Bool × List Bool
+  | false :: false :: rest =>
+    let (x, y) := unpair rest
+    (false :: x, y)
+  | true :: true :: rest =>
+    let (x, y) := unpair rest
+    (true :: x, y)
+  | false :: true :: rest => ([], rest)
+  | _ => ([], [])
+
+/-- `unpair` is a left inverse of `pair`. -/
+@[simp]
+theorem unpair_pair (x y : List Bool) : unpair (pair x y) = (x, y) := by
+  induction x with
+  | nil => rfl
+  | cons b x' ih =>
+    rw [pair_cons_eq]
+    cases b <;> simp only [unpair, ih]
+
 /-- `pair` is injective: if `pair x₁ y₁ = pair x₂ y₂` then `x₁ = x₂` and `y₁ = y₂`. -/
 theorem pair_injective {x₁ x₂ : List Bool} {y₁ y₂ : List Bool}
     (h : pair x₁ y₁ = pair x₂ y₂) : x₁ = x₂ ∧ y₁ = y₂ := by