diff --git a/Complexity.lean b/Complexity.lean
index 85d501bae2..951648520f 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1156,6 +1156,7 @@ public import Complexity.Computability.Complexity.Classes.CeqP.Time
 public import Complexity.Computability.Complexity.Classes.Constructible
 public import Complexity.Computability.Complexity.Classes.Constructible.Log
 public import Complexity.Computability.Complexity.Classes.Constructible.TwoPow
+public import Complexity.Computability.Complexity.Classes.Constructible.UnaryClock
 public import Complexity.Computability.Complexity.Classes.Counting.OracleSpace
 public import Complexity.Computability.Complexity.Classes.Counting.Space
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Accumulate
@@ -1308,6 +1309,7 @@ public import Complexity.Computability.Complexity.Classes.SharpP.GapMachine
 public import Complexity.Computability.Complexity.Classes.SharpP.Lowness
 public import Complexity.Computability.Complexity.Classes.SharpP.Machine
 public import Complexity.Computability.Complexity.Classes.SharpP.Oracle
+public import Complexity.Computability.Complexity.Classes.SharpP.PaddedCount
 public import Complexity.Computability.Complexity.Classes.SharpP.PolyTime
 public import Complexity.Computability.Complexity.Classes.SharpP.Power
 public import Complexity.Computability.Complexity.Classes.SharpP.Probability
@@ -1839,6 +1841,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Guess
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Oracle.Program
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Oracle.Replay
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.OutputPrefix
+public import Complexity.Computability.Machines.Turing.MultiTape.Counting.PaddedClock
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Program
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Sequential
 public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Verdict
@@ -2015,6 +2018,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.E
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.Table
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExplicitBlockNetwork.TablePolyTime
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ExtendTapes
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.HaltedReplay
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.InputFromTape
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalCount
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.IntervalCount.PolyTime
@@ -2944,6 +2948,7 @@ public import Complexity.Foundations.Data.Nat.CeilDiv
 public import Complexity.Foundations.Data.Nat.Choose
 public import Complexity.Foundations.Data.Nat.Choose.Real
 public import Complexity.Foundations.Data.Nat.Div
+public import Complexity.Foundations.Data.Nat.Doubling
 public import Complexity.Foundations.Data.Nat.Factorial
 public import Complexity.Foundations.Data.Nat.IntermediateValue
 public import Complexity.Foundations.Data.Nat.Log
diff --git a/Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean b/Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean
new file mode 100644
index 0000000000..c16cc6a9a7
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/Constructible/UnaryClock.lean
@@ -0,0 +1,177 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.Constructible
+public import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.OutputToTape
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Streaming
+import Complexity.Foundations.Data.Nat.Doubling
+import Complexity.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes
+import Complexity.Computability.Machines.Turing.MultiTape.Run
+
+/-!
+# Unary clocks of linear length from time-constructible bounds
+
+A time-constructible bound `T` is computed in binary within `O(T n)` steps
+(`Cslib.Complexity.TimeConstructible`). Some constructions need a clock in unary instead: a run of
+true cells on a work tape that a machine consumes one cell per step. Converting `T n` exactly
+from binary to unary by counting down takes `O((T n + 1) ^ 2)` steps
+(`Turing.MultiTapeTM.ComputableInO.natToUnary`), which is too slow for linear clocks.
+
+Rounding up to a power of two avoids the conversion. The binary word of `T n` has
+`Nat.size (T n)` digits, and doubling a unary counter once per digit writes
+`c * 2 ^ Nat.size (T n)` cells. The `i`-th doubling costs `O(c * 2 ^ i)`, so the doublings cost
+`O(c * 2 ^ Nat.size (T n)) = O(T n + 1)` together. The rounded clock lies between
+`c * (T n + 1)` and `c * (2 * T n + 1)` (`Nat.two_pow_size_le`).
+
+`Cslib.Complexity.TimeConstructible.exists_prepare_unaryClock` packages this as one deterministic
+machine that writes the clock on its last work tape within `O(T n)` steps, leaving every other
+work tape blank, its input head at the start and nothing emitted. This mirrors the polynomial
+budget of `MultiTape.Plumbing.PrepareClock`.
+
+## Main results
+
+* `Cslib.Complexity.TimeConstructible.exists_prepare_unaryClock`: a unary clock of
+  `c * 2 ^ Nat.size (T n)` cells within `O(T n)` steps.
+-/
+
+public section
+
+namespace Turing.MultiTapeTM.ComputableTidilyInO
+
+/-- The geometric sum of powers of two below `2 ^ n`. -/
+private theorem sum_range_two_pow_lt (n : ℕ) : ∑ i ∈ Finset.range n, 2 ^ i < 2 ^ n := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [Finset.sum_range_succ, pow_succ]
+    omega
+
+/-- **`c * 2 ^ l.length` in unary in linear time.** A streaming fold doubles a unary counter once
+per bit of `l`. Round `i` costs `O(c * 2 ^ i)`, so the rounds cost `O(c * 2 ^ l.length)` in total,
+plus `O(l.length)` for the scan. The tidy realization is private to this file; the public result
+is the plain preparation theorem below. -/
+private theorem mul_two_pow_length (c : ℕ) :
+    ComputableTidilyInO (fun l : List Bool => c * 2 ^ l.length) encBits encUnary
+      (fun l => c * 2 ^ l.length + l.length) fun l => c * 2 ^ l.length + l.length := by
+  obtain ⟨c₀, hstep, -⟩ := ((ComputableInDegree.unaryAdd (ComputableInDegree.fst encUnary encBool)
+    (ComputableInDegree.fst encUnary encBool) le_rfl le_rfl).inO_one).tidy
+  have hstate (l : List Bool) (i : ℕ) (hi : i ≤ l.length) :
+      (encUnary ((l.take i).foldl (fun m _ => m + m) c)).length = c * 2 ^ i := by
+    rw [List.foldl_add_self_eq_mul_two_pow, encUnary_apply, List.length_replicate, List.length_take,
+      Nat.min_eq_left hi]
+  obtain ⟨K, hK⟩ := ComputableTidilyInTimeAndSpace.foldl_bits_stream_sum (enc := encUnary)
+    (step := fun m (_ : Bool) => m + m) c hstep
+    (R := fun _ i => (5 * c₀ + 4) * (c * 2 ^ i + 1))
+    (Q := fun l => c₀ * (2 * (c * 2 ^ l.length) + 3))
+    (B := fun l => c * 2 ^ l.length)
+    (fun l i hi => by
+      have h₁ := hstate l i hi.le
+      have h₂ := hstate l (i + 1) hi
+      simp only [length_encPair, encBool_apply, List.length_singleton, h₁, h₂, pow_succ]
+      nlinarith)
+    (fun l i hi => by
+      have h₁ := hstate l i hi.le
+      have hpow : c * 2 ^ i ≤ c * 2 ^ l.length :=
+        Nat.mul_le_mul_left c (Nat.pow_le_pow_right (by norm_num) hi.le)
+      simp only [length_encPair, encBool_apply, List.length_singleton, h₁]
+      nlinarith)
+    (fun l i hi => by
+      rw [hstate l i hi]
+      exact Nat.mul_le_mul_left c (Nat.pow_le_pow_right (by norm_num) hi))
+  refine of_bounds (hK.of_enc_eq (g := fun l : List Bool => c * 2 ^ l.length)
+    fun l => by rw [List.foldl_add_self_eq_mul_two_pow])
+    (K * (5 * c₀ + 5) + K * (3 * c₀ + 3) + 1) (fun l => ?_) (fun l => ?_) fun l => ?_
+  · have hsum := sum_range_two_pow_lt l.length
+    have hs : ∑ i ∈ Finset.range l.length, (5 * c₀ + 4) * (c * 2 ^ i + 1) ≤
+        (5 * c₀ + 4) * (c * 2 ^ l.length + l.length) := by
+      rw [← Finset.mul_sum, Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_const,
+        Finset.card_range, smul_eq_mul, mul_one]
+      exact Nat.mul_le_mul_left _ (Nat.add_le_add_right (Nat.mul_le_mul_left c hsum.le) _)
+    have h₁ : ∑ i ∈ Finset.range l.length, (5 * c₀ + 4) * (c * 2 ^ i + 1) + c * 2 ^ l.length + 1
+        ≤ (5 * c₀ + 5) * (c * 2 ^ l.length + l.length + 1) := by
+      have e : (5 * c₀ + 5) * (c * 2 ^ l.length + l.length + 1) =
+          (5 * c₀ + 4) * (c * 2 ^ l.length + l.length) + (c * 2 ^ l.length + l.length) +
+            (5 * c₀ + 5) := by ring
+      rw [e]
+      omega
+    calc K * (∑ i ∈ Finset.range l.length, (5 * c₀ + 4) * (c * 2 ^ i + 1) + c * 2 ^ l.length + 1)
+        ≤ K * ((5 * c₀ + 5) * (c * 2 ^ l.length + l.length + 1)) := Nat.mul_le_mul_left K h₁
+      _ = K * (5 * c₀ + 5) * (c * 2 ^ l.length + l.length + 1) := by ring
+      _ ≤ _ := Nat.mul_le_mul_right _ (by omega)
+  · have h₁ : c₀ * (2 * (c * 2 ^ l.length) + 3) + c * 2 ^ l.length + 1 ≤
+        (3 * c₀ + 3) * (c * 2 ^ l.length + l.length + 1) := by
+      have e : (3 * c₀ + 3) * (c * 2 ^ l.length + l.length + 1) =
+          c₀ * (2 * (c * 2 ^ l.length) + 3) + c₀ * (c * 2 ^ l.length) + 3 * c₀ * l.length +
+            3 * (c * 2 ^ l.length + l.length + 1) := by ring
+      rw [e]
+      omega
+    calc K * (c₀ * (2 * (c * 2 ^ l.length) + 3) + c * 2 ^ l.length + 1)
+        ≤ K * ((3 * c₀ + 3) * (c * 2 ^ l.length + l.length + 1)) := Nat.mul_le_mul_left K h₁
+      _ = K * (3 * c₀ + 3) * (c * 2 ^ l.length + l.length + 1) := by ring
+      _ ≤ _ := Nat.mul_le_mul_right _ (by omega)
+  · simp only [encUnary_apply, List.length_replicate]
+    calc c * 2 ^ l.length ≤ 1 * (c * 2 ^ l.length + l.length + 1) := by omega
+      _ ≤ _ := Nat.mul_le_mul_right _ (by omega)
+
+end Turing.MultiTapeTM.ComputableTidilyInO
+
+namespace Cslib.Complexity
+
+open Turing Turing.MultiTapeTM
+
+/-- **A unary clock of linear length.** For a time-constructible `T` and a constant `c`, one
+deterministic machine with finitely many states writes `c * 2 ^ Nat.size (T n)` true cells on its
+last work tape within `C * T n + C` steps, on every input of length `n`. It halts with every other
+work tape blank, all heads at their starting cells and nothing emitted. The clock has between
+`c * (T n + 1)` and `c * (2 * T n + 1)` cells (`Nat.lt_size_self`, `Nat.two_pow_size_le`). -/
+theorem TimeConstructible.exists_prepare_unaryClock {T : ℕ → ℕ} (hT : TimeConstructible T)
+    (c : ℕ) :
+    ∃ (r : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeTM (r + 1) Bool State)
+      (C : ℕ), ∀ input,
+      machine.runFrom (machine.initCfg input) (C * T input.length + C) =
+        wordsCfg input none (Function.update (fun _ => []) (Fin.last r)
+          (List.replicate (c * 2 ^ Nat.size (T input.length)) true)) [] := by
+  have hbits : ComputableTidilyInO (fun x : List Bool => encNat (T x.length)) encBits encBits
+      (fun x => T x.length) fun x => T x.length :=
+    hT.computableInO.tidy.of_enc_eq fun _ => rfl
+  have hclock := ((ComputableTidilyInO.mul_two_pow_length c).comp hbits).of_enc_eq
+    (g := fun x : List Bool => List.replicate (c * 2 ^ Nat.size (T x.length)) true)
+    (encOut := encBits) fun x => by
+      simp [encUnary_apply, encNat_apply, Nat.size_eq_bits_len]
+  have hdigits (m : ℕ) : (encNat m).length = Nat.size m := by
+    rw [encNat_apply, Nat.size_eq_bits_len]
+  have hlinear (x : List Bool) : T x.length + (c * 2 ^ (encNat (T x.length)).length +
+      (encNat (T x.length)).length) ≤ (2 * c + 2) * (T x.length + 1) := by
+    have h₁ := Nat.mul_le_mul_left c (Nat.two_pow_size_le (T x.length))
+    have h₂ : Nat.size (T x.length) ≤ T x.length := Nat.size_le.mpr Nat.lt_two_pow_self
+    rw [hdigits]
+    have e : (2 * c + 2) * (T x.length + 1) = c * (2 * T x.length + 1) + c +
+        2 * (T x.length + 1) := by ring
+    rw [e]
+    omega
+  obtain ⟨c₁, ⟨r, State, hfinite, machine, hmachine⟩, -⟩ := hclock.mono (2 * c + 2)
+    (T' := fun x => T x.length) (S' := fun x => T x.length) hlinear hlinear
+  refine ⟨r, State ⊕ RewindWorkState, inferInstance, machine.outputToWord, c₁ + 2 * c + 2,
+    fun input => ?_⟩
+  have hbound : c₁ * (T input.length + 1) +
+      (List.replicate (c * 2 ^ Nat.size (T input.length)) true).length + 2 ≤
+      (c₁ + 2 * c + 2) * T input.length + (c₁ + 2 * c + 2) := by
+    have h₁ := Nat.mul_le_mul_left c (Nat.two_pow_size_le (T input.length))
+    rw [List.length_replicate]
+    have e : (c₁ + 2 * c + 2) * T input.length + (c₁ + 2 * c + 2) =
+        c₁ * (T input.length + 1) + c * (2 * T input.length + 1) + c + 2 * T input.length + 2 := by
+      ring
+    rw [e]
+    omega
+  have hwrite := (hmachine input).outputToWord.mono hbound le_rfl
+  obtain ⟨_, _, hrun, ⟨rfl, rfl⟩, _⟩ :=
+    transformsTapes_iff_runFrom.mp hwrite input (fun _ => []) [] ⟨rfl, rfl⟩
+  simpa only [initCfg_eq_wordsCfg, encBits_apply, List.nil_append] using hrun
+
+end Cslib.Complexity
diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean
index 8a12ca07ad..501c963b1d 100644
--- a/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean
+++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/CountingClasses.lean
@@ -11,8 +11,10 @@ public import Complexity.Computability.Complexity.Classes.CeqP.Time
 public import Complexity.Computability.Complexity.Classes.CountingSimulation.Separation
 public import Complexity.Computability.Complexity.Classes.ModP.Time
 import Complexity.Computability.Complexity.Classes.FunctionTime.Decide
+import Complexity.Computability.Complexity.Classes.SharpP.PaddedCount
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeBinaryDivision
 
 /-!
@@ -37,9 +39,14 @@ the containments and strict containments of `Cslib.Complexity.ParityTIME`,
 `Cslib.Complexity.ModTIME` (for every fixed `k`) and `Cslib.Complexity.CeqTIME`. The bounds are on
 time only; no polynomial workspace bound is claimed for these classes.
 
-`NTIME`, `BPTIME` and `PPTIME` reduce in this library to counts of padded fair-coin strings
-(`Cslib.Complexity.exists_acceptCount_of_mem_NTIME`), not to terminal-path counts, so they are not
-derived here. Their strict containments in `DTIME[2 ^ T]` are in `CountingSimulation.Separation`.
+`NTIME`, `BPTIME` and `PPTIME` are such classes too. The library reduces them to padded fair-coin
+counts (`Cslib.Complexity.exists_acceptCount_of_mem_NTIME`), and padded counts at a linear clock
+are `SharpTIME enc T` functions (`Cslib.Complexity.exists_clock_acceptCount_mem_SharpTIME`).
+So `NTIME[T]` is a positivity test of one count, and `PPTIME[T]` and `BPTIME[T]` compare a count
+`f` with the count `g = 2 ^ τ` of all coin strings by `g < 2 * f`
+(`Cslib.Complexity.exists_mem_SharpTIME_of_mem_NTIME`,
+`Cslib.Complexity.exists_mem_SharpTIME_of_mem_PPTIME`). Their strict containments in
+`DTIME[2 ^ T]` are instances of the same separation.
 
 ## Main results
 
@@ -52,6 +59,8 @@ derived here. Their strict containments in `DTIME[2 ^ T]` are in `CountingSimula
   `CeqTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two`: the containments.
 * `ParityTIME_ssubset_DTIME_two_pow`, `ModTIME_ssubset_DTIME_two_pow`,
   `CeqTIME_ssubset_DTIME_two_pow`: the strict containments in `DTIME[2 ^ T]`.
+* `NTIME_ssubset_DTIME_two_pow`, `BPTIME_ssubset_DTIME_two_pow`, `PPTIME_ssubset_DTIME_two_pow`:
+  the strict containments of nondeterministic, bounded-error and majority time.
 
 ## References
 
@@ -194,4 +203,52 @@ theorem CeqTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, m
     CeqTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n :=
   ssubset_DTIME_two_pow_of_forall_mem_SharpTIME hT hTn fun _ => CeqTIME_forall_mem_SharpTIME
 
+/-! ### Nondeterministic, bounded-error and majority time -/
+
+private theorem computableInPolyTime_pos :
+    ComputableInPolyTime (fun p : ℕ × ℕ => decide (0 < p.1)) (encPair encNat encNat) encBool :=
+  ComputableInPolyTime.binary_lt' (ComputableInPolyTime.const 0)
+    (ComputableInPolyTime.fst encNat encNat)
+
+private theorem computableInPolyTime_lt_two_mul :
+    ComputableInPolyTime (fun p : ℕ × ℕ => decide (p.2 < 2 * p.1)) (encPair encNat encNat)
+      encBool :=
+  ComputableInPolyTime.binary_lt' (ComputableInPolyTime.snd encNat encNat)
+    (ComputableInPolyTime.binary_mul' (ComputableInPolyTime.const 2)
+      (ComputableInPolyTime.fst encNat encNat))
+
+/-- `NTIME[T]` problems are decided by tests of counts in `SharpTIME enc T`. -/
+private theorem NTIME_forall_mem_SharpTIME (hT : TimeConstructible T) {A : Set α}
+    (hA : A ∈ NTIME enc T) :
+    ∃ f ∈ SharpTIME enc T, ∃ g ∈ SharpTIME enc T, ∃ rule : ℕ × ℕ → Bool,
+      ComputableInPolyTime rule (encPair encNat encNat) encBool ∧
+        ∀ x, x ∈ A ↔ rule (f x, g x) = true := by
+  obtain ⟨f, hf, hA⟩ := exists_mem_SharpTIME_of_mem_NTIME hT hA
+  exact ⟨f, hf, f, hf, _, computableInPolyTime_pos, fun x => by simp [hA x]⟩
+
+/-- `PPTIME[T]` problems are decided by tests of counts in `SharpTIME enc T`. -/
+private theorem PPTIME_forall_mem_SharpTIME (hT : TimeConstructible T) {A : Set α}
+    (hA : A ∈ PPTIME enc T) :
+    ∃ f ∈ SharpTIME enc T, ∃ g ∈ SharpTIME enc T, ∃ rule : ℕ × ℕ → Bool,
+      ComputableInPolyTime rule (encPair encNat encNat) encBool ∧
+        ∀ x, x ∈ A ↔ rule (f x, g x) = true := by
+  obtain ⟨f, hf, g, hg, hA⟩ := exists_mem_SharpTIME_of_mem_PPTIME hT hA
+  exact ⟨f, hf, g, hg, _, computableInPolyTime_lt_two_mul, fun x => by simp [hA x]⟩
+
+/-- **`NTIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/
+theorem NTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) :
+    NTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n :=
+  ssubset_DTIME_two_pow_of_forall_mem_SharpTIME hT hTn fun _ => NTIME_forall_mem_SharpTIME hT
+
+/-- **`BPTIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/
+theorem BPTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) :
+    BPTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n :=
+  ssubset_DTIME_two_pow_of_forall_mem_SharpTIME hT hTn fun _ hA =>
+    PPTIME_forall_mem_SharpTIME hT (BPTIME_subset_PPTIME hA)
+
+/-- **`PPTIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/
+theorem PPTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) :
+    PPTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n :=
+  ssubset_DTIME_two_pow_of_forall_mem_SharpTIME hT hTn fun _ => PPTIME_forall_mem_SharpTIME hT
+
 end Cslib.Complexity.CountingSimulation
diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean
index 10dc7f6852..9815e49cd0 100644
--- a/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean
+++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Separation.lean
@@ -15,11 +15,10 @@ import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
 /-!
 # Strict containments in `DTIME[2 ^ T]` from the counting simulation
 
-For time-constructible `T` with `max n 2 ≤ T n`, the counting simulation of #1833 places
-`NTIME[T]`, `BPTIME[T]` and `PPTIME[T]` in `⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`
-(`Cslib.Complexity.CountingSimulation.NTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two` and its
-siblings). That union lies in `DTIME[2 ^ T]` but does not exhaust it. Hence each of these classes
-is strictly contained in `DTIME[2 ^ T]` on bit strings.
+For time-constructible `T` with `max n 2 ≤ T n`, the counting simulation of #1833 places counting
+classes such as `NTIME[T]`, `BPTIME[T]` and `PPTIME[T]` in
+`⋃ C, DTIME[2 ^ (C T / √⌊log₂ T⌋)]`. That union lies in `DTIME[2 ^ T]` but does not exhaust it.
+Hence every class inside it is strictly contained in `DTIME[2 ^ T]` on bit strings.
 
 **The separating language** is the clocked diagonal `Cslib.Complexity.timeDiagonal J` of
 `Complexity.Computability.Complexity.Classes.Hierarchy.Time`, with the clock
@@ -36,9 +35,10 @@ is strictly contained in `DTIME[2 ^ T]` on bit strings.
 The polynomial overhead of the native universal machine is absorbed by the gap between
 `2 ^ (T / 4)` and `2 ^ T`. No faster universal simulation is assumed.
 
-The same separation applies to every class decided by polynomial-time tests of exact counts in
-`Cslib.Complexity.SharpTIME`, such as `⊕TIME[T]`, `Mod_kTIME[T]` and `C₌TIME[T]`
-(`Complexity.Computability.Complexity.Classes.CountingSimulation.CountingClasses`).
+The separation is applied in
+`Complexity.Computability.Complexity.Classes.CountingSimulation.CountingClasses` to every class
+decided by polynomial-time tests of exact counts in `Cslib.Complexity.SharpTIME`: `⊕TIME[T]`,
+`Mod_kTIME[T]`, `C₌TIME[T]`, and also `NTIME[T]`, `BPTIME[T]` and `PPTIME[T]`.
 
 ## Main results
 
@@ -48,8 +48,6 @@ The same separation applies to every class decided by polynomial-time tests of e
   `DTIME[2 ^ T]` lies outside every `DTIME[2 ^ (C T / √⌊log₂ T⌋)]`.
 * `Cslib.Complexity.CountingSimulation.ssubset_DTIME_two_pow_of_subset_iUnion`: every class inside
   the union is strictly contained in `DTIME[2 ^ T]`.
-* `Cslib.Complexity.CountingSimulation.NTIME_ssubset_DTIME_two_pow`,
-  `BPTIME_ssubset_DTIME_two_pow`, `PPTIME_ssubset_DTIME_two_pow`: the strict containments.
 
 ## References
 
@@ -156,25 +154,4 @@ theorem ssubset_DTIME_two_pow_of_subset_iUnion {𝒞 : Set (Set (List Bool))}
   ⟨h.trans (iUnion_DTIME_two_pow_div_sqrt_log_two_subset hTn), fun hsub =>
     DTIME_two_pow_not_subset_iUnion_DTIME_two_pow_div_sqrt_log_two hT hTn (hsub.trans h)⟩
 
-private theorem le_of_max_le (hTn : ∀ n, max n 2 ≤ T n) (n : ℕ) : n ≤ T n :=
-  (le_max_left _ _).trans (hTn n)
-
-/-- **`NTIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/
-theorem NTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) :
-    NTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n :=
-  ssubset_DTIME_two_pow_of_subset_iUnion hT (le_of_max_le hTn)
-    (NTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two hT hTn)
-
-/-- **`BPTIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/
-theorem BPTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) :
-    BPTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n :=
-  ssubset_DTIME_two_pow_of_subset_iUnion hT (le_of_max_le hTn)
-    (BPTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two hT hTn)
-
-/-- **`PPTIME[T] ⊊ DTIME[2 ^ T]`** for time-constructible `T` with `max n 2 ≤ T n`. -/
-theorem PPTIME_ssubset_DTIME_two_pow (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) :
-    PPTIME encBits T ⊂ DTIME encBits fun n => 2 ^ T n :=
-  ssubset_DTIME_two_pow_of_subset_iUnion hT (le_of_max_le hTn)
-    (PPTIME_subset_iUnion_DTIME_two_pow_div_sqrt_log_two hT hTn)
-
 end Cslib.Complexity.CountingSimulation
diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean
index a1f91e687b..2a206c82a4 100644
--- a/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean
+++ b/Complexity/Computability/Complexity/Classes/LogSpace/Randomized.lean
@@ -11,6 +11,7 @@ public import Complexity.Computability.Complexity.Classes.LogSpace
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.HaltingTime
 public import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Deterministic
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.HaltedReplay
 
 /-!
 # Randomized logarithmic space
@@ -84,18 +85,6 @@ noncomputable def acceptCoins (input : List Bool) (t : ℕ) : ℕ :=
 theorem acceptCoins_le (input : List Bool) (t : ℕ) : machine.acceptCoins input t ≤ 2 ^ t :=
   (Finset.card_filter_le _ _).trans (by simp)
 
-/-- A halted configuration ignores its coin. -/
-theorem step_withCoin_of_halted {input : List Bool} {c : Cfg k Bool State input} (h : c.Halted)
-    (bit : Bool) : (machine.withCoin bit).toTM.step c = c :=
-  MultiTapeTM.step_iff.mp ((MultiTapeNTM.step_of_halt h).mpr rfl)
-
-/-- A halted configuration ignores any further coins. -/
-theorem stepCoins_of_halted {input : List Bool} {c : Cfg k Bool State input} (h : c.Halted)
-    (coins : List Bool) : machine.stepCoins coins c = c := by
-  induction coins with
-  | nil => rfl
-  | cons bit coins ih => rw [stepCoins_cons, step_withCoin_of_halted machine h, ih]
-
 /-- Under a time bound `t`, every replay of `t` or more coins ends halted. -/
 theorem halted_stepCoins {input : List Bool} {t : ℕ} (ht : machine.toNTM.RunsInTime input t)
     {coins : List Bool} (hlen : t ≤ coins.length) :
diff --git a/Complexity/Computability/Complexity/Classes/SharpP/PaddedCount.lean b/Complexity/Computability/Complexity/Classes/SharpP/PaddedCount.lean
new file mode 100644
index 0000000000..25023433ed
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/SharpP/PaddedCount.lean
@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Complexity.Classes.Constructible
+public import Complexity.Computability.Complexity.Classes.PP.Time
+public import Complexity.Computability.Complexity.Classes.SharpP.Time
+public import Complexity.Computability.Complexity.Classes.Time.AcceptCount
+import Complexity.Computability.Complexity.Classes.Constructible.UnaryClock
+import Complexity.Computability.Machines.Turing.MultiTape.Counting.PaddedClock
+import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic
+import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.HaltedReplay
+import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.PolynomialClock
+import Complexity.Foundations.Data.Nat.Doubling
+
+/-!
+# Padded coin counts in time-bounded counting
+
+The library reduces nondeterministic, bounded-error and majority time to the padded accepting
+count of a fair-coin machine (`Turing.MultiTapePTM.acceptCount`): the number of coin strings of a
+length `τ` whose replay outputs `[true]`, where a run that halts early ignores its remaining coins
+(`Cslib.Complexity.exists_acceptCount_of_mem_NTIME`,
+`Cslib.Complexity.exists_acceptCount_of_mem_BPTIME`,
+`Turing.MultiTapePTM.decidesByMajorityInTime_iff`). `Cslib.Complexity.SharpTIME` counts accepting
+terminal branches of native counting machines instead, without padding.
+
+For a time-constructible `T`, padded counts at a linear clock are `SharpTIME enc T` functions
+(`Cslib.Complexity.exists_clock_acceptCount_mem_SharpTIME`). The clock is
+`τ n = c * 2 ^ Nat.size (T n)`, which lies between `c * (T n + 1)` and `c * (2 * T n + 1)`. A
+deterministic phase writes it in unary within `O(T n)` steps
+(`Cslib.Complexity.TimeConstructible.exists_prepare_unaryClock`). The counting machine
+`Turing.MultiTapeCTM.PaddedClock.machine` then branches once per coin, continuing after the source
+halts, until the clock is exhausted. The clock is chosen before the machine, so several counts
+can share it. A clock exactly `c₁ * T n + c₂` would need an exact binary-to-unary conversion in
+linear time; the rounded clock suffices below, because each characterization holds at every
+clock of at least `c₁ * T n + c₂`.
+
+Hence:
+
+* `NTIME[T]` problems are positivity tests of one `SharpTIME[T]` count
+  (`Cslib.Complexity.exists_mem_SharpTIME_of_mem_NTIME`).
+* `PPTIME[T]` and `BPTIME[T]` problems are comparisons `g a < 2 * f a` of two `SharpTIME[T]`
+  counts, where `g a = 2 ^ τ` is the count of a machine accepting every coin string
+  (`Cslib.Complexity.exists_mem_SharpTIME_of_mem_PPTIME`,
+  `Cslib.Complexity.exists_mem_SharpTIME_of_mem_BPTIME`).
+
+The converse direction, from terminal counts to padded counts, is
+`Turing.MultiTapeCTM.CountingChoice.acceptCount_table_of_halts`.
+
+## Main results
+
+* `Cslib.Complexity.exists_clock_acceptCount_mem_SharpTIME`: padded counts at a linear clock.
+* `Cslib.Complexity.exists_mem_SharpTIME_of_mem_NTIME`,
+  `Cslib.Complexity.exists_mem_SharpTIME_of_mem_PPTIME`,
+  `Cslib.Complexity.exists_mem_SharpTIME_of_mem_BPTIME`: the class-level count tests.
+-/
+
+public section
+
+namespace Cslib.Complexity
+
+open _root_.Turing
+
+variable {α : Type} {enc : α ↪ List Bool} {T : ℕ → ℕ} {A : Set α}
+
+/-- **Padded counts at a linear clock are time-bounded terminal counts.** For a time-constructible
+`T` and constants `c₁` and `c₂`, there is a clock `τ` with `c₁ * T n + c₂ ≤ τ n ≤ C * T n + C`
+such that, for every fair-coin machine `M` with a binary alphabet and finitely many states, the
+padded accepting count of `M` with `τ` coins lies in `SharpTIME enc T`. The clock does not depend
+on `M`. -/
+theorem exists_clock_acceptCount_mem_SharpTIME (hT : TimeConstructible T) (c₁ c₂ : ℕ) :
+    ∃ τ : ℕ → ℕ, (∀ n, c₁ * T n + c₂ ≤ τ n) ∧ (∃ C, ∀ n, τ n ≤ C * T n + C) ∧
+      ∀ {k : ℕ} {State : Type} [Finite State] (M : MultiTapePTM k Bool State),
+        (fun a => M.acceptCount (enc a) (τ (enc a).length)) ∈ SharpTIME enc T := by
+  obtain ⟨r, P, hP, prepare, C, hprepare⟩ := hT.exists_prepare_unaryClock (c₁ + c₂)
+  have hupper (n : ℕ) : (c₁ + c₂) * 2 ^ Nat.size (T n) ≤
+      2 * (c₁ + c₂) * T n + 2 * (c₁ + c₂) := by
+    have := Nat.mul_le_mul_left (c₁ + c₂) (Nat.two_pow_size_le (T n))
+    have e : 2 * (c₁ + c₂) * T n + 2 * (c₁ + c₂) =
+        (c₁ + c₂) * (2 * T n + 1) + (c₁ + c₂) := by ring
+    omega
+  refine ⟨fun n => (c₁ + c₂) * 2 ^ Nat.size (T n), fun n => ?_, ⟨2 * (c₁ + c₂), hupper⟩,
+    fun {k State} _ M => ?_⟩
+  · have h : (c₁ + c₂) * (T n + 1) ≤ (c₁ + c₂) * 2 ^ Nat.size (T n) :=
+      Nat.mul_le_mul_left _ (Nat.lt_size_self _)
+    have e : (c₁ + c₂) * (T n + 1) = c₁ * T n + c₂ + (c₂ * T n + c₁) := by ring
+    rw [e] at h
+    change c₁ * T n + c₂ ≤ (c₁ + c₂) * 2 ^ Nat.size (T n)
+    omega
+  · let compiled := MultiTapeCTM.PaddedClock.compile M (prepare.extendTapes (Fin.natAddEmb k))
+    refine ⟨C + 2 * (c₁ + c₂), C + 2 * (c₁ + c₂) + 1, k + r + 1, P ⊕ Option State,
+      inferInstance, compiled, MultiTapeCTM.PaddedClock.nonblocking_compile _ _, fun a => ?_⟩
+    have hready := MultiTapePTM.PolynomialClock.prepare_runFrom (k := k) prepare (enc a)
+      (List.replicate ((c₁ + c₂) * 2 ^ Nat.size (T (enc a).length)) true)
+      (C * T (enc a).length + C) (hprepare (enc a))
+    obtain ⟨hhalt, hcount⟩ := MultiTapeCTM.PaddedClock.haltsWithin_acceptCount_compile M
+      (prepare.extendTapes (Fin.natAddEmb k)) (enc a) _ _ hready
+    have hle : C * T (enc a).length + C + ((c₁ + c₂) * 2 ^ Nat.size (T (enc a).length) + 1) ≤
+        (C + 2 * (c₁ + c₂)) * T (enc a).length + (C + 2 * (c₁ + c₂) + 1) := by
+      have := hupper (enc a).length
+      have e : (C + 2 * (c₁ + c₂)) * T (enc a).length + (C + 2 * (c₁ + c₂) + 1) =
+          C * T (enc a).length + C + (2 * (c₁ + c₂) * T (enc a).length + 2 * (c₁ + c₂)) + 1 := by
+        ring
+      omega
+    refine ⟨hhalt.mono hle, ?_⟩
+    change compiled.branchCount (· == [true]) _ _ = _
+    rw [hhalt.branchCount_eq hle]
+    exact hcount
+
+/-- **`NTIME[T]` as a positive count.** For a time-constructible `T`, every problem in
+`NTIME enc T` consists of the instances with a positive count `f a`, for some `f` in
+`SharpTIME enc T`. -/
+theorem exists_mem_SharpTIME_of_mem_NTIME (hT : TimeConstructible T) (hA : A ∈ NTIME enc T) :
+    ∃ f ∈ SharpTIME enc T, ∀ a, a ∈ A ↔ 0 < f a := by
+  obtain ⟨k, State, _, M, c₁, c₂, hM⟩ := exists_acceptCount_of_mem_NTIME hA
+  obtain ⟨τ, hτ, -, hmem⟩ := exists_clock_acceptCount_mem_SharpTIME (enc := enc) hT c₁ c₂
+  exact ⟨_, hmem M, fun a => hM a _ (hτ _)⟩
+
+/-- **`PPTIME[T]` as a comparison of two counts.** For a time-constructible `T`, every problem in
+`PPTIME enc T` consists of the instances with `g a < 2 * f a`, for some `f` and `g` in
+`SharpTIME enc T`. Here `f` counts accepting coin strings at a common linear clock `τ` and
+`g a = 2 ^ τ` counts all of them. -/
+theorem exists_mem_SharpTIME_of_mem_PPTIME (hT : TimeConstructible T) (hA : A ∈ PPTIME enc T) :
+    ∃ f ∈ SharpTIME enc T, ∃ g ∈ SharpTIME enc T, ∀ a, a ∈ A ↔ g a < 2 * f a := by
+  obtain ⟨c₁, c₂, k, State, _, M, hM⟩ := hA
+  obtain ⟨τ, hτ, -, hmem⟩ := exists_clock_acceptCount_mem_SharpTIME (enc := enc) hT c₁ (c₂ + 1)
+  refine ⟨_, hmem M, _, hmem MultiTapePTM.acceptAll, fun a => ?_⟩
+  have hdecide := MultiTapePTM.decidesByMajorityInTime_iff.mp
+    (hM.mono (t' := fun a => τ (enc a).length) fun a => (Nat.le_succ _).trans (hτ _)) a
+  obtain ⟨m, hm⟩ : ∃ m, τ (enc a).length = m + 1 :=
+    Nat.exists_eq_add_one.mpr (Nat.lt_of_lt_of_le (Nat.succ_pos _) (hτ _))
+  rw [hdecide.2]
+  change _ ↔ MultiTapePTM.acceptAll.acceptCount (enc a) (τ (enc a).length) < _
+  rw [hm, MultiTapePTM.acceptCount_acceptAll]
+
+/-- **`BPTIME[T]` as a comparison of two counts**, through `Cslib.Complexity.BPTIME_subset_PPTIME`.
+-/
+theorem exists_mem_SharpTIME_of_mem_BPTIME (hT : TimeConstructible T) (hA : A ∈ BPTIME enc T) :
+    ∃ f ∈ SharpTIME enc T, ∃ g ∈ SharpTIME enc T, ∀ a, a ∈ A ↔ g a < 2 * f a :=
+  exists_mem_SharpTIME_of_mem_PPTIME hT (BPTIME_subset_PPTIME hA)
+
+end Cslib.Complexity
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram/Unary.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram/Unary.lean
index e23bd6f327..5ffb28cc68 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram/Unary.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram/Unary.lean
@@ -11,6 +11,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogS
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame
+import Complexity.Foundations.Data.Nat.Doubling
 import Mathlib.Data.List.GetD
 import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Size
@@ -155,14 +156,6 @@ private theorem bits_eq_map_testBit (v : ℕ) : v.bits = (List.range v.size).map
   refine List.ext_getElem (by simp [Nat.size_eq_bits_len]) fun i h _ => ?_
   simp [Nat.testBit_eq_inth, List.getI_eq_getElem _ h]
 
-private theorem two_pow_size_le (v : ℕ) : 2 ^ v.size ≤ 2 * v + 1 := by
-  rcases Nat.eq_zero_or_pos v with rfl | hv
-  · simp
-  · obtain ⟨s, hs⟩ : ∃ s, v.size = s + 1 := ⟨v.size - 1, by have := Nat.size_pos.mpr hv; omega⟩
-    have : 2 ^ s ≤ v := Nat.lt_size.mp (by omega)
-    rw [hs, pow_succ]
-    omega
-
 /-- The loop of `binaryProgram`, from the power `2 ^ i`, emits the bits of `v` from index `i` on
 below its size. -/
 private theorem reachesOut_binaryLoop (e : Expr) {v : ℕ} (hB : 2 * a + 1 + b ≤ B)
@@ -170,7 +163,7 @@ private theorem reachesOut_binaryLoop (e : Expr) {v : ℕ} (hB : 2 * a + 1 + b 
     ∀ i ≤ v.size, (binaryProgram e).ReachesOut (encPair encUnary encUnary (a, b))
       ((binaryProgram e).Active B) (6, [a, b, 2 ^ i, v]) (11, [a, b, 2 ^ v.size, v])
       ((List.range' i (v.size - i)).map v.testBit) := by
-  have hsize := two_pow_size_le v
+  have hsize := Nat.two_pow_size_le v
   intro i hi
   induction h : v.size - i generalizing i with
   | zero =>
@@ -266,7 +259,7 @@ theorem computableInLogSpace_binary (e : Expr) (d : ℕ) (he : ∀ a b, e.eval [
   rw [length_input]
   obtain ⟨h₁, h₂⟩ := le_pow_add_two (n := 2 * a + 1 + b) (by omega)
     ((hF a b).trans (Nat.pow_le_pow_left (by omega) d))
-  have hsize := two_pow_size_le (F a b)
+  have hsize := Nat.two_pow_size_le (F a b)
   refine ⟨_, _, [], reachesOut_binaryProgram e (he a b) (by omega) h₂, rfl,
     by simp [encNat_apply], bounded4 (by omega) (by omega) (by omega) (by omega)⟩
 
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean
index aac57a6a72..c225959c22 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean
@@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.Equali
 public import Mathlib.Tactic.FunProp
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition
+import Complexity.Foundations.Data.Nat.Doubling
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring
@@ -688,11 +689,7 @@ theorem lengthUnary : ComputableInO (fun l : List Bool => l.length) encBits encU
 /-- Doubling `m` once for each element of a list of length `n` multiplies it by `2 ^ n`. -/
 private theorem foldl_double (n m : ℕ) :
     (List.replicate n true).foldl (fun m _ => m + m) m = m * 2 ^ n := by
-  induction n generalizing m with
-  | zero => simp
-  | succ n ih =>
-    rw [List.replicate_succ, List.foldl_cons, ih]
-    ring
+  rw [List.foldl_add_self_eq_mul_two_pow, List.length_replicate]
 
 /-- **`2 ^ n` in unary**, by doubling `n` times, within time `O((n + 1) * 2 ^ n)` and space
 `O(2 ^ n)`. -/
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean b/Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean
new file mode 100644
index 0000000000..871b6e5525
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Counting/PaddedClock.lean
@@ -0,0 +1,352 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Deterministic
+public import Complexity.Computability.Machines.Turing.MultiTape.Counting.Sequential
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount
+import Complexity.Computability.Machines.Turing.MultiTape.Machine.Nondeterministic
+
+/-!
+# Padded coin counts as terminal-path counts
+
+A closed fair-coin table counts the coin strings of a fixed length `τ` on which it outputs
+`[true]` (`Turing.MultiTapePTM.acceptCount`). A run that halts early ignores its remaining coins,
+so an accepting run of length `ℓ` contributes `2 ^ (τ - ℓ)` strings. A native counting machine
+counts each terminal branch once (`Turing.MultiTapeCTM.acceptCount`).
+
+`Turing.MultiTapeCTM.PaddedClock.machine` turns the first count into the second. It keeps the
+source tapes on its first `k` work tapes and a unary clock on its last work tape. While the
+clock head reads `true`, it takes one of two transition occurrences, one per coin: it performs
+the source action selected by that coin and advances the clock head. After the source halts, the
+two occurrences only advance the clock. On the first cell that does not hold `true`, it halts
+with a single occurrence and emits nothing. Thus a clock of `τ` cells has exactly one terminal
+branch for each coin string of length `τ`, and that branch ends with the output of the coin
+replay.
+
+`Turing.MultiTapeCTM.PaddedClock.compile` precedes this machine by a deterministic phase that
+writes `τ` true cells on the clock tape and leaves every other tape blank. The time and
+correctness of that phase are hypotheses here; the clock is prepared from a time-constructible
+bound in `Complexity.Computability.Complexity.Classes.Constructible.UnaryClock`.
+
+## Main definitions
+
+* `Turing.MultiTapeCTM.PaddedClock.machine`: count coin strings under a prepared unary clock.
+* `Turing.MultiTapeCTM.PaddedClock.compile`: prepare the clock, then count.
+
+## Main results
+
+* `Turing.MultiTapeCTM.PaddedClock.haltsWithin_acceptCount_machine`: a clock of `n` cells halts
+  every branch within `n + 1` steps and counts the coin strings of length `n`.
+* `Turing.MultiTapeCTM.PaddedClock.haltsWithin_acceptCount_compile`: after a preparation of
+  `time` steps writing `τ` cells, every branch halts within `time + (τ + 1)` steps and the
+  terminal accepting count is the padded accepting count at `τ`.
+
+## References
+
+The unary clock tape follows `MultiTape.Machine.Clock`, whose controller does not pad halted
+runs with branching choices.
+-/
+
+public section
+
+namespace Turing.MultiTapeCTM.PaddedClock
+
+open Cslib MultiTapeMachine
+
+variable {k r : ℕ} {State : Type} {input : List Bool}
+
+/-- The source action selected by a coin at a running source state. -/
+def coinAction (M : MultiTapePTM k Bool State) (state : State) (symbol : Option Bool)
+    (work : Fin k → Option Bool) (bit : Bool) : Turing.Action k Bool State :=
+  Action.emptyOracleEquiv (M.tr state symbol work Empty.elim bit)
+
+/-- A source action on the first `k` work tapes, advancing the clock head on the last one. -/
+def lift (action : Turing.Action k Bool State) :
+    Turing.Action (k + r + 1) Bool (Option State) where
+  inputTape := action.inputTape
+  workTapes := Fin.lastCases (none, 1) (Fin.addCases action.workTapes fun _ => (none, 0))
+  output := action.output
+  state := some action.state
+
+/-- After the source halts: advance the clock head and change nothing else. -/
+def tick : Turing.Action (k + r + 1) Bool (Option State) where
+  inputTape := 0
+  workTapes := Fin.lastCases (none, 1) fun _ => (none, 0)
+  output := none
+  state := some none
+
+/-- Halt once the clock is exhausted, emitting nothing. -/
+def stop : Turing.Action (k + r + 1) Bool (Option State) where
+  inputTape := 0
+  workTapes := fun _ => (none, 0)
+  output := none
+  state := none
+
+/-- The transition occurrences: one per coin while the clock head reads `true`, and a single halt
+afterwards. A halted source keeps two occurrences per clock cell. -/
+def choices (M : MultiTapePTM k Bool State) (r : ℕ) (state : Option State)
+    (symbol : Option Bool) (work : Fin (k + r + 1) → Option Bool) :
+    List (Turing.Action (k + r + 1) Bool (Option State)) :=
+  if work (Fin.last (k + r)) = some true then
+    match state with
+    | some state => [false, true].map fun bit =>
+        lift (coinAction M state symbol (fun i => work (Fin.castAdd r i).castSucc) bit)
+    | none => [tick, tick]
+  else [stop]
+
+/-- **Padded coin counting.** Run a fair-coin table on the first `k` work tapes under the unary
+clock on the last work tape, branching once per coin until the clock is exhausted. The control
+state is the source state, `none` once the source has halted. -/
+def machine (M : MultiTapePTM k Bool State) (r : ℕ) :
+    MultiTapeCTM (k + r + 1) Bool (Option State) where
+  initial := some M.initial
+  tr state symbol work _ := (choices M r state symbol work).map Action.emptyOracleEquiv.symm
+
+/-- A source configuration on the first `k` work tapes, blank middle tapes, and the clock tape
+`clock` with its head at `pos`. -/
+def config (r : ℕ) (c : Cfg k Bool State input) (clock : ℤ → Option Bool) (pos : ℤ) :
+    Cfg (k + r + 1) Bool (Option State) input where
+  state := some c.state
+  inputPos := c.inputPos
+  workTapes := Fin.lastCases clock (Fin.addCases c.workTapes fun _ _ => none)
+  workTapePos := Fin.lastCases pos (Fin.addCases c.workTapePos fun _ => 0)
+  output := c.output
+
+/-- No local view is stuck: some occurrence is always available. -/
+theorem nonblocking_machine (M : MultiTapePTM k Bool State) (r : ℕ) :
+    (machine M r).Nonblocking := by
+  intro state symbol work
+  simp only [machine, choices, ne_eq, List.map_eq_nil_iff]
+  split_ifs
+  · cases state <;> simp
+  · simp
+
+/-- The occurrences at a simulated configuration are the coin choices of its source state. -/
+theorem actions_config (M : MultiTapePTM k Bool State) (c : Cfg k Bool State input)
+    (clock : ℤ → Option Bool) (pos : ℤ) :
+    (machine M r).actions (config r c clock pos) =
+      choices M r c.state c.inputSymbol (config r c clock pos).workTapeSymbols := by
+  simp only [actions, config, machine, List.map_map]
+  rw [Equiv.self_comp_symm, List.map_id]
+  rfl
+
+@[simp] theorem workTapeSymbols_config_last (c : Cfg k Bool State input)
+    (clock : ℤ → Option Bool) (pos : ℤ) :
+    (config r c clock pos).workTapeSymbols (Fin.last (k + r)) = clock pos := by
+  simp [config, Cfg.workTapeSymbols]
+
+@[simp] theorem workTapeSymbols_config_source (c : Cfg k Bool State input)
+    (clock : ℤ → Option Bool) (pos : ℤ) (i : Fin k) :
+    (config r c clock pos).workTapeSymbols (Fin.castAdd r i).castSucc = c.workTapeSymbols i := by
+  simp [config, Cfg.workTapeSymbols]
+
+/-- A lifted source action acts on the source data and advances the clock head. -/
+theorem apply_lift (action : Turing.Action k Bool State) (c : Cfg k Bool State input)
+    (clock : ℤ → Option Bool) (pos : ℤ) :
+    (lift (r := r) action).apply (config r c clock pos) =
+      config r (action.apply c) clock (pos + 1) := by
+  refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext j <;> induction j using Fin.lastCases with
+  | last => simp [lift, config, Action.apply]
+  | cast j =>
+    induction j using Fin.addCases with
+    | left i =>
+      simp only [lift, config, Action.apply, Fin.lastCases_castSucc, Fin.addCases_left]
+    | right i =>
+      simp only [lift, config, Action.apply, Fin.lastCases_castSucc, Fin.addCases_right,
+        SignType.coe_zero, add_zero]
+
+/-- After the source halts, a tick only advances the clock head. -/
+theorem apply_tick {c : Cfg k Bool State input} (hc : c.state = none)
+    (clock : ℤ → Option Bool) (pos : ℤ) :
+    (tick (k := k) (r := r) (State := State)).apply (config r c clock pos) =
+      config r c clock (pos + 1) := by
+  refine Cfg.ext (by simp [tick, config, hc]) (by simp [tick, config])
+    ?_ ?_ (by simp [tick, config, Action.apply]) <;>
+    funext j <;> induction j using Fin.lastCases with
+  | last => simp [tick, config, Action.apply]
+  | cast j =>
+    induction j using Fin.addCases with
+    | left i =>
+      simp only [tick, config, Action.apply, Fin.lastCases_castSucc, Fin.addCases_left,
+        SignType.coe_zero, add_zero]
+    | right i =>
+      simp only [tick, config, Action.apply, Fin.lastCases_castSucc, Fin.addCases_right,
+        SignType.coe_zero, add_zero]
+
+/-- The fixed-coin step of the source, in the notation of the coin replay. -/
+private theorem step_withCoin_of_state (M : MultiTapePTM k Bool State)
+    {c : Cfg k Bool State input} {state : State} (hc : c.state = some state) (bit : Bool) :
+    (M.withCoin bit).toTM.step c =
+      (coinAction M state c.inputSymbol c.workTapeSymbols bit).apply c := by
+  rw [MultiTapeTM.step_of_state hc, MultiTapeMachine.toTM, MultiTapeTM.tr_ofTr]
+  rfl
+
+/-- While the clock lasts, the occurrences are the two coins, each followed by the simulated
+configuration after the corresponding coin step. -/
+private theorem actions_config_of_clock (M : MultiTapePTM k Bool State)
+    (c : Cfg k Bool State input) (clock : ℤ → Option Bool) (pos : ℤ)
+    (hpos : clock pos = some true) :
+    ∃ g : Bool → Turing.Action (k + r + 1) Bool (Option State),
+      (machine M r).actions (config r c clock pos) = [false, true].map g ∧
+        ∀ bit, (g bit).apply (config r c clock pos) =
+          config r ((M.withCoin bit).toTM.step c) clock (pos + 1) := by
+  rw [actions_config]
+  cases hc : c.state with
+  | none =>
+    refine ⟨fun _ => tick, ?_, fun bit => ?_⟩
+    · simp [choices, hpos]
+    · rw [apply_tick hc, MultiTapeTM.step_of_halt hc]
+  | some state =>
+    refine ⟨fun bit => lift (coinAction M state c.inputSymbol c.workTapeSymbols bit), ?_,
+      fun bit => ?_⟩
+    · simp [choices, hpos]
+    · rw [apply_lift, step_withCoin_of_state M hc]
+
+/-- The padded count splits over the first coin. -/
+theorem acceptCount_stepCoins_succ (M : MultiTapePTM k Bool State) (c : Cfg k Bool State input)
+    (n : ℕ) :
+    Complexity.acceptCount (fun p : Cfg k Bool State input × List Bool =>
+        decide ((M.stepCoins p.2 p.1).output = [true])) c (n + 1) =
+      Complexity.acceptCount (fun p : Cfg k Bool State input × List Bool =>
+          decide ((M.stepCoins p.2 p.1).output = [true])) ((M.withCoin false).toTM.step c) n +
+        Complexity.acceptCount (fun p : Cfg k Bool State input × List Bool =>
+          decide ((M.stepCoins p.2 p.1).output = [true])) ((M.withCoin true).toTM.step c) n := by
+  rw [show n + 1 = 1 + n from Nat.add_comm n 1, Complexity.acceptCount_add,
+    Fintype.sum_equiv (Equiv.funUnique (Fin 1) Bool) _
+      (fun bit => Complexity.acceptCount (fun x : Cfg k Bool State input × List Bool =>
+        decide ((M.stepCoins (bit :: x.2) x.1).output = [true])) c n)
+      (fun u => by simp [List.ofFn_succ]),
+    Fintype.sum_bool]
+  simp only [Complexity.acceptCount, MultiTapePTM.stepCoins_cons]
+  exact Nat.add_comm _ _
+
+/-- **The counting phase.** With `n` true cells from the clock head on, every branch halts within
+`n + 1` steps, and the accepting terminal branches are counted exactly by the coin strings of
+length `n` whose replay outputs `[true]`. -/
+theorem haltsWithin_acceptCount_machine (M : MultiTapePTM k Bool State) (r n : ℕ)
+    (c : Cfg k Bool State input) (clock : ℤ → Option Bool) (pos : ℤ)
+    (hclock : ∀ i : ℕ, i < n → clock (pos + i) = some true)
+    (hstop : clock (pos + n) ≠ some true) :
+    (machine M r).HaltsWithin (n + 1) (config r c clock pos) ∧
+      (machine M r).acceptCount (n + 1) (config r c clock pos) =
+        Complexity.acceptCount (fun p : Cfg k Bool State input × List Bool =>
+          decide ((M.stepCoins p.2 p.1).output = [true])) c n := by
+  induction n generalizing c pos with
+  | zero =>
+    have hpos : clock pos ≠ some true := by simpa using hstop
+    have hact : (machine M r).actions (config r c clock pos) = [stop] := by
+      rw [actions_config]
+      simp [choices, hpos]
+    have hhalt : (stop (k := k) (r := r) (State := State)).apply (config r c clock pos)
+        |>.Halted := rfl
+    refine ⟨.step (by simp [hact]) fun index => ?_, ?_⟩
+    · have hindex : ((machine M r).actions (config r c clock pos))[index] = stop :=
+        List.mem_singleton.mp (hact ▸ List.getElem_mem index.isLt)
+      exact .halt (by rw [hindex]; exact hhalt)
+    · rw [acceptCount, ← countP_runList, runList_succ _ _ _ _ rfl, hact,
+        Complexity.acceptCount_zero]
+      by_cases hout : c.output = [true] <;> simp [stop, config, Action.apply, hout]
+  | succ n ih =>
+    have hpos : clock pos = some true := by simpa using hclock 0 (Nat.succ_pos n)
+    have hnext (bit : Bool) := ih ((M.withCoin bit).toTM.step c) (pos + 1)
+      (fun i hi => by
+        have := hclock (i + 1) (by omega)
+        rwa [Nat.cast_add, Nat.cast_one, add_comm (i : ℤ) 1, ← add_assoc] at this)
+      (by
+        have := hstop
+        rwa [Nat.cast_add, Nat.cast_one, add_comm (n : ℤ) 1, ← add_assoc] at this)
+    obtain ⟨g, hact, hg⟩ := actions_config_of_clock (r := r) M c clock pos hpos
+    refine ⟨.step (by simp [hact]) fun index => ?_, ?_⟩
+    · have hmem : ((machine M r).actions (config r c clock pos))[index] ∈
+          [false, true].map g := by
+        rw [← hact]
+        exact List.getElem_mem index.isLt
+      obtain ⟨bit, -, hbit⟩ := List.mem_map.mp hmem
+      rw [← hbit, hg]
+      exact (hnext bit).1
+    · rw [acceptCount_stepCoins_succ, acceptCount, ← countP_runList,
+        runList_succ _ _ _ _ rfl, hact, List.flatMap_map]
+      simp only [List.flatMap_cons, List.flatMap_nil, List.append_nil, List.countP_append, hg]
+      rw [← (hnext false).2, ← (hnext true).2, acceptCount, acceptCount, ← countP_runList,
+        ← countP_runList]
+
+variable {P : Type}
+
+/-- **Prepare, then count.** A deterministic phase on all tapes prepares the clock; the counting
+phase then runs the source from its initial configuration. -/
+noncomputable def compile (M : MultiTapePTM k Bool State)
+    (prepare : MultiTapeTM (k + r + 1) Bool P) : MultiTapeCTM (k + r + 1) Bool (P ⊕ Option State) :=
+  (ofDeterministic prepare).seq (machine M r)
+
+theorem nonblocking_compile (M : MultiTapePTM k Bool State)
+    (prepare : MultiTapeTM (k + r + 1) Bool P) : (compile M prepare).Nonblocking :=
+  (nonblocking_ofDeterministic prepare).seq (nonblocking_machine M r)
+
+/-- A prepared clock of `τ` cells is the initial source configuration under that clock. -/
+private theorem start_eq (M : MultiTapePTM k Bool State) (input : List Bool) (τ : ℕ) :
+    (wordsCfg input (none : Option P)
+        (Function.update (fun _ => []) (Fin.last (k + r)) (List.replicate τ true)) []).withState
+        (some (machine M r).initial) =
+      config r (Cfg.init M.initial input) (tapeOfList (List.replicate τ true)) 0 := by
+  refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext j <;> induction j using Fin.lastCases with
+  | last => simp [config, wordsCfg, Cfg.withState]
+  | cast j =>
+    induction j using Fin.addCases with
+    | left i =>
+      simp only [config, wordsCfg, Cfg.withState, Fin.lastCases_castSucc, Fin.addCases_left,
+        Cfg.init, Function.update_of_ne (Fin.castSucc_ne_last _), tapeOfList_nil]
+    | right i =>
+      simp only [config, wordsCfg, Cfg.withState, Fin.lastCases_castSucc, Fin.addCases_right,
+        Function.update_of_ne (Fin.castSucc_ne_last _), tapeOfList_nil]
+
+/-- **Padded counts from a prepared clock.** If the preparation halts after `time` steps with
+exactly `τ` true cells on the last work tape, every other tape blank and nothing emitted, then
+every branch of the compiled machine halts within `time + (τ + 1)` steps, and its accepting
+terminal count is the padded accepting count `M.acceptCount input τ`. -/
+theorem haltsWithin_acceptCount_compile (M : MultiTapePTM k Bool State)
+    (prepare : MultiTapeTM (k + r + 1) Bool P) (input : List Bool) (time τ : ℕ)
+    (hprepare : prepare.runFrom (prepare.initCfg input) time =
+      wordsCfg input none
+        (Function.update (fun _ => []) (Fin.last (k + r)) (List.replicate τ true)) []) :
+    (compile M prepare).HaltsWithin (time + (τ + 1)) (Cfg.init (compile M prepare).initial input) ∧
+      (compile M prepare).acceptCount (time + (τ + 1))
+        (Cfg.init (compile M prepare).initial input) = M.acceptCount input τ := by
+  set first := ofDeterministic prepare with hfirst_def
+  set cfg := first.initialConfig input with hcfg_def
+  have hready : prepare.runFrom cfg.tapes time = wordsCfg input none
+      (Function.update (fun _ => []) (Fin.last (k + r)) (List.replicate τ true)) [] := hprepare
+  have hfirst : first.HaltsWithin time cfg.tapes := by
+    rw [haltsWithin_ofDeterministic_iff, hready]
+    rfl
+  have hrun : first.runList time cfg.tapes = [wordsCfg input none
+      (Function.update (fun _ => []) (Fin.last (k + r)) (List.replicate τ true)) []] := by
+    rw [runList_ofDeterministic, hready]
+  have hclock := haltsWithin_acceptCount_machine M r τ (Cfg.init M.initial input)
+    (tapeOfList (List.replicate τ true)) 0 (fun i hi => by simp [hi]) (by simp)
+  have hsecond : ∀ result ∈ first.runList time cfg.tapes,
+      (machine M r).HaltsWithin (τ + 1) (result.withState (some (machine M r).initial)) := by
+    intro result hresult
+    rw [hrun, List.mem_singleton] at hresult
+    rw [hresult, start_eq]
+    exact hclock.1
+  have hstart : Cfg.init (compile M prepare).initial input =
+      (Sequential.left (machine M r) cfg).tapes := rfl
+  refine ⟨hstart ▸ HaltsWithin.seq (nonblocking_ofDeterministic prepare) (nonblocking_machine M r)
+    cfg time (τ + 1) hfirst hsecond, ?_⟩
+  rw [hstart, acceptCount, ← countP_runList,
+    show compile M prepare = first.seq (machine M r) from rfl,
+    runList_seq first (machine M r) cfg time (τ + 1) hfirst hsecond, hrun, List.flatMap_singleton,
+    List.countP_map, start_eq]
+  have hcount := hclock.2
+  rw [acceptCount, ← countP_runList] at hcount
+  simp only [Function.comp_def, Cfg.mapState, Option.isNone_map]
+  rw [hcount, MultiTapePTM.acceptCount]
+  simp only [Complexity.acceptCount, MultiTapePTM.runClosedCoins_eq_output_stepCoins]
+
+end Turing.MultiTapeCTM.PaddedClock
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/HaltedReplay.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/HaltedReplay.lean
new file mode 100644
index 0000000000..927db50ec6
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/HaltedReplay.lean
@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.AcceptCount
+
+/-!
+# Replays after halting
+
+A halted configuration of a fair-coin table ignores its coin
+(`Turing.MultiTapePTM.step_withCoin_of_halted`) and every further coin
+(`Turing.MultiTapePTM.stepCoins_of_halted`). So a table that halts at its first step decides
+every coin string at once: the table `Turing.MultiTapePTM.acceptAll`, which emits `true` and
+halts, accepts all `2 ^ τ` coin strings of every positive length `τ`
+(`Turing.MultiTapePTM.acceptCount_acceptAll`).
+
+## Main definitions
+
+* `Turing.MultiTapePTM.acceptAll`: the fair-coin table that emits `true` and halts.
+
+## Main results
+
+* `Turing.MultiTapePTM.step_withCoin_of_halted`, `Turing.MultiTapePTM.stepCoins_of_halted`: a
+  halted configuration ignores its coins.
+* `Turing.MultiTapePTM.acceptCount_acceptAll`: `acceptAll` accepts every coin string of positive
+  length.
+-/
+
+public section
+
+namespace Turing.MultiTapePTM
+
+variable {k : ℕ} {Symbol State : Type} {input : List Symbol}
+
+/-- A halted configuration ignores its coin. -/
+theorem step_withCoin_of_halted (machine : MultiTapePTM k Symbol State)
+    {c : Cfg k Symbol State input} (h : c.Halted) (bit : Bool) :
+    (machine.withCoin bit).toTM.step c = c :=
+  MultiTapeTM.step_of_halt h
+
+/-- A halted configuration ignores any further coins. -/
+theorem stepCoins_of_halted (machine : MultiTapePTM k Symbol State)
+    {c : Cfg k Symbol State input} (h : c.Halted) (coins : List Bool) :
+    machine.stepCoins coins c = c := by
+  induction coins with
+  | nil => rfl
+  | cons bit coins ih => rw [stepCoins_cons, step_withCoin_of_halted machine h, ih]
+
+/-- The fair-coin table that emits `true` and halts at its first step, whatever the coin. -/
+@[expose] def acceptAll : MultiTapePTM 0 Bool Unit where
+  initial := ()
+  tr _ _ _ _ _ := .step ⟨0, Fin.elim0, some true, none⟩ Empty.elim Empty.elim
+
+/-- Every coin string of positive length makes `acceptAll` accept. -/
+theorem acceptCount_acceptAll (input : List Bool) (n : ℕ) :
+    acceptAll.acceptCount input (n + 1) = 2 ^ (n + 1) := by
+  rw [acceptCount, Cslib.Complexity.acceptCount, Finset.filter_true_of_mem]
+  · simp
+  · intro w _
+    have hstep : (acceptAll.withCoin (w 0)).toTM.step (Cfg.init acceptAll.initial input) =
+        ⟨none, 1, fun _ _ => none, fun _ => 0, [true]⟩ := by
+      rw [MultiTapeTM.step_of_state rfl, MultiTapeMachine.toTM, MultiTapeTM.tr_ofTr]
+      exact Cfg.ext rfl (by simp [acceptAll, MultiTapeMachine.Action.emptyOracleEquiv,
+        withCoin]) (funext fun i => i.elim0) (funext fun i => i.elim0) rfl
+    rw [List.ofFn_succ, runClosedCoins_eq_output_stepCoins, stepCoins_cons, hstep,
+      stepCoins_of_halted _ rfl]
+    simp
+
+end Turing.MultiTapePTM
diff --git a/Complexity/Foundations/Data/Nat/Doubling.lean b/Complexity/Foundations/Data/Nat/Doubling.lean
new file mode 100644
index 0000000000..1eec7ee01c
--- /dev/null
+++ b/Complexity/Foundations/Data/Nat/Doubling.lean
@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Mathlib.Data.Nat.Size
+import Mathlib.Tactic.Ring
+
+/-!
+# Powers of two by doubling
+
+Doubling a counter once per element of a list multiplies it by `2 ^ length`
+(`List.foldl_add_self_eq_mul_two_pow`), and the least power of two above `n`, `2 ^ Nat.size n`,
+is at most `2 * n + 1` (`Nat.two_pow_size_le`). Together they bound unary counters built by
+doubling once per binary digit.
+
+## Main results
+
+* `List.foldl_add_self_eq_mul_two_pow`: `l.foldl (fun m _ => m + m) m = m * 2 ^ l.length`.
+* `Nat.two_pow_size_le`: `2 ^ Nat.size n ≤ 2 * n + 1`.
+-/
+
+public section
+
+namespace List
+
+/-- Doubling a counter once per element of a list multiplies it by `2 ^ length`. -/
+theorem foldl_add_self_eq_mul_two_pow {α : Type*} (l : List α) (m : ℕ) :
+    l.foldl (fun m _ => m + m) m = m * 2 ^ l.length := by
+  induction l generalizing m with
+  | nil => simp
+  | cons a l ih =>
+    rw [List.foldl_cons, ih, List.length_cons, pow_succ]
+    ring
+
+end List
+
+namespace Nat
+
+/-- `2 ^ Nat.size n` is the least power of two above `n`, so it is at most `2 * n + 1`. -/
+theorem two_pow_size_le (n : ℕ) : 2 ^ n.size ≤ 2 * n + 1 := by
+  rcases Nat.eq_zero_or_pos n with rfl | hn
+  · simp
+  · obtain ⟨s, hs⟩ : ∃ s, n.size = s + 1 := ⟨n.size - 1, by have := Nat.size_pos.mpr hn; omega⟩
+    have : 2 ^ s ≤ n := Nat.lt_size.mp (by omega)
+    rw [hs, pow_succ]
+    omega
+
+end Nat
diff --git a/ComplexityTests/PaddedCount.lean b/ComplexityTests/PaddedCount.lean
new file mode 100644
index 0000000000..b94cb59092
--- /dev/null
+++ b/ComplexityTests/PaddedCount.lean
@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Complexity.Classes.SharpP.PaddedCount
+import Complexity.Computability.Complexity.Classes.Constructible.UnaryClock
+import Complexity.Computability.Machines.Turing.MultiTape.Counting.PaddedClock
+import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.HaltedReplay
+import Complexity.Foundations.Data.Nat.Doubling
+import ComplexityTests.CountingSeparation
+
+/-! # Padded coin counts as `SharpTIME` functions: checked instances
+
+The unary clock of `Cslib.Complexity.TimeConstructible.exists_prepare_unaryClock`, the padded
+count bridge and the class-level count tests, at the clock `T n = (n + 1) ^ 2 + 1`. The
+always-accepting table gives a nonvacuous instance: its padded count is positive. -/
+
+namespace ComplexityTests.PaddedCount
+
+open Cslib.Complexity Turing ComplexityTests.CountingSeparation
+
+/-! ### The clock -/
+
+/-- The rounded clock is between `c * (m + 1)` and `c * (2 * m + 1)`. -/
+example (c m : ℕ) : c * (m + 1) ≤ c * 2 ^ Nat.size m ∧ c * 2 ^ Nat.size m ≤ c * (2 * m + 1) :=
+  ⟨Nat.mul_le_mul_left c (Nat.lt_size_self m), Nat.mul_le_mul_left c (Nat.two_pow_size_le m)⟩
+
+example : ∃ (r : ℕ) (State : Type) (_ : Finite State) (machine : MultiTapeTM (r + 1) Bool State)
+    (C : ℕ), ∀ input,
+      machine.runFrom (machine.initCfg input) (C * ((input.length + 1) ^ 2 + 1) + C) =
+        wordsCfg input none (Function.update (fun _ => []) (Fin.last r)
+          (List.replicate (3 * 2 ^ Nat.size ((input.length + 1) ^ 2 + 1)) true)) [] :=
+  timeConstructible_succ_sq_add_one.exists_prepare_unaryClock 3
+
+/-! ### The always-accepting table -/
+
+example : MultiTapePTM.acceptAll.acceptCount [true, false] 3 = 8 :=
+  MultiTapePTM.acceptCount_acceptAll _ 2
+
+example : MultiTapePTM.acceptAll.acceptCount [] 0 = 0 := by
+  rw [MultiTapePTM.acceptCount, acceptCount_zero]
+  rfl
+
+/-! ### The bridge -/
+
+/-- A padded count at a linear clock is a positive `SharpTIME` function. -/
+example {α : Type} {enc : α ↪ List Bool} :
+    ∃ f ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1), ∀ a, 0 < f a := by
+  obtain ⟨τ, hτ, -, hmem⟩ := exists_clock_acceptCount_mem_SharpTIME (enc := enc)
+    timeConstructible_succ_sq_add_one 0 1
+  refine ⟨_, hmem MultiTapePTM.acceptAll, fun a => ?_⟩
+  obtain ⟨m, hm⟩ : ∃ m, τ (enc a).length = m + 1 :=
+    Nat.exists_eq_add_one.mpr (Nat.lt_of_lt_of_le (by norm_num) (hτ (enc a).length))
+  simp only [hm, MultiTapePTM.acceptCount_acceptAll]
+  positivity
+
+/-- The counting phase alone: a clock of `n` cells and the coin strings of length `n`. -/
+example {k : ℕ} {State : Type} (M : MultiTapePTM k Bool State) (input : List Bool) (n : ℕ) :
+    (MultiTapeCTM.PaddedClock.machine M 0).acceptCount (n + 1)
+        (MultiTapeCTM.PaddedClock.config 0 (Cfg.init M.initial input)
+          (tapeOfList (List.replicate n true)) 0) =
+      M.acceptCount input n := by
+  rw [(MultiTapeCTM.PaddedClock.haltsWithin_acceptCount_machine M 0 n _ _ 0
+    (fun i hi => by simp [hi]) (by simp)).2, MultiTapePTM.acceptCount]
+  simp only [Cslib.Complexity.acceptCount, MultiTapePTM.runClosedCoins_eq_output_stepCoins]
+
+/-! ### Count tests for nondeterministic, majority and bounded-error time -/
+
+example {α : Type} {enc : α ↪ List Bool} {A : Set α}
+    (hA : A ∈ NTIME enc fun n => (n + 1) ^ 2 + 1) :
+    ∃ f ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1), ∀ a, a ∈ A ↔ 0 < f a :=
+  exists_mem_SharpTIME_of_mem_NTIME timeConstructible_succ_sq_add_one hA
+
+example {α : Type} {enc : α ↪ List Bool} {A : Set α}
+    (hA : A ∈ PPTIME enc fun n => (n + 1) ^ 2 + 1) :
+    ∃ f ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1),
+      ∃ g ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1), ∀ a, a ∈ A ↔ g a < 2 * f a :=
+  exists_mem_SharpTIME_of_mem_PPTIME timeConstructible_succ_sq_add_one hA
+
+example {α : Type} {enc : α ↪ List Bool} {A : Set α}
+    (hA : A ∈ BPTIME enc fun n => (n + 1) ^ 2 + 1) :
+    ∃ f ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1),
+      ∃ g ∈ SharpTIME enc (fun n => (n + 1) ^ 2 + 1), ∀ a, a ∈ A ↔ g a < 2 * f a :=
+  exists_mem_SharpTIME_of_mem_BPTIME timeConstructible_succ_sq_add_one hA
+
+end ComplexityTests.PaddedCount