From 55f8583db954e289afa94a8eff768ebc2f1bf419 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Sep 2026 10:45:53 -0700
Subject: [PATCH 1/8] initial draft

---
 Cslib.lean                                    |   2 +
 .../FunctionAlgebras/Cobham/Defs.lean         | 184 ++++++++++++++++++
 .../FunctionAlgebras/Cobham/PolyTime.lean     |  38 ++++
 CslibTests.lean                               |   1 +
 CslibTests/Cobham.lean                        |  65 +++++++
 references.bib                                |  11 ++
 6 files changed, 301 insertions(+)
 create mode 100644 Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
 create mode 100644 Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
 create mode 100644 CslibTests/Cobham.lean

diff --git a/Cslib.lean b/Cslib.lean
index 8cfe47e01..03b3c8cf1 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -44,6 +44,8 @@ public import Cslib.Computability.Distributed.FLP.Impossibility
 public import Cslib.Computability.Distributed.FLP.OnePseudoConsensus
 public import Cslib.Computability.Distributed.FLP.PseudoConsensus
 public import Cslib.Computability.Distributed.FLP.ZeroConsensus
+public import Cslib.Computability.FunctionAlgebras.Cobham.Defs
+public import Cslib.Computability.FunctionAlgebras.Cobham.PolyTime
 public import Cslib.Computability.Languages.Congruences.BuchiCongruence
 public import Cslib.Computability.Languages.Congruences.RightCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero
diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
new file mode 100644
index 000000000..be206a5c9
--- /dev/null
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -0,0 +1,184 @@
+/-
+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 Cslib.Init
+public import Mathlib.Data.Fin.Tuple.Basic
+
+/-!
+# Cobham's function algebra
+
+This file defines Cobham's machine-independent characterization
+of the polynomial-time computable functions
+[Cobham, *The intrinsic computational difficulty of functions*][Cobham1965],
+as a model of computation on strings `List Symbol` over an arbitrary alphabet `Symbol`:
+the smallest class of functions `(Fin n → List Symbol) → List Symbol` containing
+the projections, the empty string, the symbol successors, and the smash functions,
+and closed under composition and limited recursion on notation.
+
+The algebra is presented as a syntax `Cobham Symbol n` of terms denoting `n`-ary string functions,
+with semantics given by `Cobham.eval`.
+Cobham's side condition on recursion — that the recursively defined
+function be length-bounded by another function of the class — is not part of the syntax:
+it is the structural predicate `Cobham.Limited`,
+and `CobhamFP` collects the unary functions denoted by limited terms.
+
+The functions are multi-arity (indexed by `Fin n` argument vectors) because limited
+recursion on notation inherently produces functions of higher arity.
+
+## Main definitions
+
+- `Cslib.Cobham` — the terms of Cobham's function algebra over an alphabet `Symbol`
+- `Cslib.Cobham.recNotation` — the recursion-on-notation combinator on string functions
+- `Cslib.Cobham.eval` — the string function denoted by a term
+- `Cslib.Cobham.Limited` — the side condition that every recursion in a term is bounded
+  by its bounding term
+- `Cslib.CobhamFP` — the unary string functions denoted by limited terms
+
+## Design notes
+
+We work over strings of arbitrary `Symbol` type, rather than binary natural numbers.
+
+The bound in `Cobham.boundedRec` follows Cobham's original formulation: the recursively
+defined function must be length-bounded by another function of the class
+(rather than by an external polynomial).
+Together with `smash` and the successors this realizes exactly the polynomial length bounds,
+which is what makes the class no larger than the polynomial-time computable functions.
+
+## TODO
+
+* Prove the limited Cobham functions are exactly the polynomial-time computable functions.
+
+## References
+
+* [A. Cobham, *The intrinsic computational difficulty of functions*][Cobham1965]
+-/
+
+@[expose] public section
+
+universe u
+
+namespace Cslib
+
+variable {Symbol : Type u}
+
+/-- **Terms of Cobham's function algebra** over the alphabet `Symbol`. A term of type
+`Cobham Symbol n` denotes an `n`-ary function on strings `List Symbol` (see
+`Cobham.eval`): the projections, the empty string, the symbol successors `x ↦ a :: x`,
+and the smash functions, closed under composition and recursion on notation.
+
+In `boundedRec g h j`, the term `j` is the *bound* of the recursion: Cobham's side
+condition that the recursion be length-bounded by `j` is the predicate `Cobham.Limited`. -/
+inductive Cobham (Symbol : Type u) : ℕ → Type u
+  /-- The `i`-th projection. -/
+  | proj {n : ℕ} (i : Fin n) : Cobham Symbol n
+  /-- The empty-string constant (at every arity). -/
+  | empty {n : ℕ} : Cobham Symbol n
+  /-- The successor `x ↦ a :: x` for the symbol `a`. -/
+  | cons (a : Symbol) : Cobham Symbol 1
+  /-- The smash function returning a list of `a` of length |x₀| * |x₁|. -/
+  | smash (a : Symbol) : Cobham Symbol 2
+  /-- Composition of an `m`-ary term with `m` terms of arity `n`. -/
+  | comp {m n : ℕ} (f : Cobham Symbol m) (gs : Fin m → Cobham Symbol n) : Cobham Symbol n
+  /-- Limited recursion on notation on the first argument, with base case `g`, step
+  `h a` for each symbol `a`, and bounding term `j`. -/
+  | boundedRec {n : ℕ} (g : Cobham Symbol n) (h : Symbol → Cobham Symbol (n + 2))
+      (j : Cobham Symbol (n + 1)) : Cobham Symbol (n + 1)
+
+namespace Cobham
+
+/-- **Recursion on notation**: the string analogue of primitive recursion, recursing on
+the symbol structure of the first argument.
+
+`recNotation g h v x` computes `g v` when `x` is empty, and on `a :: x` applies the
+step function `h a` selected by the symbol `a` to the argument vector consisting of the
+tail `x`, the recursive value on the tail, and the parameters `v`. -/
+def recNotation {n : ℕ} (g : (Fin n → List Symbol) → List Symbol)
+    (h : Symbol → (Fin (n + 2) → List Symbol) → List Symbol) (v : Fin n → List Symbol) :
+    List Symbol → List Symbol
+  | [] => g v
+  | a :: x => h a (Fin.cons x (Fin.cons (recNotation g h v x) v))
+
+@[simp] theorem recNotation_nil {n : ℕ} (g : (Fin n → List Symbol) → List Symbol)
+    (h : Symbol → (Fin (n + 2) → List Symbol) → List Symbol) (v : Fin n → List Symbol) :
+    recNotation g h v [] = g v := rfl
+
+@[simp] theorem recNotation_cons {n : ℕ} (g : (Fin n → List Symbol) → List Symbol)
+    (h : Symbol → (Fin (n + 2) → List Symbol) → List Symbol) (v : Fin n → List Symbol)
+    (a : Symbol) (x : List Symbol) :
+    recNotation g h v (a :: x) = h a (Fin.cons x (Fin.cons (recNotation g h v x) v)) := rfl
+
+/-- The string function denoted by a term. The bound `j` of a `boundedRec` plays no role
+in evaluation; it is checked by `Cobham.Limited`. -/
+def eval : {n : ℕ} → Cobham Symbol n → (Fin n → List Symbol) → List Symbol
+  | _, proj i, v => v i
+  | _, empty, _ => []
+  | _, cons a, v => a :: v 0
+  | _, smash a, v => List.replicate ((v 0).length * (v 1).length) a
+  | _, comp f gs, v => f.eval fun i => (gs i).eval v
+  | _, boundedRec g h _, v => recNotation g.eval (fun a => (h a).eval) (Fin.tail v) (v 0)
+
+@[simp] theorem eval_proj {n : ℕ} (i : Fin n) (v : Fin n → List Symbol) :
+    (proj i).eval v = v i := rfl
+
+@[simp] theorem eval_empty {n : ℕ} (v : Fin n → List Symbol) :
+    empty.eval v = [] := rfl
+
+@[simp] theorem eval_cons (a : Symbol) (v : Fin 1 → List Symbol) :
+    (cons a).eval v = a :: v 0 := rfl
+
+@[simp] theorem eval_smash (a : Symbol) (v : Fin 2 → List Symbol) :
+    (smash a).eval v = List.replicate ((v 0).length * (v 1).length) a := rfl
+
+@[simp] theorem eval_comp {m n : ℕ} (f : Cobham Symbol m) (gs : Fin m → Cobham Symbol n)
+    (v : Fin n → List Symbol) : (comp f gs).eval v = f.eval fun i => (gs i).eval v := rfl
+
+@[simp] theorem eval_boundedRec {n : ℕ} (g : Cobham Symbol n) (h : Symbol → Cobham Symbol (n + 2))
+    (j : Cobham Symbol (n + 1)) (v : Fin (n + 1) → List Symbol) :
+    (boundedRec g h j).eval v = recNotation g.eval (fun a => (h a).eval) (Fin.tail v) (v 0) :=
+  rfl
+
+/-- A term is **limited** when every recursion in it is limited in Cobham's sense: the
+result of each `boundedRec g h j` is length-bounded, uniformly in the arguments, by its
+bounding term `j`. -/
+def Limited : {n : ℕ} → Cobham Symbol n → Prop
+  | _, proj _ => True
+  | _, empty => True
+  | _, cons _ => True
+  | _, smash _ => True
+  | _, comp f gs => f.Limited ∧ ∀ i, (gs i).Limited
+  | _, boundedRec g h j =>
+      g.Limited ∧ (∀ a, (h a).Limited) ∧ j.Limited ∧
+        ∀ v x, (recNotation g.eval (fun a => (h a).eval) v x).length ≤
+          (j.eval (Fin.cons x v)).length
+
+@[simp] theorem limited_proj {n : ℕ} (i : Fin n) : (proj i : Cobham Symbol n).Limited := trivial
+
+@[simp] theorem limited_empty {n : ℕ} : (empty : Cobham Symbol n).Limited := trivial
+
+@[simp] theorem limited_cons (a : Symbol) : (cons a).Limited := trivial
+
+@[simp] theorem limited_smash (a : Symbol) : (smash a).Limited := trivial
+
+@[simp] theorem limited_comp {m n : ℕ} (f : Cobham Symbol m) (gs : Fin m → Cobham Symbol n) :
+    (comp f gs).Limited ↔ f.Limited ∧ ∀ i, (gs i).Limited := Iff.rfl
+
+@[simp] theorem limited_boundedRec {n : ℕ} (g : Cobham Symbol n)
+    (h : Symbol → Cobham Symbol (n + 2)) (j : Cobham Symbol (n + 1)) :
+    (boundedRec g h j).Limited ↔
+      g.Limited ∧ (∀ a, (h a).Limited) ∧ j.Limited ∧
+        ∀ v x, (recNotation g.eval (fun a => (h a).eval) v x).length ≤
+          (j.eval (Fin.cons x v)).length := Iff.rfl
+
+end Cobham
+
+/-- The unary fragment of Cobham's function algebra over `Symbol`: the string functions
+denoted by limited unary terms. By Cobham's theorem [Cobham1965], this machine-independent
+class is exactly the polynomial-time computable functions. -/
+def CobhamFP (Symbol : Type u) : Set (List Symbol → List Symbol) :=
+  {f | ∃ c : Cobham Symbol 1, c.Limited ∧ ∀ x, c.eval (fun _ => x) = f x}
+
+end Cslib
diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean b/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
new file mode 100644
index 000000000..46776aecd
--- /dev/null
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
@@ -0,0 +1,38 @@
+/-
+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 Cslib.Computability.FunctionAlgebras.Cobham.Defs
+public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+
+/-!
+# Cobham's theorem
+
+Cobham's theorem [Cobham1965] states that the functions of Cobham's algebra
+(`Cslib.CobhamFP`) are exactly the functions computable in polynomial time by a Turing
+machine (`Cslib.Turing.SingleTapeTM.PolyTimeComputable`).
+
+## References
+
+* [A. Cobham, *The intrinsic computational difficulty of functions*][Cobham1965]
+-/
+
+-- A `proof_wanted` adds no declaration to the module, so this file has nothing public.
+set_option linter.privateModule false
+
+@[expose] public section
+
+namespace Cslib
+
+open Turing.SingleTapeTM
+
+/-- **Cobham's theorem**: a string function is in Cobham's algebra if and only if it is
+computable in polynomial time by a single-tape Turing machine. -/
+proof_wanted CobhamFP_iff_polyTimeComputable {Symbol : Type} [Inhabited Symbol]
+    [Fintype Symbol] (f : List Symbol → List Symbol) :
+    f ∈ CobhamFP Symbol ↔ Nonempty (PolyTimeComputable f)
+
+end Cslib
diff --git a/CslibTests.lean b/CslibTests.lean
index f7b53299f..029b20f14 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -3,6 +3,7 @@ import CslibTests.CCS
 import CslibTests.CCS.VendingMachine
 import CslibTests.CLL
 import CslibTests.Circuits
+import CslibTests.Cobham
 import CslibTests.Commitment
 import CslibTests.Congruence
 import CslibTests.DFA
diff --git a/CslibTests/Cobham.lean b/CslibTests/Cobham.lean
new file mode 100644
index 000000000..59f08baff
--- /dev/null
+++ b/CslibTests/Cobham.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+
+import Cslib.Computability.FunctionAlgebras.Cobham.Defs
+import Mathlib.Data.Fin.VecNotation
+
+/-! # Cobham's function algebra tests
+
+These tests evaluate a few terms of Cobham's algebra, over the binary alphabet and a
+three-symbol alphabet, and check membership of some simple unary functions in `CobhamFP`,
+including one built by limited recursion on notation.
+-/
+
+namespace CslibTests.Cobham
+
+open Cslib Cslib.Cobham
+
+/-! ## Evaluation -/
+
+/-- Recursion on notation counting the symbols of its argument in unary, bounded by the
+successor `x ↦ true :: x`. -/
+private def unaryLength : Cobham Bool 1 :=
+  boundedRec empty (fun _ => comp (cons true) fun _ => proj 1) (cons true)
+
+example : unaryLength.eval ![[true, false, true]] = [true, true, true] := by decide
+
+example : unaryLength.eval ![[]] = [] := by decide
+
+example : (comp (cons true) fun _ => cons false).eval ![[true]] = [true, false, true] := by
+  decide
+
+example : (smash (2 : Fin 3)).eval ![[0, 1], [0, 0, 0]] = List.replicate 6 2 := by decide
+
+/-! ## Membership in the unary class -/
+
+example : (fun x => x) ∈ CobhamFP Bool := ⟨proj 0, trivial, fun _ => rfl⟩
+
+example : (fun x => true :: false :: x) ∈ CobhamFP Bool :=
+  ⟨comp (cons true) fun _ => cons false, by simp, fun _ => rfl⟩
+
+example : (fun x : List (Fin 3) => List.replicate (x.length * x.length) 0) ∈ CobhamFP (Fin 3) :=
+  ⟨comp (smash 0) fun _ => proj 0, by simp, fun _ => rfl⟩
+
+/-- The recursion in `unaryLength` computes the unary length, for any parameter vector. -/
+private theorem unaryLength_rec (v : Fin 0 → List Bool) (x : List Bool) :
+    recNotation empty.eval (fun _ => (comp (cons true) fun _ => proj 1).eval) v x =
+      List.replicate x.length true := by
+  induction x with
+  | nil => rfl
+  | cons b x ih => simp [ih, List.replicate_succ]
+
+/-- Unary length is in the class: its bound `x ↦ true :: x` is a limited term, and the
+recursion is length-bounded by it. -/
+example : (fun x : List Bool => List.replicate x.length true) ∈ CobhamFP Bool := by
+  refine ⟨unaryLength, ?_, fun x => ?_⟩
+  · simp only [unaryLength, limited_boundedRec, limited_empty, limited_comp, limited_cons,
+      limited_proj, implies_true, true_and]
+    intro v x
+    simp [unaryLength_rec]
+  · simp [unaryLength, unaryLength_rec]
+
+end CslibTests.Cobham
diff --git a/references.bib b/references.bib
index 72051ea9c..f1d47ef87 100644
--- a/references.bib
+++ b/references.bib
@@ -406,6 +406,17 @@ @incollection{ Thomas1990
   year         = {1990}
 }
 
+@incollection{ Cobham1965,
+  author       = {Cobham, Alan},
+  editor       = {Bar-Hillel, Yehoshua},
+  title        = {The intrinsic computational difficulty of functions},
+  booktitle    = {Logic, Methodology and Philosophy of Science: Proceedings of the 1964 International Congress},
+  pages        = {24--30},
+  publisher    = {North-Holland},
+  address      = {Amsterdam},
+  year         = {1965}
+}
+
 @book{            Cutland1980,
   author       = {Cutland, Nigel J.},
   title        = {Computability: An Introduction to Recursive Function Theory},

From f9e19f3115ea392b7366930d773483ebd2f1a28f Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Sep 2026 11:03:21 -0700
Subject: [PATCH 2/8] naming things

---
 .../FunctionAlgebras/Cobham/Defs.lean         | 78 ++++++++++---------
 1 file changed, 41 insertions(+), 37 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index be206a5c9..d880d11ce 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -70,8 +70,9 @@ variable {Symbol : Type u}
 `Cobham.eval`): the projections, the empty string, the symbol successors `x ↦ a :: x`,
 and the smash functions, closed under composition and recursion on notation.
 
-In `boundedRec g h j`, the term `j` is the *bound* of the recursion: Cobham's side
-condition that the recursion be length-bounded by `j` is the predicate `Cobham.Limited`. -/
+In `boundedRec base step bound`, Cobham's side condition that the recursion be
+length-bounded by `bound` is not enforced by the syntax; it is the predicate
+`Cobham.Limited`. -/
 inductive Cobham (Symbol : Type u) : ℕ → Type u
   /-- The `i`-th projection. -/
   | proj {n : ℕ} (i : Fin n) : Cobham Symbol n
@@ -83,43 +84,45 @@ inductive Cobham (Symbol : Type u) : ℕ → Type u
   | smash (a : Symbol) : Cobham Symbol 2
   /-- Composition of an `m`-ary term with `m` terms of arity `n`. -/
   | comp {m n : ℕ} (f : Cobham Symbol m) (gs : Fin m → Cobham Symbol n) : Cobham Symbol n
-  /-- Limited recursion on notation on the first argument, with base case `g`, step
-  `h a` for each symbol `a`, and bounding term `j`. -/
-  | boundedRec {n : ℕ} (g : Cobham Symbol n) (h : Symbol → Cobham Symbol (n + 2))
-      (j : Cobham Symbol (n + 1)) : Cobham Symbol (n + 1)
+  /-- Limited recursion on notation on the first argument, with the given base case, a
+  step `step a` for each symbol `a`, and the given bounding term. -/
+  | boundedRec {n : ℕ} (base : Cobham Symbol n) (step : Symbol → Cobham Symbol (n + 2))
+      (bound : Cobham Symbol (n + 1)) : Cobham Symbol (n + 1)
 
 namespace Cobham
 
 /-- **Recursion on notation**: the string analogue of primitive recursion, recursing on
 the symbol structure of the first argument.
 
-`recNotation g h v x` computes `g v` when `x` is empty, and on `a :: x` applies the
-step function `h a` selected by the symbol `a` to the argument vector consisting of the
+`recNotation base step v x` computes `base v` when `x` is empty, and on `a :: x` applies the
+step function `step a` selected by the symbol `a` to the argument vector consisting of the
 tail `x`, the recursive value on the tail, and the parameters `v`. -/
-def recNotation {n : ℕ} (g : (Fin n → List Symbol) → List Symbol)
-    (h : Symbol → (Fin (n + 2) → List Symbol) → List Symbol) (v : Fin n → List Symbol) :
+def recNotation {n : ℕ} (base : (Fin n → List Symbol) → List Symbol)
+    (step : Symbol → (Fin (n + 2) → List Symbol) → List Symbol) (v : Fin n → List Symbol) :
     List Symbol → List Symbol
-  | [] => g v
-  | a :: x => h a (Fin.cons x (Fin.cons (recNotation g h v x) v))
+  | [] => base v
+  | a :: x => step a (Fin.cons x (Fin.cons (recNotation base step v x) v))
 
-@[simp] theorem recNotation_nil {n : ℕ} (g : (Fin n → List Symbol) → List Symbol)
-    (h : Symbol → (Fin (n + 2) → List Symbol) → List Symbol) (v : Fin n → List Symbol) :
-    recNotation g h v [] = g v := rfl
+@[simp] theorem recNotation_nil {n : ℕ} (base : (Fin n → List Symbol) → List Symbol)
+    (step : Symbol → (Fin (n + 2) → List Symbol) → List Symbol) (v : Fin n → List Symbol) :
+    recNotation base step v [] = base v := rfl
 
-@[simp] theorem recNotation_cons {n : ℕ} (g : (Fin n → List Symbol) → List Symbol)
-    (h : Symbol → (Fin (n + 2) → List Symbol) → List Symbol) (v : Fin n → List Symbol)
+@[simp] theorem recNotation_cons {n : ℕ} (base : (Fin n → List Symbol) → List Symbol)
+    (step : Symbol → (Fin (n + 2) → List Symbol) → List Symbol) (v : Fin n → List Symbol)
     (a : Symbol) (x : List Symbol) :
-    recNotation g h v (a :: x) = h a (Fin.cons x (Fin.cons (recNotation g h v x) v)) := rfl
+    recNotation base step v (a :: x) =
+      step a (Fin.cons x (Fin.cons (recNotation base step v x) v)) := rfl
 
-/-- The string function denoted by a term. The bound `j` of a `boundedRec` plays no role
-in evaluation; it is checked by `Cobham.Limited`. -/
+/-- The string function denoted by a term. The bounding term of a `boundedRec` plays no
+role in evaluation; it is checked by `Cobham.Limited`. -/
 def eval : {n : ℕ} → Cobham Symbol n → (Fin n → List Symbol) → List Symbol
   | _, proj i, v => v i
   | _, empty, _ => []
   | _, cons a, v => a :: v 0
   | _, smash a, v => List.replicate ((v 0).length * (v 1).length) a
   | _, comp f gs, v => f.eval fun i => (gs i).eval v
-  | _, boundedRec g h _, v => recNotation g.eval (fun a => (h a).eval) (Fin.tail v) (v 0)
+  | _, boundedRec base step _, v =>
+      recNotation base.eval (fun a => (step a).eval) (Fin.tail v) (v 0)
 
 @[simp] theorem eval_proj {n : ℕ} (i : Fin n) (v : Fin n → List Symbol) :
     (proj i).eval v = v i := rfl
@@ -136,24 +139,25 @@ def eval : {n : ℕ} → Cobham Symbol n → (Fin n → List Symbol) → List Sy
 @[simp] theorem eval_comp {m n : ℕ} (f : Cobham Symbol m) (gs : Fin m → Cobham Symbol n)
     (v : Fin n → List Symbol) : (comp f gs).eval v = f.eval fun i => (gs i).eval v := rfl
 
-@[simp] theorem eval_boundedRec {n : ℕ} (g : Cobham Symbol n) (h : Symbol → Cobham Symbol (n + 2))
-    (j : Cobham Symbol (n + 1)) (v : Fin (n + 1) → List Symbol) :
-    (boundedRec g h j).eval v = recNotation g.eval (fun a => (h a).eval) (Fin.tail v) (v 0) :=
-  rfl
+@[simp] theorem eval_boundedRec {n : ℕ} (base : Cobham Symbol n)
+    (step : Symbol → Cobham Symbol (n + 2)) (bound : Cobham Symbol (n + 1))
+    (v : Fin (n + 1) → List Symbol) :
+    (boundedRec base step bound).eval v =
+      recNotation base.eval (fun a => (step a).eval) (Fin.tail v) (v 0) := rfl
 
 /-- A term is **limited** when every recursion in it is limited in Cobham's sense: the
-result of each `boundedRec g h j` is length-bounded, uniformly in the arguments, by its
-bounding term `j`. -/
+result of each `boundedRec base step bound` is length-bounded, uniformly in the arguments,
+by `bound`. -/
 def Limited : {n : ℕ} → Cobham Symbol n → Prop
   | _, proj _ => True
   | _, empty => True
   | _, cons _ => True
   | _, smash _ => True
   | _, comp f gs => f.Limited ∧ ∀ i, (gs i).Limited
-  | _, boundedRec g h j =>
-      g.Limited ∧ (∀ a, (h a).Limited) ∧ j.Limited ∧
-        ∀ v x, (recNotation g.eval (fun a => (h a).eval) v x).length ≤
-          (j.eval (Fin.cons x v)).length
+  | _, boundedRec base step bound =>
+      base.Limited ∧ (∀ a, (step a).Limited) ∧ bound.Limited ∧
+        ∀ v x, (recNotation base.eval (fun a => (step a).eval) v x).length ≤
+          (bound.eval (Fin.cons x v)).length
 
 @[simp] theorem limited_proj {n : ℕ} (i : Fin n) : (proj i : Cobham Symbol n).Limited := trivial
 
@@ -166,12 +170,12 @@ def Limited : {n : ℕ} → Cobham Symbol n → Prop
 @[simp] theorem limited_comp {m n : ℕ} (f : Cobham Symbol m) (gs : Fin m → Cobham Symbol n) :
     (comp f gs).Limited ↔ f.Limited ∧ ∀ i, (gs i).Limited := Iff.rfl
 
-@[simp] theorem limited_boundedRec {n : ℕ} (g : Cobham Symbol n)
-    (h : Symbol → Cobham Symbol (n + 2)) (j : Cobham Symbol (n + 1)) :
-    (boundedRec g h j).Limited ↔
-      g.Limited ∧ (∀ a, (h a).Limited) ∧ j.Limited ∧
-        ∀ v x, (recNotation g.eval (fun a => (h a).eval) v x).length ≤
-          (j.eval (Fin.cons x v)).length := Iff.rfl
+@[simp] theorem limited_boundedRec {n : ℕ} (base : Cobham Symbol n)
+    (step : Symbol → Cobham Symbol (n + 2)) (bound : Cobham Symbol (n + 1)) :
+    (boundedRec base step bound).Limited ↔
+      base.Limited ∧ (∀ a, (step a).Limited) ∧ bound.Limited ∧
+        ∀ v x, (recNotation base.eval (fun a => (step a).eval) v x).length ≤
+          (bound.eval (Fin.cons x v)).length := Iff.rfl
 
 end Cobham
 

From f191e530a5b3757dad67cd9bb89e4e522b82c3c1 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Sep 2026 11:17:35 -0700
Subject: [PATCH 3/8] arguments before colon

---
 .../FunctionAlgebras/Cobham/Defs.lean         | 29 ++++++++++---------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index d880d11ce..dff709147 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -115,13 +115,14 @@ def recNotation {n : ℕ} (base : (Fin n → List Symbol) → List Symbol)
 
 /-- The string function denoted by a term. The bounding term of a `boundedRec` plays no
 role in evaluation; it is checked by `Cobham.Limited`. -/
-def eval : {n : ℕ} → Cobham Symbol n → (Fin n → List Symbol) → List Symbol
-  | _, proj i, v => v i
-  | _, empty, _ => []
-  | _, cons a, v => a :: v 0
-  | _, smash a, v => List.replicate ((v 0).length * (v 1).length) a
-  | _, comp f gs, v => f.eval fun i => (gs i).eval v
-  | _, boundedRec base step _, v =>
+def eval {n : ℕ} (t : Cobham Symbol n) (v : Fin n → List Symbol) : List Symbol :=
+  match t with
+  | proj i => v i
+  | empty => []
+  | cons a => a :: v 0
+  | smash a => List.replicate ((v 0).length * (v 1).length) a
+  | comp f gs => f.eval fun i => (gs i).eval v
+  | boundedRec base step _ =>
       recNotation base.eval (fun a => (step a).eval) (Fin.tail v) (v 0)
 
 @[simp] theorem eval_proj {n : ℕ} (i : Fin n) (v : Fin n → List Symbol) :
@@ -148,13 +149,13 @@ def eval : {n : ℕ} → Cobham Symbol n → (Fin n → List Symbol) → List Sy
 /-- A term is **limited** when every recursion in it is limited in Cobham's sense: the
 result of each `boundedRec base step bound` is length-bounded, uniformly in the arguments,
 by `bound`. -/
-def Limited : {n : ℕ} → Cobham Symbol n → Prop
-  | _, proj _ => True
-  | _, empty => True
-  | _, cons _ => True
-  | _, smash _ => True
-  | _, comp f gs => f.Limited ∧ ∀ i, (gs i).Limited
-  | _, boundedRec base step bound =>
+def Limited {n : ℕ} : Cobham Symbol n → Prop
+  | proj _ => True
+  | empty => True
+  | cons _ => True
+  | smash _ => True
+  | comp f gs => f.Limited ∧ ∀ i, (gs i).Limited
+  | boundedRec base step bound =>
       base.Limited ∧ (∀ a, (step a).Limited) ∧ bound.Limited ∧
         ∀ v x, (recNotation base.eval (fun a => (step a).eval) v x).length ≤
           (bound.eval (Fin.cons x v)).length

From 10c83605da73e3eb049da8302008b0eb84ebbe21 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Sep 2026 21:26:56 -0700
Subject: [PATCH 4/8] move definition

---
 Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean    | 6 ------
 .../Computability/FunctionAlgebras/Cobham/PolyTime.lean  | 9 ++++++---
 2 files changed, 6 insertions(+), 9 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index dff709147..fd4bf8009 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -180,10 +180,4 @@ def Limited {n : ℕ} : Cobham Symbol n → Prop
 
 end Cobham
 
-/-- The unary fragment of Cobham's function algebra over `Symbol`: the string functions
-denoted by limited unary terms. By Cobham's theorem [Cobham1965], this machine-independent
-class is exactly the polynomial-time computable functions. -/
-def CobhamFP (Symbol : Type u) : Set (List Symbol → List Symbol) :=
-  {f | ∃ c : Cobham Symbol 1, c.Limited ∧ ∀ x, c.eval (fun _ => x) = f x}
-
 end Cslib
diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean b/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
index 46776aecd..82fe74b9d 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
@@ -20,13 +20,16 @@ machine (`Cslib.Turing.SingleTapeTM.PolyTimeComputable`).
 * [A. Cobham, *The intrinsic computational difficulty of functions*][Cobham1965]
 -/
 
--- A `proof_wanted` adds no declaration to the module, so this file has nothing public.
-set_option linter.privateModule false
-
 @[expose] public section
 
 namespace Cslib
 
+/-- The unary fragment of Cobham's function algebra over `Symbol`: the string functions
+denoted by limited unary terms. By Cobham's theorem [Cobham1965], this machine-independent
+class is exactly the polynomial-time computable functions. -/
+def CobhamFP (Symbol : Type u) : Set (List Symbol → List Symbol) :=
+  {f | ∃ c : Cobham Symbol 1, c.Limited ∧ ∀ x, c.eval (fun _ => x) = f x}
+
 open Turing.SingleTapeTM
 
 /-- **Cobham's theorem**: a string function is in Cobham's algebra if and only if it is

From a54c6fe61221d16ee572a25847dcc7a3dd468a8a Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Sep 2026 14:00:55 -0700
Subject: [PATCH 5/8] update import

---
 Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean | 1 -
 CslibTests/Cobham.lean                                | 2 +-
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index fd4bf8009..bbf34bdb4 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -36,7 +36,6 @@ recursion on notation inherently produces functions of higher arity.
 - `Cslib.Cobham.eval` — the string function denoted by a term
 - `Cslib.Cobham.Limited` — the side condition that every recursion in a term is bounded
   by its bounding term
-- `Cslib.CobhamFP` — the unary string functions denoted by limited terms
 
 ## Design notes
 
diff --git a/CslibTests/Cobham.lean b/CslibTests/Cobham.lean
index 59f08baff..a5d8df7b9 100644
--- a/CslibTests/Cobham.lean
+++ b/CslibTests/Cobham.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bolton Bailey
 -/
 
-import Cslib.Computability.FunctionAlgebras.Cobham.Defs
+import Cslib.Computability.FunctionAlgebras.Cobham.PolyTime
 import Mathlib.Data.Fin.VecNotation
 
 /-! # Cobham's function algebra tests

From 66aa0d609b644236aefe5be6c9edb78cb40a5d3f Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Sep 2026 14:27:35 -0700
Subject: [PATCH 6/8] style

---
 Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean  |  6 +-----
 .../FunctionAlgebras/Cobham/PolyTime.lean              | 10 ++++++----
 CslibTests/Cobham.lean                                 | 10 +++++-----
 3 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index bbf34bdb4..6aaea13d2 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -24,7 +24,7 @@ with semantics given by `Cobham.eval`.
 Cobham's side condition on recursion — that the recursively defined
 function be length-bounded by another function of the class — is not part of the syntax:
 it is the structural predicate `Cobham.Limited`,
-and `CobhamFP` collects the unary functions denoted by limited terms.
+and `cobhamFP` collects the unary functions denoted by limited terms.
 
 The functions are multi-arity (indexed by `Fin n` argument vectors) because limited
 recursion on notation inherently produces functions of higher arity.
@@ -47,10 +47,6 @@ defined function must be length-bounded by another function of the class
 Together with `smash` and the successors this realizes exactly the polynomial length bounds,
 which is what makes the class no larger than the polynomial-time computable functions.
 
-## TODO
-
-* Prove the limited Cobham functions are exactly the polynomial-time computable functions.
-
 ## References
 
 * [A. Cobham, *The intrinsic computational difficulty of functions*][Cobham1965]
diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean b/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
index 82fe74b9d..8cc37f554 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
@@ -12,7 +12,7 @@ public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
 # Cobham's theorem
 
 Cobham's theorem [Cobham1965] states that the functions of Cobham's algebra
-(`Cslib.CobhamFP`) are exactly the functions computable in polynomial time by a Turing
+(`Cslib.cobhamFP`) are exactly the functions computable in polynomial time by a Turing
 machine (`Cslib.Turing.SingleTapeTM.PolyTimeComputable`).
 
 ## References
@@ -22,20 +22,22 @@ machine (`Cslib.Turing.SingleTapeTM.PolyTimeComputable`).
 
 @[expose] public section
 
+universe u
+
 namespace Cslib
 
 /-- The unary fragment of Cobham's function algebra over `Symbol`: the string functions
 denoted by limited unary terms. By Cobham's theorem [Cobham1965], this machine-independent
 class is exactly the polynomial-time computable functions. -/
-def CobhamFP (Symbol : Type u) : Set (List Symbol → List Symbol) :=
+def cobhamFP (Symbol : Type u) : Set (List Symbol → List Symbol) :=
   {f | ∃ c : Cobham Symbol 1, c.Limited ∧ ∀ x, c.eval (fun _ => x) = f x}
 
 open Turing.SingleTapeTM
 
 /-- **Cobham's theorem**: a string function is in Cobham's algebra if and only if it is
 computable in polynomial time by a single-tape Turing machine. -/
-proof_wanted CobhamFP_iff_polyTimeComputable {Symbol : Type} [Inhabited Symbol]
+proof_wanted cobhamFP_iff_polyTimeComputable {Symbol : Type} [Inhabited Symbol]
     [Fintype Symbol] (f : List Symbol → List Symbol) :
-    f ∈ CobhamFP Symbol ↔ Nonempty (PolyTimeComputable f)
+    f ∈ cobhamFP Symbol ↔ Nonempty (PolyTimeComputable f)
 
 end Cslib
diff --git a/CslibTests/Cobham.lean b/CslibTests/Cobham.lean
index a5d8df7b9..8b3d66d97 100644
--- a/CslibTests/Cobham.lean
+++ b/CslibTests/Cobham.lean
@@ -10,7 +10,7 @@ import Mathlib.Data.Fin.VecNotation
 /-! # Cobham's function algebra tests
 
 These tests evaluate a few terms of Cobham's algebra, over the binary alphabet and a
-three-symbol alphabet, and check membership of some simple unary functions in `CobhamFP`,
+three-symbol alphabet, and check membership of some simple unary functions in `cobhamFP`,
 including one built by limited recursion on notation.
 -/
 
@@ -36,12 +36,12 @@ example : (smash (2 : Fin 3)).eval ![[0, 1], [0, 0, 0]] = List.replicate 6 2 :=
 
 /-! ## Membership in the unary class -/
 
-example : (fun x => x) ∈ CobhamFP Bool := ⟨proj 0, trivial, fun _ => rfl⟩
+example : (fun x => x) ∈ cobhamFP Bool := ⟨proj 0, trivial, fun _ => rfl⟩
 
-example : (fun x => true :: false :: x) ∈ CobhamFP Bool :=
+example : (fun x => true :: false :: x) ∈ cobhamFP Bool :=
   ⟨comp (cons true) fun _ => cons false, by simp, fun _ => rfl⟩
 
-example : (fun x : List (Fin 3) => List.replicate (x.length * x.length) 0) ∈ CobhamFP (Fin 3) :=
+example : (fun x : List (Fin 3) => List.replicate (x.length * x.length) 0) ∈ cobhamFP (Fin 3) :=
   ⟨comp (smash 0) fun _ => proj 0, by simp, fun _ => rfl⟩
 
 /-- The recursion in `unaryLength` computes the unary length, for any parameter vector. -/
@@ -54,7 +54,7 @@ private theorem unaryLength_rec (v : Fin 0 → List Bool) (x : List Bool) :
 
 /-- Unary length is in the class: its bound `x ↦ true :: x` is a limited term, and the
 recursion is length-bounded by it. -/
-example : (fun x : List Bool => List.replicate x.length true) ∈ CobhamFP Bool := by
+example : (fun x : List Bool => List.replicate x.length true) ∈ cobhamFP Bool := by
   refine ⟨unaryLength, ?_, fun x => ?_⟩
   · simp only [unaryLength, limited_boundedRec, limited_empty, limited_comp, limited_cons,
       limited_proj, implies_true, true_and]

From 050b30074ade6bf5fe6c5e4eeeb8cb664c854823 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Sep 2026 14:32:35 -0700
Subject: [PATCH 7/8] add unneeded typeclasses

---
 Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean b/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
index 8cc37f554..09b324bd8 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
@@ -29,7 +29,8 @@ namespace Cslib
 /-- The unary fragment of Cobham's function algebra over `Symbol`: the string functions
 denoted by limited unary terms. By Cobham's theorem [Cobham1965], this machine-independent
 class is exactly the polynomial-time computable functions. -/
-def cobhamFP (Symbol : Type u) : Set (List Symbol → List Symbol) :=
+def cobhamFP (Symbol : Type u) [Inhabited Symbol] [Fintype Symbol] :
+    Set (List Symbol → List Symbol) :=
   {f | ∃ c : Cobham Symbol 1, c.Limited ∧ ∀ x, c.eval (fun _ => x) = f x}
 
 open Turing.SingleTapeTM

From 8d526a1f09606e8679297befb55dfcf090ba3226 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Sep 2026 15:13:16 -0700
Subject: [PATCH 8/8] remove file

---
 Cslib.lean                                    |  1 -
 .../FunctionAlgebras/Cobham/Defs.lean         | 19 +++++++-
 .../FunctionAlgebras/Cobham/PolyTime.lean     | 44 -------------------
 CslibTests/Cobham.lean                        | 23 +++++-----
 4 files changed, 30 insertions(+), 57 deletions(-)
 delete mode 100644 Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean

diff --git a/Cslib.lean b/Cslib.lean
index 03b3c8cf1..328de8a68 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -45,7 +45,6 @@ public import Cslib.Computability.Distributed.FLP.OnePseudoConsensus
 public import Cslib.Computability.Distributed.FLP.PseudoConsensus
 public import Cslib.Computability.Distributed.FLP.ZeroConsensus
 public import Cslib.Computability.FunctionAlgebras.Cobham.Defs
-public import Cslib.Computability.FunctionAlgebras.Cobham.PolyTime
 public import Cslib.Computability.Languages.Congruences.BuchiCongruence
 public import Cslib.Computability.Languages.Congruences.RightCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero
diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index 6aaea13d2..6c9f3fe85 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -7,6 +7,7 @@ module
 
 public import Cslib.Init
 public import Mathlib.Data.Fin.Tuple.Basic
+import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
 
 /-!
 # Cobham's function algebra
@@ -23,8 +24,7 @@ The algebra is presented as a syntax `Cobham Symbol n` of terms denoting `n`-ary
 with semantics given by `Cobham.eval`.
 Cobham's side condition on recursion — that the recursively defined
 function be length-bounded by another function of the class — is not part of the syntax:
-it is the structural predicate `Cobham.Limited`,
-and `cobhamFP` collects the unary functions denoted by limited terms.
+it is the structural predicate `Cobham.Limited`.
 
 The functions are multi-arity (indexed by `Fin n` argument vectors) because limited
 recursion on notation inherently produces functions of higher arity.
@@ -37,6 +37,13 @@ recursion on notation inherently produces functions of higher arity.
 - `Cslib.Cobham.Limited` — the side condition that every recursion in a term is bounded
   by its bounding term
 
+## Main statements
+
+- `Cslib.Cobham.exists_limited_iff_polyTimeComputable` — Cobham's characterization of
+  polynomial time: over the binary alphabet, the functions denoted by limited unary terms are
+  exactly the polynomial-time computable functions
+  (`Cslib.Turing.SingleTapeTM.PolyTimeComputable`). Proof wanted.
+
 ## Design notes
 
 We work over strings of arbitrary `Symbol` type, rather than binary natural numbers.
@@ -173,6 +180,14 @@ def Limited {n : ℕ} : Cobham Symbol n → Prop
         ∀ v x, (recNotation base.eval (fun a => (step a).eval) v x).length ≤
           (bound.eval (Fin.cons x v)).length := Iff.rfl
 
+open Turing.SingleTapeTM in
+/-- **Cobham's characterization of polynomial time** [Cobham1965]: a binary string function
+is denoted by a limited unary term if and only if it is computable in polynomial time by a
+single-tape Turing machine. -/
+proof_wanted exists_limited_iff_polyTimeComputable (f : List Bool → List Bool) :
+    (∃ c : Cobham Bool 1, c.Limited ∧ ∀ x, c.eval (fun _ => x) = f x) ↔
+      Nonempty (PolyTimeComputable f)
+
 end Cobham
 
 end Cslib
diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean b/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
deleted file mode 100644
index 09b324bd8..000000000
--- a/Cslib/Computability/FunctionAlgebras/Cobham/PolyTime.lean
+++ /dev/null
@@ -1,44 +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 Cslib.Computability.FunctionAlgebras.Cobham.Defs
-public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
-
-/-!
-# Cobham's theorem
-
-Cobham's theorem [Cobham1965] states that the functions of Cobham's algebra
-(`Cslib.cobhamFP`) are exactly the functions computable in polynomial time by a Turing
-machine (`Cslib.Turing.SingleTapeTM.PolyTimeComputable`).
-
-## References
-
-* [A. Cobham, *The intrinsic computational difficulty of functions*][Cobham1965]
--/
-
-@[expose] public section
-
-universe u
-
-namespace Cslib
-
-/-- The unary fragment of Cobham's function algebra over `Symbol`: the string functions
-denoted by limited unary terms. By Cobham's theorem [Cobham1965], this machine-independent
-class is exactly the polynomial-time computable functions. -/
-def cobhamFP (Symbol : Type u) [Inhabited Symbol] [Fintype Symbol] :
-    Set (List Symbol → List Symbol) :=
-  {f | ∃ c : Cobham Symbol 1, c.Limited ∧ ∀ x, c.eval (fun _ => x) = f x}
-
-open Turing.SingleTapeTM
-
-/-- **Cobham's theorem**: a string function is in Cobham's algebra if and only if it is
-computable in polynomial time by a single-tape Turing machine. -/
-proof_wanted cobhamFP_iff_polyTimeComputable {Symbol : Type} [Inhabited Symbol]
-    [Fintype Symbol] (f : List Symbol → List Symbol) :
-    f ∈ cobhamFP Symbol ↔ Nonempty (PolyTimeComputable f)
-
-end Cslib
diff --git a/CslibTests/Cobham.lean b/CslibTests/Cobham.lean
index 8b3d66d97..5f11bac4c 100644
--- a/CslibTests/Cobham.lean
+++ b/CslibTests/Cobham.lean
@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bolton Bailey
 -/
 
-import Cslib.Computability.FunctionAlgebras.Cobham.PolyTime
+import Cslib.Computability.FunctionAlgebras.Cobham.Defs
 import Mathlib.Data.Fin.VecNotation
 
 /-! # Cobham's function algebra tests
 
 These tests evaluate a few terms of Cobham's algebra, over the binary alphabet and a
-three-symbol alphabet, and check membership of some simple unary functions in `cobhamFP`,
-including one built by limited recursion on notation.
+three-symbol alphabet, and check that some simple unary functions are denoted by limited
+terms, including one built by limited recursion on notation.
 -/
 
 namespace CslibTests.Cobham
@@ -34,14 +34,16 @@ example : (comp (cons true) fun _ => cons false).eval ![[true]] = [true, false,
 
 example : (smash (2 : Fin 3)).eval ![[0, 1], [0, 0, 0]] = List.replicate 6 2 := by decide
 
-/-! ## Membership in the unary class -/
+/-! ## Functions denoted by limited unary terms -/
 
-example : (fun x => x) ∈ cobhamFP Bool := ⟨proj 0, trivial, fun _ => rfl⟩
+example : ∃ c : Cobham Bool 1, c.Limited ∧ ∀ x, c.eval (fun _ => x) = x :=
+  ⟨proj 0, trivial, fun _ => rfl⟩
 
-example : (fun x => true :: false :: x) ∈ cobhamFP Bool :=
+example : ∃ c : Cobham Bool 1, c.Limited ∧ ∀ x, c.eval (fun _ => x) = true :: false :: x :=
   ⟨comp (cons true) fun _ => cons false, by simp, fun _ => rfl⟩
 
-example : (fun x : List (Fin 3) => List.replicate (x.length * x.length) 0) ∈ cobhamFP (Fin 3) :=
+example : ∃ c : Cobham (Fin 3) 1, c.Limited ∧
+    ∀ x, c.eval (fun _ => x) = List.replicate (x.length * x.length) 0 :=
   ⟨comp (smash 0) fun _ => proj 0, by simp, fun _ => rfl⟩
 
 /-- The recursion in `unaryLength` computes the unary length, for any parameter vector. -/
@@ -52,9 +54,10 @@ private theorem unaryLength_rec (v : Fin 0 → List Bool) (x : List Bool) :
   | nil => rfl
   | cons b x ih => simp [ih, List.replicate_succ]
 
-/-- Unary length is in the class: its bound `x ↦ true :: x` is a limited term, and the
-recursion is length-bounded by it. -/
-example : (fun x : List Bool => List.replicate x.length true) ∈ cobhamFP Bool := by
+/-- Unary length is denoted by a limited term: its bound `x ↦ true :: x` is a limited term,
+and the recursion is length-bounded by it. -/
+example : ∃ c : Cobham Bool 1, c.Limited ∧
+    ∀ x, c.eval (fun _ => x) = List.replicate x.length true := by
   refine ⟨unaryLength, ?_, fun x => ?_⟩
   · simp only [unaryLength, limited_boundedRec, limited_empty, limited_comp, limited_cons,
       limited_proj, implies_true, true_and]