diff --git a/Complexity.lean b/Complexity.lean
index 0b1a6ab06..a615f3f2e 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1587,7 +1587,6 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.S
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Words
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower
-public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatStream
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Padding
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean
index 11bd50bbb..c4a458a8f 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean
@@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Foldl
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Basic
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat
+import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormalForm
 
 /-!
 # Tidy computability in polynomial time
@@ -281,10 +282,12 @@ public theorem ComputableTidilyInPolyTime.foldl {γ α β : Type u} {encIn : γ
       ((hlen.add (.const 1)).mul ((hmax.add hlMax').add (.const 1)))),
     (PolyBounded.const c).mul ((((hs₁.add hs₂).add hmax).add hlMax').add (.const 1)), h⟩
 
-/-- The successor is tidily computable in polynomial time, in the binary encoding `encNat`. -/
+/-- The successor is tidily computable in polynomial time, in the binary encoding `encNat`, from
+the transducer certificate `computableInTimeAndSpace_succ`. -/
 @[fun_prop]
 public theorem computableTidilyInPolyTime_succ : ComputableTidilyInPolyTime (· + 1) encNat encNat :=
-  let ⟨c, h⟩ := computableTidilyInTimeAndSpace_succ
-  ⟨_, _, .of_forall_le c 2 (fun _ => le_rfl), .of_forall_le c 1 (fun _ => by simp), h⟩
+  let ⟨c, h⟩ := computableInTimeAndSpace_succ.exists_computableTidilyInTimeAndSpace
+  ⟨_, _, .of_forall_le (c + 6) 1 (fun _ => by simp only [pow_one]; nlinarith),
+    .of_forall_le c 0 (fun _ => by simp), h⟩
 
 end Turing.MultiTapeTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean
index e051e45ed..7570c4bcb 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean
@@ -34,6 +34,7 @@ Framed-list and option rules infer the payload encoding from the representation
 
 * `Turing.MultiTapeTM.ComputableInDegree.foldl'`,
   `Turing.MultiTapeTM.ComputableInDegree.foldlWith`: plain left folds with degree bounds.
+* `Turing.MultiTapeTM.ComputableInDegree.natSucc`: binary successor with degrees one.
 * `Turing.MultiTapeTM.computableInDegree_add`, `Turing.MultiTapeTM.computableInDegree_mul`:
   plain binary addition (quadratic) and multiplication (cubic).
 * `Turing.MultiTapeTM.ComputableInO.comp_enc`: reuse a bit-word computation on encoded
@@ -305,6 +306,11 @@ private lemma run_copy_fin3 (T : Transducer Bool (Fin 3)) (hT : ∀ b, T.step 2
   | nil => simp [hf]
   | cons b w ih => simp [hT, ih]
 
+/-- Binary successor has cost and output degree one, from the transducer certificate
+`computableInTimeAndSpace_succ`. -/
+theorem natSucc : ComputableInDegree (· + 1) encNat encNat 1 1 :=
+  of_linear .natSucc
+
 /-- Adding one on unary-magnitude signed integers. -/
 theorem int_succ : ComputableInDegree (· + 1) encInt encInt 1 1 := by
   refine of_linear (.of_transducer intSuccT fun z => ?_)
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean
index 9587f63f8..c9e1f8bef 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean
@@ -8,31 +8,26 @@ module
 -- upstream: vendored crei:crei/tidy-universal @7f7c0696 (unsubmitted)
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits
-public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Foldl
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair
-import Mathlib.Data.Nat.Bitwise
-import Mathlib.Tactic.Ring
+public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTransducer
 
 /-!
 # The successor in binary
 
 `encNat`, reexported from `Encodings.Nat.Bits`, encodes a natural number by its binary digits,
 least significant first (`Nat.bits`).
-The successor is a left fold over the digits that keeps a carry and appends one digit per round,
-followed by a final carry digit. Its tidy computability is derived from that of the fold
-(`Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl`) and of the parts of a round.
-
-## Main definitions
-
-* `Turing.MultiTapeTM.encNat`: natural numbers encoded by their binary digits.
-* `Turing.MultiTapeTM.encNat3`: triples of natural numbers encoded in binary.
+The successor is computed by one streaming transducer whose state is the carry: on each digit `b`
+in carry `c` it emits `c ^^ b` and keeps the carry `c && b`, and at the end it emits a final `1`
+exactly when a carry remains. The machine reads its input once and uses no work tape.
 
 ## Main results
 
-* `Turing.MultiTapeTM.computableTidilyInTimeAndSpace_succ`: the successor is tidily computable in
-  quadratic time and linear space.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_succ`: the successor is computable within
+  `2 * (encNat n).length + 3` steps and zero work space.
+* `Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natSucc`: its linear form.
 -/
 
 namespace Turing.MultiTapeTM
@@ -42,96 +37,39 @@ public abbrev encNat3 : ℕ × ℕ × ℕ ↪ List Bool := encPair encNat (encPa
 
 namespace NatSucc
 
-open ComputableInLinearTimeAndSpace
-
-/-- A round is tidily computable in linear time and space. -/
-public lemma linear_succStep :
-    ComputableTidilyInLinearTimeAndSpace (fun p => succStep p.1 p.2)
-      (encPair encAcc encBool) encAcc := by
-  apply Internal.NormalForm.linear
-  have hacc : ComputableInLinearTimeAndSpace Prod.fst (encPair encAcc encBool) encAcc :=
-    PairEncoding.fst encBool
-  have hcarry : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => p.1.1)
-      (encPair encAcc encBool) encBool :=
-    (PairEncoding.fst encBits).comp hacc
-  have hdigit : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => p.2)
-      (encPair encAcc encBool) encBool :=
-    PairEncoding.snd encAcc
-  have hdigits : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => p.1.2)
-      (encPair encAcc encBool) encBits :=
-    (PairEncoding.snd encBool).comp hacc
-  have hand : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool =>
-      p.1.1 && p.2) (encPair encAcc encBool) encBool := by
-    convert hdigit.ite (hcarry.restrict _) ((const false).restrict _) using 1
-    funext p
-    cases p.2 <;> simp
-  have hnot : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => !p.1.1)
-      (encPair encAcc encBool) encBool := by
-    convert hcarry.ite ((const false).restrict _) ((const true).restrict _) using 1
-    funext p
-    cases p.1.1 <;> rfl
-  have hxor : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool =>
-      p.1.1 ^^ p.2) (encPair encAcc encBool) encBool := by
-    convert hdigit.ite (hnot.restrict _) (hcarry.restrict _) using 1
-    funext p
-    cases p.2 <;> simp
-  exact hand.pair (hdigits.append hxor (encOut := encBits) fun _ => rfl)
-
-/-- The final carry digit is appended in linear time and space. -/
-public lemma linear_succFinish :
-    ComputableTidilyInLinearTimeAndSpace succFinish encAcc encBits := by
-  apply Internal.NormalForm.linear
-  have hdigits : ComputableInLinearTimeAndSpace Prod.snd encAcc encBits :=
-    PairEncoding.snd encBool
-  have happend : ComputableInLinearTimeAndSpace (fun p => p.2 ++ [true]) encAcc encBits :=
-    hdigits.append (const (encMid := encBool) true) (encOut := encBits) fun _ => rfl
-  have hcarry : ComputableInLinearTimeAndSpace Prod.fst encAcc encBool :=
-    PairEncoding.fst encBits
-  exact hcarry.ite (happend.restrict _) (hdigits.restrict _)
+/-- The successor as a transducer: the state is the carry, initially set. -/
+private def succTransducer : Transducer Bool Bool where
+  q₀ := true
+  step c b := (c && b, [c ^^ b])
+  final c := if c then [true] else []
+  length_step_le _ _ := by simp
+  length_final_le c := by cases c <;> simp
+
+private lemma run_succTransducer (c : Bool) (l : List Bool) :
+    succTransducer.run c l = incr c l := by
+  induction l generalizing c with
+  | nil => cases c <;> rfl
+  | cons b l ih =>
+    rw [Transducer.run_cons, ih]
+    cases c <;> cases b <;> simp [succTransducer, incr]
 
 end NatSucc
 
 open NatSucc in
-/-- The successor is tidily computable in quadratic time and linear space, in the binary encoding
-`encNat`. -/
-public theorem computableTidilyInTimeAndSpace_succ :
-    ∃ c, ComputableTidilyInTimeAndSpace (· + 1) encNat encNat
-      (fun n => c * ((encNat n).length + 1) ^ 2) (fun n => c * ((encNat n).length + 1)) := by
-  obtain ⟨cl, hlist⟩ := ComputableTidilyInLinearTimeAndSpace.of_eq (f := Nat.bits)
-    (encIn := encNat) (encMid := encBits) fun _ => rfl
-  obtain ⟨ci, hinit⟩ := ComputableTidilyInLinearTimeAndSpace.const (encIn := encNat)
-    (encMid := encAcc) (true, [])
-  obtain ⟨cs, hstep⟩ := linear_succStep
-  -- the bounds of a round and of the state of the fold
-  have hlen (n i : ℕ) : (((n.bits.take i).foldl succStep (true, [])).2).length ≤ n.bits.length := by
-    rw [length_foldl_succStep]
-    simp
-  obtain ⟨cf, hfold⟩ := ComputableTidilyInTimeAndSpace.foldl (encA := encBool) (encL := encBits)
-    (encBA := encPair encAcc encBool) (encS := encPair encBits encAcc)
-    (encO := encOption (encPair encBits encAcc))
-    (hlist.mono (t' := fun n => (cl + ci) * ((encNat n).length + 1))
-      (s' := fun n => (cl + ci) * ((encNat n).length + 1))
-      (fun n => by ring_nf; omega) (fun n => by ring_nf; omega))
-    (hinit.mono (fun n => by ring_nf; omega) (fun n => by ring_nf; omega)) hstep
-    (tMax := fun n => cs * (2 * (encNat n).length + 9))
-    (sMax := fun n => cs * (2 * (encNat n).length + 9))
-    (lMax := fun n => 2 * (encNat n).length + 4)
-    (fun n i _ => Nat.mul_le_mul_left cs (by simp; have := hlen n i; omega))
-    (fun n i _ => Nat.mul_le_mul_left cs (by simp; have := hlen n i; omega))
-    (fun n i hi => by simp [length_foldl_succStep]; omega)
-  obtain ⟨cg, hfinish⟩ := linear_succFinish
-  -- vendored: crei's `comp` is `comp_linear` here, as cslib #1111 restates `comp`
-  obtain ⟨cc, h⟩ := ComputableTidilyInTimeAndSpace.comp_linear hfinish hfold
-  obtain ⟨k, S, _, tm, htm⟩ := h
-  refine ⟨cf * (cl + ci + 9 * cs + 5) + 4 * (cg + cc), k, S, inferInstance, tm, fun n => ?_⟩
-  have hmid : (encAcc (n.bits.foldl succStep (true, []))).length = n.bits.length + 3 := by
-    rw [length_encAcc, length_foldl_succStep]
-    simp
-  change tm.ComputesTidilyInTimeAndSpace _ (n + 1).bits _ _
-  rw [bits_succ_eq_foldl]
-  refine (htm n).mono ?_ ?_ <;>
-  · simp only [hmid, encNat_apply]
-    ring_nf
-    omega
+/-- **Binary successor in linear time and zero work space.** One streaming transducer computes
+`n + 1` from `encNat n` within `2 * (encNat n).length + 3` steps without work tapes. -/
+public theorem computableInTimeAndSpace_succ :
+    ComputableInTimeAndSpace (· + 1) encNat encNat (fun n => 2 * (encNat n).length + 3)
+      (fun _ => 0) :=
+  ⟨0, _, inferInstance, succTransducer.toTM, fun n => by
+    rw [encNat_apply, encNat_apply, bits_succ, ← run_succTransducer]
+    exact succTransducer.computesInTimeAndSpace_toTM n.bits⟩
+
+/-- Binary successor in linear time and work space, from `computableInTimeAndSpace_succ`. -/
+public theorem ComputableInLinearTimeAndSpace.natSucc :
+    ComputableInLinearTimeAndSpace (· + 1) encNat encNat :=
+  let ⟨k, Q, hQ, tm, h⟩ := computableInTimeAndSpace_succ
+  ⟨3, k, Q, hQ, tm, fun n =>
+    ⟨(h n).1, (h n).2.1.mono (by dsimp; omega), (h n).2.2.mono (Nat.zero_le _)⟩⟩
 
 end Turing.MultiTapeTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatStream.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatStream.lean
deleted file mode 100644
index bb7508453..000000000
--- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatStream.lean
+++ /dev/null
@@ -1,117 +0,0 @@
-/-
-Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Christian Reitwiessner
--/
-
-module
--- upstream: vendored crei:crei/tidy-universal @7f7c0696 (unsubmitted)
-
-public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat
-public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.StreamFold
-import Mathlib.Tactic.Linarith
-
-/-!
-# The successor in binary, as a streaming fold
-
-The successor on `Turing.MultiTapeTM.encNat` reads the digits once, least significant first,
-keeping the carry as its state: it emits each digit plus the carry and, at the end, a final carry
-digit. As a streaming fold (`Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.streamFold`) it is
-tidily computable in linear time and constant space.
-
-## Main results
-
-* `Turing.MultiTapeTM.computableTidilyInTimeAndSpace_succ_stream`: the successor is tidily
-  computable in linear time and constant space.
--/
-
-namespace Turing.MultiTapeTM
-
-namespace NatStream
-
-open NatSucc
-
-/-- Reads one digit and emits it. -/
-def digitReader : InputReader Bool Unit := ⟨(), fun _ b => (none, some b)⟩
-
-/-- The carry after a digit. -/
-def carry (p : Bool × Bool) : Bool := p.1 && p.2
-
-/-- The digit plus the carry. -/
-def sumDigit (p : Bool × Bool) : Bool := p.1 ^^ p.2
-
-/-- The final carry digit. -/
-def finalDigit (c : Bool) : List Bool := if c then [true] else []
-
-lemma streamEmit_append_finalDigit (c : Bool) (l : List Bool) :
-    streamEmit carry (fun p => encBool (sumDigit p)) c l ++
-      encBits (finalDigit (streamState c carry l l.length)) = incr c l := by
-  induction l generalizing c with
-  | nil => cases c <;> rfl
-  | cons b l ih =>
-    have h := ih (c && b)
-    simp only [streamEmit, streamState, List.length_cons, List.take_succ_cons, List.foldl_cons,
-      List.take_length] at h ⊢
-    cases c <;> cases b <;> simp_all [incr, carry, sumDigit]
-
-open ComputableTidilyInLinearTimeAndSpace in
-/-- The parts of a round, on the carry and a digit, in linear time and space. -/
-lemma linear_parts :
-    ComputableTidilyInLinearTimeAndSpace carry (encPair encBool encBool) encBool ∧
-      ComputableTidilyInLinearTimeAndSpace sumDigit (encPair encBool encBool) encBool := by
-  have hc : ComputableTidilyInLinearTimeAndSpace Prod.fst (encPair encBool encBool) encBool :=
-    Internal.NormalForm.linear (PairEncoding.fst encBool)
-  have hd : ComputableTidilyInLinearTimeAndSpace Prod.snd (encPair encBool encBool) encBool :=
-    Internal.NormalForm.linear (PairEncoding.snd encBool)
-  have hnot : ComputableTidilyInLinearTimeAndSpace (fun p : Bool × Bool => !p.1)
-      (encPair encBool encBool) encBool := by
-    convert hc.ite ((const false).restrict _) ((const true).restrict _) using 1
-    funext ⟨a, b⟩
-    cases a <;> rfl
-  refine ⟨?_, ?_⟩
-  · convert hd.ite (hc.restrict _) ((const false).restrict _) using 1
-    funext ⟨a, b⟩
-    cases a <;> cases b <;> rfl
-  · convert hd.ite (hnot.restrict _) (hc.restrict _) using 1
-    funext ⟨a, b⟩
-    cases a <;> cases b <;> rfl
-
-open ComputableTidilyInLinearTimeAndSpace in
-lemma linear_finalDigit : ComputableTidilyInLinearTimeAndSpace finalDigit encBool encBits := by
-  convert (of_eq (f := id) (encIn := encBool) (encMid := encBool) fun _ => rfl).ite
-    ((const [true]).restrict _) ((const []).restrict _) using 1
-  funext c
-  cases c <;> rfl
-
-end NatStream
-
-open NatSucc NatStream in
-/-- The successor is tidily computable in linear time and constant space, in the binary encoding
-`encNat`. -/
-public theorem computableTidilyInTimeAndSpace_succ_stream :
-    ∃ c, ComputableTidilyInTimeAndSpace (· + 1) encNat encNat
-      (fun n => c * ((encNat n).length + 1)) (fun _ => c) := by
-  obtain ⟨cI, hI⟩ := computableInTimeAndSpace_of_const (encIn := encNat) (encOut := encBool) true
-  obtain ⟨⟨cN, hN⟩, ⟨cE, hE⟩⟩ := linear_parts
-  obtain ⟨cF, hF⟩ := linear_finalDigit
-  have hpair (p : Bool × Bool) : (encPair encBool encBool p).length = 4 := by simp
-  obtain ⟨c, h⟩ := ComputableTidilyInTimeAndSpace.streamFold (g := (· + 1)) (encOut := encNat)
-    digitReader (fun b => [b])
-    (fun _ => List.cons_ne_nil _ _) (fun a rest => by simp [digitReader, InputReader.read])
-    Nat.bits (fun n => by simp) hI.computableTidilyInTimeAndSpace hN hE hF
-    (fun n => by
-      change (n + 1).bits = _
-      rw [bits_succ, ← streamEmit_append_finalDigit]
-      rfl)
-    (tMax := fun _ => 5 * (cN + cE)) (sMax := fun _ => 5 * (cN + cE)) (lMax := fun _ => 4)
-    (fun _ _ _ => by simp only [hpair]; omega) (fun _ _ _ => by simp only [hpair]; omega)
-    (fun _ _ _ => by simp) (fun _ _ _ => by simp)
-  refine ⟨c * (2 * cI + 2 * cF + 5 * (cN + cE) + 20), h.mono (fun n => ?_) (fun n => ?_)⟩
-  · simp only [encBool_apply, List.length_singleton, encNat_apply]
-    rw [Nat.mul_assoc]
-    refine Nat.mul_le_mul_left c ?_
-    nlinarith
-  · simp only [encBool_apply, List.length_singleton]
-    exact Nat.mul_le_mul_left c (by omega)
-
-end Turing.MultiTapeTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean
index ffe6bb41e..38a816b7f 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean
@@ -8,21 +8,24 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops
-public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring
 
 /-!
 # Direct binary counter resource certificates
 
-The original carry, borrow and leading-zero normalization folds compute successor and predecessor.
-Their time is quadratic and their charged workspace linear in the binary input length. The zero
-test uses the existing empty-word machine. All round certificates are plain; normalization occurs
-only when the internal machine combinators construct the fold.
+The original borrow and leading-zero normalization folds compute the predecessor. Its time is
+quadratic and its charged workspace linear in the binary input length. The successor's
+certificate here is a weakening of the streaming transducer `computableInTimeAndSpace_succ`; the
+carry rounds remain as the shared step of binary addition. The zero test uses the existing
+empty-word machine. All round certificates are plain; normalization occurs only when the internal
+machine combinators construct the fold.
 
 ## Main results
 
-* `ComputableInO.succStep`, `ComputableInO.succFinish`: shared linear carry-round certificates.
+* `ComputableInO.succStep`, `ComputableInO.succFinish`: shared linear carry-round certificates
+  for binary addition.
 * `ComputableInO.natSucc`, `ComputableInO.natPred`: quadratic-time, linear-space binary counters.
 * `ComputableInO.natIsZero`: linear zero testing.
 -/
@@ -143,19 +146,13 @@ theorem foldl_bits {β : Type} {encB : β ↪ List Bool} {init : β} {step : β
   · simp only [encBits_apply]
     nlinarith
 
-/-- Binary successor with the original quadratic clock and linear output-charged workspace. -/
+/-- Binary successor within the quadratic clock and linear charged workspace used by its
+clients, weakened from the linear-time, zero-work-space transducer certificate
+`computableInTimeAndSpace_succ`. -/
 theorem natSucc :
     ComputableInO (· + 1) encNat encNat (fun n => ((encNat n).length + 1) ^ 2)
-      (fun n => (encNat n).length + 1) := by
-  have hfold := foldl_bits (init := (true, [])) succStep 3 fun l i => by
-    rw [NatSucc.length_encAcc, NatSucc.length_foldl_succStep]
-    simp only [List.length_nil, Nat.zero_add]
-    have := List.length_take_le' i l
-    omega
-  have h := (succFinish.comp_linear hfold).of_encIn_eq (encD := encNat) Nat.bits (fun _ => rfl)
-  refine h.of_enc_eq fun n => ?_
-  simp only [encNat_apply, encBits_apply, Function.comp_apply, NatSucc.succFinish_foldl,
-    List.nil_append, NatSucc.bits_succ]
+      (fun n => (encNat n).length + 1) :=
+  (of_linear .natSucc).mono_le (fun n => by simp only [encNat_apply]; nlinarith) fun _ => by omega
 
 /-- Binary predecessor keeps zero at zero and preserves the original independent resource bounds. -/
 theorem natPred :
diff --git a/ComplexityTests/Encodings.lean b/ComplexityTests/Encodings.lean
index a3b506811..91f45fb43 100644
--- a/ComplexityTests/Encodings.lean
+++ b/ComplexityTests/Encodings.lean
@@ -8,6 +8,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Encoding
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.ResourceFacts
 
 /-!
 # Tests for the framed encodings
@@ -27,10 +28,13 @@ example : encList encBool [true, false] = [true, true, false, true, false, false
 example (w u : List Bool) : unframe (frame w ++ u) = w := unframe_frame_append w u
 
 -- Binary successor can expose its raw output word with precisely the same time/space bounds.
-example : ∃ c, ComputableTidilyInTimeAndSpace (fun n : ℕ => encNat (n + 1)) encNat encBits
-    (fun n => c * ((encNat n).length + 1) ^ 2)
-    (fun n => c * ((encNat n).length + 1)) :=
-  let ⟨c, h⟩ := computableTidilyInTimeAndSpace_succ
-  ⟨c, h.of_enc_eq fun _ => rfl⟩
+example : ComputableInTimeAndSpace (fun n : ℕ => encNat (n + 1)) encNat encBits
+    (fun n => 2 * (encNat n).length + 3) (fun _ => 0) :=
+  let ⟨k, Q, hQ, tm, h⟩ := computableInTimeAndSpace_succ
+  ⟨k, Q, hQ, tm, h⟩
+
+-- The encoded successor, one digit longer after a carry out, is written within the linear clock.
+example (n : ℕ) : (encNat (n + 1)).length ≤ 2 * (encNat n).length + 3 :=
+  computableInTimeAndSpace_succ.length_le n
 
 end ComplexityTests.Encodings
diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json
index 51e1dd697..06f1c636d 100644
--- a/scripts/tidy_surface_baseline.json
+++ b/scripts/tidy_surface_baseline.json
@@ -50,9 +50,7 @@
  "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Translate.lean": 2,
  "Complexity/Computability/Machines/Turing/MultiTape/Encodings/Basic.lean": 7,
  "Complexity/Computability/Machines/Turing/MultiTape/Encodings/MultiPass.lean": 1,
- "Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean": 3,
  "Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatPower.lean": 1,
- "Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatStream.lean": 1,
  "Complexity/Computability/Machines/Turing/MultiTape/Encodings/StreamFold.lean": 4,
  "Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean": 5,
  "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 2,