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 01/16] 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 02/16] 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 03/16] 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 04/16] 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 05/16] 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 06/16] 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 07/16] 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 08/16] 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]

From 0a04070cdd46b8cb6ac9c63370c51d985a904e23 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 19 Sep 2026 13:07:36 -0700
Subject: [PATCH 09/16] more design notes.

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

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index 6c9f3fe85..4aefa606e 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -46,17 +46,40 @@ recursion on notation inherently produces functions of higher arity.
 
 ## 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.
+Cobham's paper operates over natural numbers,
+but essentially only manipulates these numbers through operations on the list of digits.
+In light of this, and for the convenience in recursive definitions,
+we modify Cobham's definition slightly to work over strings of arbitrary `Symbol` type,
+rather than naturals.
+
+### Length bounding
+
+There are essentially two slightly different ways of handling the part of the definition that
+ensures the recursions are bounded are bounded.
+
+In Cobham's original formulation, a function is allowed in the set of
+recursive constructions that allows us to obtain outputs whose length is a multiplication of
+lengths of input. This type of function seems to be known as a "smash function".
+Originally this smash function was `x ^ length y`, but `c^(length x * length y)` for a 1-character
+string `c` is also possible (e.g. [BBFMT16]).
+The presence of a smash function ensures we can create functions of polynomial blowup of any degree.
+The limited recursion is then length-bounded by another function of the class.
+
+The alternative is to bound the recursion not by another function of the class,
+but by a generic multivariable polynomial in the lengths of the inputs.
+This obviates the need for a smash function.
+Proof that this is equivalent to FP can be found in [Clote] Lemma 3.90, where it is called
+"polynomially bounded recursion on notation".
+Implementing this version is a TODO.
 
 ## References
 
 * [A. Cobham, *The intrinsic computational difficulty of functions*][Cobham1965]
+  [Link](https://www.cs.toronto.edu/~sacook/homepage/cobham_intrinsic.pdf)
+* [Beckmann et al., "Cobham Recursive Set Functions"][BBFMT16]
+  [Link](https://mathweb.ucsd.edu/~sbuss/ResearchWeb/CRSF_paperone/paperoneRevisedAPALNov2015.pdf)
+* [Clote, *Computational Models and Function Algebras*][Clote]
+  [Link](https://bioinformatics.bc.edu/clotelab/pub/cloteHandbookRecTheory.pdf)
 -/
 
 @[expose] public section

From ed7a2e7d0161e448914fc93a6737e682072ed524 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 19 Sep 2026 13:20:27 -0700
Subject: [PATCH 10/16] more explanation

---
 .../FunctionAlgebras/Cobham/Defs.lean         | 27 ++++++++++++-------
 1 file changed, 17 insertions(+), 10 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index 4aefa606e..4b6fd564e 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -17,7 +17,7 @@ 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,
+the projections, the empty string, the symbol conses, 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,
@@ -52,7 +52,7 @@ In light of this, and for the convenience in recursive definitions,
 we modify Cobham's definition slightly to work over strings of arbitrary `Symbol` type,
 rather than naturals.
 
-### Length bounding
+### Length bounding syntax approaches
 
 There are essentially two slightly different ways of handling the part of the definition that
 ensures the recursions are bounded are bounded.
@@ -72,6 +72,15 @@ Proof that this is equivalent to FP can be found in [Clote] Lemma 3.90, where it
 "polynomially bounded recursion on notation".
 Implementing this version is a TODO.
 
+### Enforcing the bounding condition
+
+In `Cobham.boundedRec`, while we provide a bound, we do not actually enforce this bound always holds
+either in the syntax or in the evaluation.
+This avoids mutual recursion.
+Instead, we add a predicate `Limited` which checks that the bound always holds, which we can use
+to examine the class of functions that are actually bounded.
+
+
 ## References
 
 * [A. Cobham, *The intrinsic computational difficulty of functions*][Cobham1965]
@@ -90,20 +99,18 @@ namespace Cslib
 
 variable {Symbol : Type u}
 
-/-- **Terms of Cobham's function algebra** over the alphabet `Symbol`. A term of type
+/--
+**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 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`. -/
+`Cobham.eval`): the projections, the empty string, the cons operation for each symbol `x ↦ a :: x`,
+and the smash function, closed under composition and recursion on notation.
+-/
 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`. -/
+  /-- The cons function `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

From bd1684e651c60483837010b8640d258e4c4dd25d Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 19 Sep 2026 13:25:47 -0700
Subject: [PATCH 11/16] add multitape version

---
 .../FunctionAlgebras/Cobham/Defs.lean         | 21 ++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index 4b6fd564e..4e87f07ff 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.MultiTape.Deterministic
 import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
 
 /-!
@@ -43,6 +44,9 @@ recursion on notation inherently produces functions of higher arity.
   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.
+- `Cslib.Cobham.exists_limited_iff_multiTapePolyTimeComputable` — the same characterization
+  against the multi-tape model
+  (`Cslib.Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength`). Proof wanted.
 
 ## Design notes
 
@@ -76,11 +80,10 @@ Implementing this version is a TODO.
 
 In `Cobham.boundedRec`, while we provide a bound, we do not actually enforce this bound always holds
 either in the syntax or in the evaluation.
-This avoids mutual recursion.
+We do this to avoid mutual recursion.
 Instead, we add a predicate `Limited` which checks that the bound always holds, which we can use
 to examine the class of functions that are actually bounded.
 
-
 ## References
 
 * [A. Cobham, *The intrinsic computational difficulty of functions*][Cobham1965]
@@ -211,13 +214,25 @@ def Limited {n : ℕ} : Cobham Symbol n → Prop
           (bound.eval (Fin.cons x v)).length := Iff.rfl
 
 open Turing.SingleTapeTM in
-/-- **Cobham's characterization of polynomial time** [Cobham1965]: a binary string function
+/-- **Cobham's characterization of polynomial time**: 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)
 
+open Turing.MultiTapeTM in
+/-- **Cobham's characterization of polynomial time, multi-tape version**: a binary
+string function is denoted by a limited unary term if and only if it is computable in polynomial
+time by a multi-tape Turing machine. The number of tapes is existentially quantified by
+`ComputableInTimeAndSpace`. The space bound is a separate polynomial, which is no extra
+assumption: a machine running for `t` steps visits at most `t + 1` cells per tape. -/
+proof_wanted exists_limited_iff_multiTapePolyTimeComputable (f : List Bool → List Bool) :
+    (∃ c : Cobham Bool 1, c.Limited ∧ ∀ x, c.eval (fun _ => x) = f x) ↔
+      ∃ time space : Polynomial ℕ,
+        ComputableInTimeAndSpaceOfLength f (Function.Embedding.refl _)
+          (Function.Embedding.refl _) (fun n => time.eval n) (fun n => space.eval n)
+
 end Cobham
 
 end Cslib

From 8aa96fb8ad46d7b0ce57e15e597ae8dd1c4f036f Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 19 Sep 2026 14:03:12 -0700
Subject: [PATCH 12/16] add refs

---
 .../FunctionAlgebras/Cobham/Defs.lean         | 10 ++++----
 references.bib                                | 25 +++++++++++++++++++
 2 files changed, 30 insertions(+), 5 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index 4e87f07ff..d1e8e9fd5 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -46,7 +46,7 @@ recursion on notation inherently produces functions of higher arity.
   (`Cslib.Turing.SingleTapeTM.PolyTimeComputable`). Proof wanted.
 - `Cslib.Cobham.exists_limited_iff_multiTapePolyTimeComputable` — the same characterization
   against the multi-tape model
-  (`Cslib.Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength`). Proof wanted.
+  (`Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength`). Proof wanted.
 
 ## Design notes
 
@@ -65,14 +65,14 @@ In Cobham's original formulation, a function is allowed in the set of
 recursive constructions that allows us to obtain outputs whose length is a multiplication of
 lengths of input. This type of function seems to be known as a "smash function".
 Originally this smash function was `x ^ length y`, but `c^(length x * length y)` for a 1-character
-string `c` is also possible (e.g. [BBFMT16]).
+string `c` is also possible (e.g. [Beckmann2016]).
 The presence of a smash function ensures we can create functions of polynomial blowup of any degree.
 The limited recursion is then length-bounded by another function of the class.
 
 The alternative is to bound the recursion not by another function of the class,
 but by a generic multivariable polynomial in the lengths of the inputs.
 This obviates the need for a smash function.
-Proof that this is equivalent to FP can be found in [Clote] Lemma 3.90, where it is called
+Proof that this is equivalent to FP can be found in [Clote1999] Lemma 3.90, where it is called
 "polynomially bounded recursion on notation".
 Implementing this version is a TODO.
 
@@ -88,9 +88,9 @@ to examine the class of functions that are actually bounded.
 
 * [A. Cobham, *The intrinsic computational difficulty of functions*][Cobham1965]
   [Link](https://www.cs.toronto.edu/~sacook/homepage/cobham_intrinsic.pdf)
-* [Beckmann et al., "Cobham Recursive Set Functions"][BBFMT16]
+* [Beckmann et al., "Cobham Recursive Set Functions"][Beckmann2016]
   [Link](https://mathweb.ucsd.edu/~sbuss/ResearchWeb/CRSF_paperone/paperoneRevisedAPALNov2015.pdf)
-* [Clote, *Computational Models and Function Algebras*][Clote]
+* [Clote, *Computation Models and Function Algebras*][Clote1999]
   [Link](https://bioinformatics.bc.edu/clotelab/pub/cloteHandbookRecTheory.pdf)
 -/
 
diff --git a/references.bib b/references.bib
index f1d47ef87..4ada465c9 100644
--- a/references.bib
+++ b/references.bib
@@ -417,6 +417,31 @@ @incollection{ Cobham1965
   year         = {1965}
 }
 
+@article{ Beckmann2016,
+  author       = {Beckmann, Arnold and Buss, Sam and Friedman, Sy-David and
+                  M{\"u}ller, Moritz and Thapen, Neil},
+  title        = {Cobham recursive set functions},
+  journal      = {Annals of Pure and Applied Logic},
+  volume       = {167},
+  number       = {3},
+  pages        = {335--369},
+  year         = {2016},
+  doi          = {10.1016/j.apal.2015.12.005}
+}
+
+@incollection{ Clote1999,
+  author       = {Clote, Peter},
+  editor       = {Griffor, Edward R.},
+  title        = {Computation Models and Function Algebras},
+  booktitle    = {Handbook of Computability Theory},
+  series       = {Studies in Logic and the Foundations of Mathematics},
+  volume       = {140},
+  pages        = {589--681},
+  publisher    = {North-Holland},
+  address      = {Amsterdam},
+  year         = {1999}
+}
+
 @book{            Cutland1980,
   author       = {Cutland, Nigel J.},
   title        = {Computability: An Introduction to Recursive Function Theory},

From 2e7d697cf405b38924539b222072d9c6d74207ad Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 19 Sep 2026 14:07:01 -0700
Subject: [PATCH 13/16] wording nits

---
 .../Computability/FunctionAlgebras/Cobham/Defs.lean  | 12 ++++++------
 CslibTests/Cobham.lean                               |  2 +-
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index d1e8e9fd5..eafa23b95 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -45,8 +45,7 @@ recursion on notation inherently produces functions of higher arity.
   exactly the polynomial-time computable functions
   (`Cslib.Turing.SingleTapeTM.PolyTimeComputable`). Proof wanted.
 - `Cslib.Cobham.exists_limited_iff_multiTapePolyTimeComputable` — the same characterization
-  against the multi-tape model
-  (`Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength`). Proof wanted.
+  against the multi-tape model. Proof wanted.
 
 ## Design notes
 
@@ -59,11 +58,12 @@ rather than naturals.
 ### Length bounding syntax approaches
 
 There are essentially two slightly different ways of handling the part of the definition that
-ensures the recursions are bounded are bounded.
+ensures the recursions are bounded.
 
-In Cobham's original formulation, a function is allowed in the set of
-recursive constructions that allows us to obtain outputs whose length is a multiplication of
-lengths of input. This type of function seems to be known as a "smash function".
+In Cobham's original formulation, a function is included in the set of
+recursive constructions that allows us to obtain an output
+the length of which is a multiplication of lengths of input.
+This type of function seems to be known as a "smash function".
 Originally this smash function was `x ^ length y`, but `c^(length x * length y)` for a 1-character
 string `c` is also possible (e.g. [Beckmann2016]).
 The presence of a smash function ensures we can create functions of polynomial blowup of any degree.
diff --git a/CslibTests/Cobham.lean b/CslibTests/Cobham.lean
index 5f11bac4c..2de8a2e5a 100644
--- a/CslibTests/Cobham.lean
+++ b/CslibTests/Cobham.lean
@@ -21,7 +21,7 @@ open Cslib Cslib.Cobham
 /-! ## Evaluation -/
 
 /-- Recursion on notation counting the symbols of its argument in unary, bounded by the
-successor `x ↦ true :: x`. -/
+cons `x ↦ true :: x`. -/
 private def unaryLength : Cobham Bool 1 :=
   boundedRec empty (fun _ => comp (cons true) fun _ => proj 1) (cons true)
 

From db9cf38809247d446e88a9ed15977a60200429eb Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 19 Sep 2026 15:05:37 -0700
Subject: [PATCH 14/16] grammar

---
 Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index eafa23b95..c42935e01 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -17,9 +17,14 @@ 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 conses, and the smash functions,
-and closed under composition and limited recursion on notation.
+This is the smallest class of functions `(Fin n → List Symbol) → List Symbol` that
+
+* contains projections,
+* contains the constant empty string function,
+* contains the symbol consing functions,
+* contains the smash functions,
+* is closed under composition,
+* and is closed under "limited" or "bounded" 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`.

From 429ae9316d24f22beb2d3c36a3c9be271e7ebd7d Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 19 Sep 2026 15:09:55 -0700
Subject: [PATCH 15/16] more docstring improvements

---
 .../Computability/FunctionAlgebras/Cobham/Defs.lean  | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
index c42935e01..916fbd5cd 100644
--- a/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
+++ b/Cslib/Computability/FunctionAlgebras/Cobham/Defs.lean
@@ -28,9 +28,8 @@ This is the smallest class of functions `(Fin n → List Symbol) → List Symbol
 
 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`.
+Cobham's condition that the recursively defined functions obey their length bounds is enforced by
+the 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.
@@ -43,7 +42,7 @@ 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
+## Proofs Wanted
 
 - `Cslib.Cobham.exists_limited_iff_polyTimeComputable` — Cobham's characterization of
   polynomial time: over the binary alphabet, the functions denoted by limited unary terms are
@@ -83,7 +82,7 @@ Implementing this version is a TODO.
 
 ### Enforcing the bounding condition
 
-In `Cobham.boundedRec`, while we provide a bound, we do not actually enforce this bound always holds
+In `Cobham.boundedRec`, while we provide a bound, we do not enforce this bound always holds
 either in the syntax or in the evaluation.
 We do this to avoid mutual recursion.
 Instead, we add a predicate `Limited` which checks that the bound always holds, which we can use
@@ -110,7 +109,8 @@ 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 cons operation for each symbol `x ↦ a :: x`,
+`Cobham.eval`):
+the projections, the empty string, the cons operation for each symbol `x ↦ a :: x`,
 and the smash function, closed under composition and recursion on notation.
 -/
 inductive Cobham (Symbol : Type u) : ℕ → Type u

From c3b8bbfab45c6a3428c1398978dd6ca4f88db3bc Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 19 Sep 2026 15:18:13 -0700
Subject: [PATCH 16/16] cite data

---
 references.bib | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/references.bib b/references.bib
index 4ada465c9..fde0a0105 100644
--- a/references.bib
+++ b/references.bib
@@ -436,10 +436,13 @@ @incollection{ Clote1999
   booktitle    = {Handbook of Computability Theory},
   series       = {Studies in Logic and the Foundations of Mathematics},
   volume       = {140},
+  chapter      = {17},
   pages        = {589--681},
-  publisher    = {North-Holland},
-  address      = {Amsterdam},
-  year         = {1999}
+  publisher    = {Elsevier},
+  year         = {1999},
+  issn         = {0049-237X},
+  doi          = {10.1016/S0049-237X(99)80033-0},
+  url          = {https://www.sciencedirect.com/science/article/pii/S0049237X99800330}
 }
 
 @book{            Cutland1980,