diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
index 477ab60b1..2e1c76a98 100644
--- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
+++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
@@ -9,6 +9,7 @@ module
 public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.RelatesInSteps
 public import Mathlib.Algebra.Polynomial.Eval.Defs
+public import Cslib.Computability.Turing.Encoding
 
 /-!
 # Single-Tape Turing Machines
diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Encoding.lean b/Cslib/Computability/Machines/SingleTapeTuring/Encoding.lean
new file mode 100644
index 000000000..2ad75e4fc
--- /dev/null
+++ b/Cslib/Computability/Machines/SingleTapeTuring/Encoding.lean
@@ -0,0 +1,49 @@
+Here is the exact code for the new file.
+
+You can create a new file named Encoding.lean in the Cslib/Computability/Turing/ directory and copy-paste this directly into it. I've included the standard copyright header that matches the rest of the files in that folder.
+
+Lean
+/-
+Copyright (c) 2026 Silvère Gangloff. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey, Pim Spelier, Daan van Gent
+-/
+
+import Mathlib.Tactic.Basic
+
+/-!
+# Turing Machine Tape Encodings
+
+This file defines the `TapeEncodable` typeclass, which provides a framework
+for encoding arbitrary types onto a Turing machine tape. This allows us to
+define computability for functions on types other than just `List Symbol`.
+-/
+
+namespace Turing
+
+variable {Symbol : Type}
+
+/-- 
+A typeclass for types that can be encoded onto a Turing machine tape.
+Provides a canonical way to translate back and forth between a type `α` 
+and a `List Symbol`, alongside a proof that decoding an encoded value succeeds.
+-/
+class TapeEncodable (α : Type) (Symbol : Type) where
+  /-- Translates the type into a tape-compatible list of symbols -/
+  encode : α → List Symbol
+  /-- Attempts to parse a list of symbols back into the type -/
+  decode : List Symbol → Option α
+  /-- Proof that decoding a freshly encoded value yields the original value -/
+  decode_encode_eq : ∀ (a : α), decode (encode a) = some a
+
+/-- 
+The trivial encoding for `List Symbol` itself. 
+This ensures backward compatibility with machines that already operate 
+directly on tape strings.
+-/
+instance : TapeEncodable (List Symbol) Symbol where
+  encode := id
+  decode := some
+  decode_encode_eq _ := rfl
+
+end Turing