diff --git a/Complexity.lean b/Complexity.lean
index fb762678b..b1d6f3d37 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1032,6 +1032,9 @@ public import Complexity.Computability.Complexity.Classes.Constructible
 public import Complexity.Computability.Complexity.Classes.Constructible.Log
 public import Complexity.Computability.Complexity.Classes.Counting.OracleSpace
 public import Complexity.Computability.Complexity.Classes.Counting.Space
+public import Complexity.Computability.Complexity.Classes.CountingSimulation.Accumulate
+public import Complexity.Computability.Complexity.Classes.CountingSimulation.Assembly
+public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces
 public import Complexity.Computability.Complexity.Classes.DP
 public import Complexity.Computability.Complexity.Classes.EXP
 public import Complexity.Computability.Complexity.Classes.FewP
diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean
new file mode 100644
index 000000000..a464744eb
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean
@@ -0,0 +1,287 @@
+/-
+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.GenericRAM.Native.IndexFold
+public import Complexity.Foundations.Data.Nat.ResidueSum
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv
+
+/-!
+# Streamed sums modulo a computed modulus
+
+`Cslib.Complexity.CountingSimulation.modSum r modulus count c` adds the terms `r (c, 0)`, …,
+`r (c, count c - 1)` to an accumulator one at a time, reducing modulo `modulus c` after each
+addition. The terms are visited by the binary-index fold `Cslib.GenericRAM.IndexFold`, which keeps
+only the index, the context `c` and the accumulator, so the workspace does not grow with the
+number of terms.
+
+This is the outer loop of the deterministic counting simulation of #1833: the context is the input
+and the clock, the terms are the residues of the contractions of the networks of the movement
+schedules, and the modulus is a power of two above the count being recovered
+(`Nat.foldl_range_add_mod_eq_of_lt`).
+
+The resource bound (`Cslib.Complexity.CountingSimulation.exists_computableInO_modSum`) is a native
+multi-tape certificate: if the number of terms and the modulus are computable in polynomial time,
+the terms lie below the modulus, and a certificate computes the term at every summed index within
+time `R c` and space `Q c`, then the streamed sum is computable within time
+`(count c + 1) * (poly + R c)` and space `poly + Q c`, for a polynomial in the encoded length of the
+context. Neither `R` nor `Q` needs to be polynomial.
+
+## Main definitions
+
+* `Cslib.Complexity.CountingSimulation.modSumStep`: one round of the streamed sum.
+* `Cslib.Complexity.CountingSimulation.modSum`: the streamed sum modulo the modulus.
+
+## Main results
+
+* `Cslib.Complexity.CountingSimulation.modSum_eq_sum_mod`: the streamed sum is the sum of the terms
+  modulo the modulus.
+* `Cslib.Complexity.CountingSimulation.exists_computableInO_modSum`: its time and space bounds.
+-/
+
+public section
+
+namespace Cslib.Complexity.CountingSimulation
+
+open Turing.MultiTapeTM Cslib.GenericRAM
+
+variable {C : Type}
+
+/-- One round of the streamed sum at index `p.1`, with context `p.2.1` and accumulator `p.2.2`:
+below the number of terms, add the term and reduce modulo the modulus; otherwise leave the state
+unchanged. -/
+def modSumStep (r : C × ℕ → ℕ) (modulus count : C → ℕ) (p : ℕ × (C × ℕ)) : C × ℕ :=
+  if p.1 < count p.2.1 then (p.2.1, (p.2.2 + r (p.2.1, p.1)) % modulus p.2.1) else p.2
+
+/-- The terms `r (c, 0)`, …, `r (c, count c - 1)` summed one at a time from zero, reducing modulo
+`modulus c` after each addition, by a streaming fold over a binary index. -/
+def modSum (r : C × ℕ → ℕ) (modulus count : C → ℕ) (c : C) : ℕ :=
+  (IndexFold.run (modSumStep r modulus count) (count c) (c, 0)).2.2
+
+variable {r : C × ℕ → ℕ} {modulus count : C → ℕ}
+
+/-- The state of the streamed sum after `j ≤ count c` rounds: the index `j`, the unchanged context
+and the residue of the first `j` terms. -/
+theorem run_modSumStep {c : C} {j : ℕ} (hj : j ≤ count c) :
+    IndexFold.run (modSumStep r modulus count) j (c, 0) =
+      (j, (c, (List.range j).foldl (fun acc i => (acc + r (c, i)) % modulus c) 0)) := by
+  induction j with
+  | zero => rfl
+  | succ j ih =>
+    rw [IndexFold.run_succ, ih (by omega)]
+    simp only [IndexFold.step, modSumStep, (show j < count c by omega), ↓reduceIte, List.range_succ,
+      List.foldl_append, List.foldl_cons, List.foldl_nil]
+
+/-- **The streamed sum is the sum modulo the modulus.** -/
+theorem modSum_eq_sum_mod (r : C × ℕ → ℕ) (modulus count : C → ℕ) (c : C) :
+    modSum r modulus count c = (∑ i ∈ Finset.range (count c), r (c, i)) % modulus c := by
+  have h := Nat.foldl_range_add_mod (fun i => r (c, i)) (modulus c) 0 (count c)
+  rw [Nat.zero_mod, Nat.zero_add] at h
+  rw [modSum, run_modSumStep le_rfl, h]
+
+private theorem foldl_add_mod_lt {f : ℕ → ℕ} {m : ℕ} (hm : 0 < m) (j : ℕ) :
+    (List.range j).foldl (fun acc i => (acc + f i) % m) 0 < m := by
+  cases j with
+  | zero => exact hm
+  | succ j =>
+    rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil]
+    exact Nat.mod_lt _ hm
+
+private theorem polyBounded_comp_poly {size u : C → ℕ} {p : ℕ → ℕ}
+    (hp : Cslib.PolynomiallyBounded p) (hu : PolyBounded size u) :
+    PolyBounded size fun c => p (u c) :=
+  (PolyBounded.of_polynomiallyBounded id hp).comp hu
+
+/-- **Resource bound of the streamed sum.** Suppose the number of terms and the modulus are
+computable in polynomial time, the modulus is positive, every summed term lies below it, and a
+native certificate computes the terms within time `R c` and space `Q c` at the summed indices.
+Then the streamed sum is computable within time `(count c + 1) * (a * (n + 1) ^ d + R c)` and space
+`a * (n + 1) ^ d + Q c`, where `n` is the encoded length of the context and `a`, `d` are constants:
+the workspace holds one binary index, the context and an accumulator below the modulus. -/
+theorem exists_computableInO_modSum {encC : C ↪ List Bool}
+    (hmodulus : ComputableInPolyTime modulus encC encNat)
+    (hcount : ComputableInPolyTime count encC encNat)
+    (cr : NativeCertificate r (encPair encC encNat) encNat)
+    (hpos : ∀ c, 0 < modulus c) (hr : ∀ c i, i < count c → r (c, i) < modulus c)
+    (R Q : C → ℕ) (hR : ∀ c i, i < count c → cr.time (c, i) ≤ R c)
+    (hQ : ∀ c i, i < count c → cr.space (c, i) ≤ Q c) :
+    ∃ a d : ℕ, ComputableInO (modSum r modulus count) encC encNat
+      (fun c => (count c + 1) * (a * ((encC c).length + 1) ^ d + R c))
+      (fun c => a * ((encC c).length + 1) ^ d + Q c) := by
+  -- The polynomial-time pieces of a round.
+  have htest : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => decide (p.1 < count p.2.1))
+      (encPair encNat (encPair encC encNat)) encBool := by fun_prop
+  have hctx : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => p.2.1)
+      (encPair encNat (encPair encC encNat)) encC := by fun_prop
+  have hacc : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => p.2.2)
+      (encPair encNat (encPair encC encNat)) encNat := by fun_prop
+  have hswap : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => (p.2.1, p.1))
+      (encPair encNat (encPair encC encNat)) (encPair encC encNat) := by fun_prop
+  have hmod : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => modulus p.2.1)
+      (encPair encNat (encPair encC encNat)) encNat := by fun_prop
+  have hno : ComputableInPolyTime (fun p : ℕ × (C × ℕ) => p.2)
+      (encPair encNat (encPair encC encNat)) (encPair encC encNat) := by fun_prop
+  have hadd : ComputableInPolyTime (fun q : ℕ × ℕ × ℕ => (q.1 + q.2.1) % q.2.2)
+      (encPair encNat (encPair encNat encNat)) encNat := by fun_prop
+  have hinit : ComputableInPolyTime (fun c : C => (c, 0)) encC (encPair encC encNat) := by
+    fun_prop
+  -- The round: a test, then either the addition or nothing.
+  let yes : NativeCertificate
+      (fun p : ℕ × (C × ℕ) => (p.2.1, (p.2.2 + r (p.2.1, p.1)) % modulus p.2.1))
+      (encPair encNat (encPair encC encNat)) (encPair encC encNat) :=
+    (NativeCertificate.ofPolyTime hctx).prod
+      ((NativeCertificate.ofPolyTime hadd).comp
+        ((NativeCertificate.ofPolyTime hacc).prod
+          ((cr.comp (NativeCertificate.ofPolyTime hswap)).prod
+            (NativeCertificate.ofPolyTime hmod))))
+  let cstep : NativeCertificate (modSumStep r modulus count)
+      (encPair encNat (encPair encC encNat)) (encPair encC encNat) :=
+    (NativeCertificate.branch (NativeCertificate.ofPolyTime htest) yes
+      (NativeCertificate.ofPolyTime hno)).congr fun p => by
+        simp only [modSumStep, decide_eq_true_eq]
+  -- Monotone polynomial bounds of the pieces.
+  obtain ⟨pT, hpT, mT, bT⟩ := exists_mono_poly_cert htest
+  obtain ⟨pC, hpC, mC, bC⟩ := exists_mono_poly_cert hctx
+  obtain ⟨pA, hpA, mA, bA⟩ := exists_mono_poly_cert hacc
+  obtain ⟨pW, hpW, mW, bW⟩ := exists_mono_poly_cert hswap
+  obtain ⟨pM, hpM, mM, bM⟩ := exists_mono_poly_cert hmod
+  obtain ⟨pN, hpN, mN, bN⟩ := exists_mono_poly_cert hno
+  obtain ⟨pD, hpD, mD, bD⟩ := exists_mono_poly_cert hadd
+  obtain ⟨pI, hpI, -, bI⟩ := exists_mono_poly_cert hinit
+  obtain ⟨pK, hpK, -, bK⟩ := exists_mono_poly_cert hcount
+  -- Sizes: the context, the modulus and the number of terms.
+  set L : C → ℕ := fun c => (encC c).length with hL
+  set lm : C → ℕ := fun c => (encNat (modulus c)).length with hlm
+  set lk : C → ℕ := fun c => (encNat (count c)).length with hlk
+  have hLp : PolyBounded L L := PolyBounded.self
+  have hlmp : PolyBounded L lm := hmodulus.polyBounded_length
+  have hlkp : PolyBounded L lk := hcount.polyBounded_length
+  -- A state `(j, (c, acc))` with `j ≤ count c` and `acc < modulus c` has length at most `S c`; the
+  -- input of the addition has length at most `S' c`; the accumulator pair at most `B c`.
+  let S : C → ℕ := fun c => 2 * lk c + 2 * L c + lm c + 2
+  let S' : C → ℕ := fun c => 5 * lm c + 2
+  let B : C → ℕ := fun c => 2 * L c + 1 + lm c
+  let U : C → ℕ := fun c => pT (S c) + pC (S c) + pA (S c) + pW (S c) + pM (S c) + pD (S' c) +
+    pN (S c)
+  have hstate (c : C) (j : ℕ) (hj : j ≤ count c) :
+      (encPair encNat (encPair encC encNat)
+        (IndexFold.run (modSumStep r modulus count) j (c, 0))).length ≤ S c := by
+    rw [run_modSumStep hj]
+    have hacc := length_encNat_mono (foldl_add_mod_lt (f := fun i => r (c, i)) (hpos c) j).le
+    have hj' := length_encNat_mono hj
+    simp only [length_encPair, S, L, lm, lk] at hacc hj' ⊢
+    omega
+  have hround_time (c : C) (j : ℕ) (hj : j ≤ count c) :
+      cstep.time (IndexFold.run (modSumStep r modulus count) j (c, 0)) ≤ U c + R c := by
+    have hs := hstate c j hj
+    rw [run_modSumStep hj] at hs ⊢
+    set acc := (List.range j).foldl (fun acc i => (acc + r (c, i)) % modulus c) 0
+    simp only [cstep, yes, NativeCertificate.congr, NativeCertificate.branch_time,
+      NativeCertificate.prod_time, NativeCertificate.comp_time, Function.comp_apply]
+    have h1 := (bT (j, (c, acc))).1.trans (mT hs)
+    split_ifs with hlt
+    · have hjc : j < count c := of_decide_eq_true hlt
+      have hacc_lt : acc < modulus c := foldl_add_mod_lt (hpos c) j
+      have hrj := hr c j hjc
+      have hq : (encPair encNat (encPair encNat encNat)
+          (acc, r (c, j), modulus c)).length ≤ S' c := by
+        have := length_encNat_mono hacc_lt.le
+        have := length_encNat_mono hrj.le
+        simp only [length_encPair, S', lm] at *
+        omega
+      have h2 := (bC (j, (c, acc))).1.trans (mC hs)
+      have h3 := (bA (j, (c, acc))).1.trans (mA hs)
+      have h4 := (bW (j, (c, acc))).1.trans (mW hs)
+      have h5 := (bM (j, (c, acc))).1.trans (mM hs)
+      have h6 := (bD (acc, r (c, j), modulus c)).1.trans (mD hq)
+      have h7 := hR c j hjc
+      simp only [U]
+      omega
+    · have h2 := (bN (j, (c, acc))).1.trans (mN hs)
+      simp only [U]
+      omega
+  have hround_space (c : C) (j : ℕ) (hj : j ≤ count c) :
+      cstep.space (IndexFold.run (modSumStep r modulus count) j (c, 0)) ≤ U c + Q c := by
+    have hs := hstate c j hj
+    rw [run_modSumStep hj] at hs ⊢
+    set acc := (List.range j).foldl (fun acc i => (acc + r (c, i)) % modulus c) 0
+    simp only [cstep, yes, NativeCertificate.congr, NativeCertificate.branch_space,
+      NativeCertificate.prod_space, NativeCertificate.comp_space, Function.comp_apply]
+    have h1 := (bT (j, (c, acc))).2.trans (mT hs)
+    split_ifs with hlt
+    · have hjc : j < count c := of_decide_eq_true hlt
+      have hacc_lt : acc < modulus c := foldl_add_mod_lt (hpos c) j
+      have hrj := hr c j hjc
+      have hq : (encPair encNat (encPair encNat encNat)
+          (acc, r (c, j), modulus c)).length ≤ S' c := by
+        have := length_encNat_mono hacc_lt.le
+        have := length_encNat_mono hrj.le
+        simp only [length_encPair, S', lm] at *
+        omega
+      have h2 := (bC (j, (c, acc))).2.trans (mC hs)
+      have h3 := (bA (j, (c, acc))).2.trans (mA hs)
+      have h4 := (bW (j, (c, acc))).2.trans (mW hs)
+      have h5 := (bM (j, (c, acc))).2.trans (mM hs)
+      have h6 := (bD (acc, r (c, j), modulus c)).2.trans (mD hq)
+      have h7 := hQ c j hjc
+      simp only [U]
+      omega
+    · have h2 := (bN (j, (c, acc))).2.trans (mN hs)
+      simp only [U]
+      omega
+  have hacc_len (c : C) (j : ℕ) (hj : j ≤ count c) :
+      (encPair encC encNat (IndexFold.run (modSumStep r modulus count) j (c, 0)).2).length ≤
+        B c := by
+    rw [run_modSumStep hj]
+    have := length_encNat_mono (foldl_add_mod_lt (f := fun i => r (c, i)) (hpos c) j).le
+    simp only [length_encPair, B, L, lm] at this ⊢
+    omega
+  have hrun := IndexFold.computableInO (NativeCertificate.ofPolyTime hcount)
+    (NativeCertificate.ofPolyTime hinit) cstep (fun c => U c + R c) (fun c => U c + Q c) B
+    hround_time hround_space hacc_len
+  have hout := (ComputableInO.snd encC encNat).comp_linear
+    ((ComputableInO.snd encNat (encPair encC encNat)).comp_linear hrun)
+  -- Collect the polynomial overhead.
+  let V : C → ℕ := fun c => pK (L c) + (L c + pI (L c)) + 2 * (2 * lk c + 1 + B c) +
+    2 * (lk c + 1) ^ 2 + (lk c + 1) + lk c + U c
+  have hSp : PolyBounded L S :=
+    ((((PolyBounded.const 2).mul hlkp).add ((PolyBounded.const 2).mul hLp)).add hlmp).add
+      (PolyBounded.const 2)
+  have hS'p : PolyBounded L S' := ((PolyBounded.const 5).mul hlmp).add (PolyBounded.const 2)
+  have hBp : PolyBounded L B :=
+    ((((PolyBounded.const 2).mul hLp).add (PolyBounded.const 1))).add hlmp
+  have hUp : PolyBounded L U :=
+    ((((((polyBounded_comp_poly hpT hSp).add (polyBounded_comp_poly hpC hSp)).add
+      (polyBounded_comp_poly hpA hSp)).add (polyBounded_comp_poly hpW hSp)).add
+      (polyBounded_comp_poly hpM hSp)).add (polyBounded_comp_poly hpD hS'p)).add
+      (polyBounded_comp_poly hpN hSp)
+  have hVp : PolyBounded L V :=
+    ((((((polyBounded_comp_poly hpK hLp).add (hLp.add (polyBounded_comp_poly hpI hLp))).add
+      ((PolyBounded.const 2).mul ((((PolyBounded.const 2).mul hlkp).add
+        (PolyBounded.const 1)).add hBp))).add
+      ((PolyBounded.const 2).mul ((hlkp.add (PolyBounded.const 1)).pow 2))).add
+      (hlkp.add (PolyBounded.const 1))).add hlkp).add hUp
+  obtain ⟨a, d, hV⟩ := hVp.exists_le
+  refine ⟨a, d, (hout.mono_le (fun c => ?_) fun c => ?_).of_enc_eq fun c => rfl⟩
+  · have hK := (bK c).1
+    have hI := (bI c).1
+    have hVc := hV c
+    have hone : 1 ≤ count c + 1 := by omega
+    have hmul : V c + R c ≤ (count c + 1) * (V c + R c) := Nat.le_mul_of_pos_left _ hone
+    have hmono : (count c + 1) * (V c + R c) ≤ (count c + 1) * (a * (L c + 1) ^ d + R c) :=
+      Nat.mul_le_mul_left _ (by omega)
+    simp only [V, L, lk] at hK hI hVc hmul hmono ⊢
+    nlinarith
+  · have hK := (bK c).2
+    have hI := (bI c).2
+    have hVc := hV c
+    simp only [V, L, lk] at hK hI hVc ⊢
+    omega
+
+end Cslib.Complexity.CountingSimulation
diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean
new file mode 100644
index 000000000..a0f6d3e82
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean
@@ -0,0 +1,463 @@
+/-
+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.CountingSimulation.Accumulate
+public import Complexity.Computability.Complexity.Classes.CountingSimulation.Interfaces
+public import Complexity.Computability.Complexity.Classes.Constructible
+public import Complexity.Foundations.Data.Nat.SqrtLog
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryLog
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith
+
+/-!
+# The deterministic counting simulation, assembled from its interfaces
+
+This module assembles the deterministic simulation of #1833 from the two interfaces of
+`Cslib.Complexity.CountingSimulation.NetworkFamily` and
+`Cslib.Complexity.CountingSimulation.ContractionAlgorithm`. **It is conditional**: every result
+here assumes a network family and a contraction algorithm, which are proved separately.
+
+On an input `x` with clock `t`, the simulation (`Cslib.Complexity.CountingSimulation.simulate`)
+visits the `scheduleCount heads t` movement schedules one at a time, contracts the network of each
+modulo `2 ^ (paddedTime t + 1)`, and adds the residues modulo the same power of two
+(`Cslib.Complexity.CountingSimulation.modSum`). Since the count is at most `2 ^ (paddedTime t)`,
+the residue of the sum is the count itself (`Cslib.Complexity.CountingSimulation.simulate_eq`).
+
+Its cost is the number of schedules times the cost of one network, and its workspace that of one
+network and an accumulator (`Cslib.Complexity.CountingSimulation.exists_computableInO_simulate`).
+With the clock `t = c * T n` of a time-constructible `T n ≥ max n 2`, the schedules number
+`3 ^ O(T / log T)`, so the total time is `2 ^ O(T / √(log T))` in the natural-number scale of
+`Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`, and the space is polynomial in `T`
+(`Cslib.Complexity.CountingSimulation.exists_computableInO_count`). The result may be any
+polynomial-time function of the padded time, in unary, and the count, such as a comparison
+deciding acceptance.
+
+## Main definitions
+
+* `Cslib.Complexity.CountingSimulation.scheduleResidue`: the contraction of the network of one
+  schedule, modulo `2 ^ (paddedTime t + 1)`.
+* `Cslib.Complexity.CountingSimulation.simulate`: the streamed sum of these residues.
+
+## Main results
+
+* `Cslib.Complexity.CountingSimulation.simulate_eq`: the simulation computes the count.
+* `Cslib.Complexity.CountingSimulation.exists_computableInO_simulate`: its time and space bounds in
+  terms of the clock.
+* `Cslib.Complexity.CountingSimulation.exists_computableInO_count`: from a time-constructible bound,
+  the count at the padded clock, or any polynomial-time function of it and the padded time, within
+  time `2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d`.
+-/
+
+public section
+
+namespace Cslib.Complexity.CountingSimulation
+
+open Turing.MultiTapeTM Cslib.GenericRAM
+
+variable {N : Type} {encN : N ↪ List Bool} {value : N → ℕ} {Admissible : ℕ → ℕ → N → Prop}
+  {count : List Bool → ℕ → ℕ}
+
+/-! ### The algorithm and its correctness -/
+
+/-- The value of the network of the schedule `p.2` for the input `p.1.1` and the clock `p.1.2`,
+modulo `2 ^ (paddedTime p.1.2 + 1)`. -/
+def scheduleResidue (F : NetworkFamily encN value Admissible count) (p : (List Bool × ℕ) × ℕ) :
+    ℕ :=
+  value (F.net (p.1.1, p.1.2, p.2)) % 2 ^ (paddedTime p.1.2 + 1)
+
+/-- **The simulation** on the input `p.1` with the clock `p.2`: when `|p.1| ≤ p.2` and `2 ≤ p.2`,
+the residues of the networks of all schedules, summed one at a time modulo
+`2 ^ (paddedTime p.2 + 1)`; otherwise `0`. -/
+def simulate (F : NetworkFamily encN value Admissible count) (p : List Bool × ℕ) : ℕ :=
+  if p.1.length ≤ p.2 ∧ 2 ≤ p.2 then
+    modSum (scheduleResidue F) (fun p => 2 ^ (paddedTime p.2 + 1))
+      (fun p => scheduleCount F.heads p.2) p
+  else 0
+
+/-- **The simulation computes the count**: when `|x| ≤ t` and `2 ≤ t`, and the count at the padded
+time is at most `2 ^ paddedTime t`, the residue of the sum of the network values modulo
+`2 ^ (paddedTime t + 1)` is the count itself. -/
+theorem simulate_eq (F : NetworkFamily encN value Admissible count) {x : List Bool} {t : ℕ}
+    (hx : x.length ≤ t) (ht : 2 ≤ t) (hcount : count x (paddedTime t) ≤ 2 ^ paddedTime t) :
+    simulate F (x, t) = count x (paddedTime t) := by
+  rw [simulate, ite_eq_left_of_eq_true _ _ (eq_true (⟨hx, ht⟩ : x.length ≤ t ∧ 2 ≤ t)),
+    modSum_eq_sum_mod]
+  simp only [scheduleResidue]
+  rw [← Finset.sum_nat_mod, F.sum_value x t hx ht]
+  exact Nat.mod_eq_of_lt (hcount.trans_lt (Nat.pow_lt_pow_right one_lt_two (Nat.lt_succ_self _)))
+
+/-! ### Polynomial-time parameters -/
+
+private theorem paddedTime_eq (t : ℕ) :
+    paddedTime t = (t + Nat.clog 2 (t + 2) - 1) / Nat.clog 2 (t + 2) * Nat.clog 2 (t + 2) := by
+  rw [paddedTime, numBlocks, blockLength, Nat.ceilDiv_eq_add_pred_div]
+
+private theorem computableInPolyTime_paddedTime_succ :
+    ComputableInPolyTime (fun t => paddedTime t + 1) encUnary encNat := by
+  simp only [paddedTime_eq]
+  fun_prop
+
+private theorem computableInPolyTime_paddedTime :
+    ComputableInPolyTime paddedTime encUnary encUnary := by
+  rw [show paddedTime = _ from funext paddedTime_eq]
+  fun_prop
+
+private theorem computableInPolyTime_two_pow_paddedTime :
+    ComputableInPolyTime (fun t => 2 ^ (paddedTime t + 1)) encUnary encNat := by
+  simp only [paddedTime_eq]
+  fun_prop
+
+private theorem computableInPolyTime_scheduleCount (heads : ℕ) :
+    ComputableInPolyTime (scheduleCount heads) encUnary encNat := by
+  have h : ComputableInPolyTime
+      (fun t => 3 ^ (heads * ((t + Nat.clog 2 (t + 2) - 1) / Nat.clog 2 (t + 2)))) encUnary
+      encNat :=
+    ComputableInPolyTime.binary_pow' (ComputableInPolyTime.const (encOut := encNat) 3) (by fun_prop)
+  convert h using 2 with t
+  rw [scheduleCount, numBlocks, blockLength, Nat.ceilDiv_eq_add_pred_div]
+
+/-! ### Resource bounds -/
+
+/-- **Time and space of the simulation** (conditional on the interfaces). For a constant `k`, the
+simulation on an input `x` with clock `t` runs within time
+`k * (|x| + t + 1) ^ k * scheduleCount heads t * 2 ^ (k * t / √⌊log₂ t⌋)` and space
+`k * (|x| + t + 1) ^ k`: it contracts one network per schedule, keeping one network, its
+contraction workspace and an accumulator. -/
+theorem exists_computableInO_simulate (F : NetworkFamily encN value Admissible count)
+    (A : ContractionAlgorithm encN value Admissible) :
+    ∃ k : ℕ, ComputableInO (simulate F) (encPair encBits encUnary) encNat
+      (fun p => k * (p.1.length + p.2 + 1) ^ k * scheduleCount F.heads p.2 *
+        2 ^ (k * p.2 / Nat.sqrt (Nat.log 2 p.2)))
+      (fun p => k * (p.1.length + p.2 + 1) ^ k) := by
+  classical
+  -- The polynomial-time pieces.
+  have hP : ComputableInPolyTime (fun p : (List Bool × ℕ) × ℕ => paddedTime p.1.2 + 1)
+      (encPair (encPair encBits encUnary) encNat) encNat :=
+    computableInPolyTime_paddedTime_succ.comp (by fun_prop)
+  have hPc : ComputableInPolyTime (fun p : List Bool × ℕ => paddedTime p.2 + 1)
+      (encPair encBits encUnary) encNat :=
+    computableInPolyTime_paddedTime_succ.comp (by fun_prop)
+  have hnet : ComputableInPolyTime (fun p : (List Bool × ℕ) × ℕ => F.net (p.1.1, p.1.2, p.2))
+      (encPair (encPair encBits encUnary) encNat) encN :=
+    F.polyTime.comp (by fun_prop)
+  have hmod : ComputableInPolyTime (fun p : List Bool × ℕ => 2 ^ (paddedTime p.2 + 1))
+      (encPair encBits encUnary) encNat :=
+    computableInPolyTime_two_pow_paddedTime.comp (by fun_prop)
+  have hcnt : ComputableInPolyTime (fun p : List Bool × ℕ => scheduleCount F.heads p.2)
+      (encPair encBits encUnary) encNat :=
+    (computableInPolyTime_scheduleCount F.heads).comp (by fun_prop)
+  have hguard : ComputableInPolyTime
+      (fun p : List Bool × ℕ => decide (p.1.length ≤ p.2 ∧ 2 ≤ p.2))
+      (encPair encBits encUnary) encBool := by fun_prop
+  -- The residue of one schedule: the contraction of its network at the precision.
+  let cr : NativeCertificate (scheduleResidue F) (encPair (encPair encBits encUnary) encNat)
+      encNat :=
+    A.certificate.comp ((NativeCertificate.ofPolyTime hP).prod (NativeCertificate.ofPolyTime hnet))
+  let R : List Bool × ℕ → ℕ := fun c =>
+    (Finset.range (scheduleCount F.heads c.2)).sup fun i => cr.time (c, i)
+  let Q : List Bool × ℕ → ℕ := fun c =>
+    (Finset.range (scheduleCount F.heads c.2)).sup fun i => cr.space (c, i)
+  obtain ⟨a, d, hms⟩ := exists_computableInO_modSum hmod hcnt cr (fun _ => by positivity)
+    (fun c i _ => Nat.mod_lt _ (by positivity)) R Q
+    (fun c i hi => Finset.le_sup (f := fun i => cr.time (c, i)) (Finset.mem_range.mpr hi))
+    (fun c i hi => Finset.le_sup (f := fun i => cr.space (c, i)) (Finset.mem_range.mpr hi))
+  let cms : NativeCertificate (modSum (scheduleResidue F) (fun p => 2 ^ (paddedTime p.2 + 1))
+      (fun p => scheduleCount F.heads p.2)) (encPair encBits encUnary) encNat := ⟨_, _, hms⟩
+  let csim : NativeCertificate (simulate F) (encPair encBits encUnary) encNat :=
+    (NativeCertificate.branch (NativeCertificate.ofPolyTime hguard) cms
+      (NativeCertificate.const 0)).congr fun p => by simp only [simulate, decide_eq_true_eq]
+  -- Bounds on the pieces.
+  obtain ⟨K, hK⟩ := A.bound F.constant 2
+  obtain ⟨pP, hpP, mP, bP⟩ := exists_mono_poly_cert hP
+  obtain ⟨pN, hpN, mN, bN⟩ := exists_mono_poly_cert hnet
+  obtain ⟨pG, hpG, -, bG⟩ := exists_mono_poly_cert hguard
+  obtain ⟨an, dn, hnl⟩ := hnet.polyBounded_length.exists_le
+  set sz : List Bool × ℕ → ℕ := fun c => (encPair encBits encUnary c).length with hsz
+  let Z : List Bool × ℕ → ℕ := fun c => 2 * sz c + 1 + (encNat (scheduleCount F.heads c.2)).length
+  let Y : List Bool × ℕ → ℕ := fun c =>
+    2 * (encNat (paddedTime c.2 + 1)).length + 1 + an * (Z c + 1) ^ dn
+  let U : List Bool × ℕ → ℕ := fun c => pP (Z c) + pN (Z c) + K * (Y c + 1) ^ K
+  let E : List Bool × ℕ → ℕ := fun c => 2 ^ (K * c.2 / Nat.sqrt (Nat.log 2 c.2))
+  have hE (c : List Bool × ℕ) : 1 ≤ E c := Nat.one_le_two_pow
+  have hcnt1 (c : List Bool × ℕ) : 1 ≤ scheduleCount F.heads c.2 := Nat.one_le_pow _ _ (by norm_num)
+  -- One schedule at a good context.
+  have hone (c : List Bool × ℕ) (hc : c.1.length ≤ c.2 ∧ 2 ≤ c.2) (i : ℕ)
+      (hi : i < scheduleCount F.heads c.2) :
+      cr.time (c, i) ≤ U c * E c ∧ cr.space (c, i) ≤ U c := by
+    have hZ : (encPair (encPair encBits encUnary) encNat (c, i)).length ≤ Z c := by
+      have := (length_encNat_mono hi.le)
+      simp only [length_encPair, Z, sz] at this ⊢
+      omega
+    have hG : (encN (F.net (c.1, c.2, i))).length ≤
+        an * ((encPair (encPair encBits encUnary) encNat (c, i)).length + 1) ^ dn := hnl (c, i)
+    have hY : (encPair encNat encN (paddedTime c.2 + 1, F.net (c.1, c.2, i))).length ≤ Y c := by
+      have hG' := hG.trans
+        (Nat.mul_le_mul_left an (Nat.pow_le_pow_left (Nat.add_le_add_right hZ 1) dn))
+      rw [length_encPair]
+      simp only [Y]
+      omega
+    have hA := hK c.2 (paddedTime c.2 + 1) (F.net (c.1, c.2, i)) hc.2 (by omega)
+      (paddedTime_add_one_le hc.2) (F.admissible c.1 c.2 i hc.1 hc.2 hi)
+    have hKY := Nat.mul_le_mul_left K (Nat.pow_le_pow_left (Nat.add_le_add_right hY 1) K)
+    have h1 := (bP (c, i)).1.trans (mP hZ)
+    have h2 := (bN (c, i)).1.trans (mN hZ)
+    have h3 := (bP (c, i)).2.trans (mP hZ)
+    have h4 := (bN (c, i)).2.trans (mN hZ)
+    have hEc := hE c
+    simp only [cr, NativeCertificate.comp_time, NativeCertificate.comp_space,
+      NativeCertificate.prod_time, NativeCertificate.prod_space]
+    constructor
+    · have hmul : K * ((encPair encNat encN (paddedTime c.2 + 1, F.net (c.1, c.2, i))).length +
+          1) ^ K * E c ≤ K * (Y c + 1) ^ K * E c := Nat.mul_le_mul_right _ hKY
+      have hpe : pP (Z c) + pN (Z c) ≤ (pP (Z c) + pN (Z c)) * E c := Nat.le_mul_of_pos_right _ hEc
+      simp only [U, E] at hA hmul hpe ⊢
+      nlinarith [hA.1]
+    · simp only [U] at hA ⊢
+      omega
+  -- Collect the polynomial overhead.
+  let V : List Bool × ℕ → ℕ := fun c => pG (sz c) + sz c + 2 * (a * (sz c + 1) ^ d + U c)
+  have hszp : PolyBounded sz sz := PolyBounded.self
+  have hcntp : PolyBounded sz fun c => (encNat (scheduleCount F.heads c.2)).length :=
+    hcnt.polyBounded_length
+  have hPcp : PolyBounded sz fun c => (encNat (paddedTime c.2 + 1)).length := hPc.polyBounded_length
+  have hZp : PolyBounded sz Z :=
+    (((PolyBounded.const 2).mul hszp).add (PolyBounded.const 1)).add hcntp
+  have hYp : PolyBounded sz Y :=
+    ((((PolyBounded.const 2).mul hPcp).add (PolyBounded.const 1))).add
+      ((PolyBounded.const an).mul ((hZp.add (PolyBounded.const 1)).pow dn))
+  have hUp : PolyBounded sz U :=
+    (((PolyBounded.of_polynomiallyBounded id hpP).comp hZp).add
+      ((PolyBounded.of_polynomiallyBounded id hpN).comp hZp)).add
+      ((PolyBounded.const K).mul ((hYp.add (PolyBounded.const 1)).pow K))
+  have hVp : PolyBounded sz V :=
+    (((PolyBounded.of_polynomiallyBounded id hpG).comp hszp).add hszp).add
+      ((PolyBounded.const 2).mul (((PolyBounded.const a).mul
+        ((hszp.add (PolyBounded.const 1)).pow d)).add hUp))
+  obtain ⟨k₀, d₀, hV⟩ := hVp.exists_le
+  -- The simulation's time and space.
+  have htime (c : List Bool × ℕ) :
+      csim.time c ≤ V c * scheduleCount F.heads c.2 * E c := by
+    have hG := (bG c).1
+    have hVc : pG (sz c) + sz c + 2 * (a * (sz c + 1) ^ d + U c) = V c := rfl
+    have hcE : 1 ≤ scheduleCount F.heads c.2 * E c := Nat.one_le_iff_ne_zero.mpr
+      (Nat.mul_ne_zero (by have := hcnt1 c; omega) (by have := hE c; omega))
+    simp only [csim, cms, NativeCertificate.congr, NativeCertificate.branch_time,
+      NativeCertificate.const_time]
+    split_ifs with hc
+    · have hc' : c.1.length ≤ c.2 ∧ 2 ≤ c.2 := of_decide_eq_true hc
+      have hR : R c ≤ U c * E c :=
+        Finset.sup_le fun i hi => (hone c hc' i (Finset.mem_range.mp hi)).1
+      have h1 : (scheduleCount F.heads c.2 + 1) * (a * (sz c + 1) ^ d + R c) ≤
+          2 * (a * (sz c + 1) ^ d + U c) * (scheduleCount F.heads c.2 * E c) := by
+        have hAE : a * (sz c + 1) ^ d ≤ a * (sz c + 1) ^ d * E c := Nat.le_mul_of_pos_right _ (hE c)
+        calc _ ≤ (scheduleCount F.heads c.2 + 1) * (a * (sz c + 1) ^ d + U c * E c) :=
+              Nat.mul_le_mul_left _ (by omega)
+          _ ≤ (2 * scheduleCount F.heads c.2) * ((a * (sz c + 1) ^ d + U c) * E c) :=
+              Nat.mul_le_mul (by have := hcnt1 c; omega)
+                ((Nat.add_le_add_right hAE (U c * E c)).trans_eq (Nat.add_mul _ _ _).symm)
+          _ = _ := by ring
+      have h2 : pG (sz c) ≤ pG (sz c) * (scheduleCount F.heads c.2 * E c) :=
+        Nat.le_mul_of_pos_right _ hcE
+      calc _ ≤ pG (sz c) * (scheduleCount F.heads c.2 * E c) +
+            2 * (a * (sz c + 1) ^ d + U c) * (scheduleCount F.heads c.2 * E c) := by
+              simp only [sz] at hG h1 h2 ⊢
+              omega
+        _ ≤ V c * (scheduleCount F.heads c.2 * E c) := by
+              rw [← hVc, ← Nat.add_mul]
+              exact Nat.mul_le_mul_right _ (by omega)
+        _ = _ := by ring
+    · have h2 : pG (sz c) + sz c ≤ (pG (sz c) + sz c) * (scheduleCount F.heads c.2 * E c) :=
+        Nat.le_mul_of_pos_right _ hcE
+      calc _ ≤ (pG (sz c) + sz c) * (scheduleCount F.heads c.2 * E c) := by
+              simp only [sz] at hG h2 ⊢
+              omega
+        _ ≤ V c * (scheduleCount F.heads c.2 * E c) := Nat.mul_le_mul_right _ (by omega)
+        _ = _ := by ring
+  have hspace (c : List Bool × ℕ) : csim.space c ≤ V c := by
+    have hG := (bG c).2
+    simp only [csim, cms, NativeCertificate.congr, NativeCertificate.branch_space,
+      NativeCertificate.const_space]
+    split_ifs with hc
+    · have hc' : c.1.length ≤ c.2 ∧ 2 ≤ c.2 := of_decide_eq_true hc
+      have hQ : Q c ≤ U c := Finset.sup_le fun i hi => (hone c hc' i (Finset.mem_range.mp hi)).2
+      simp only [V, sz] at hG hQ ⊢
+      omega
+    · simp only [V, sz] at hG ⊢
+      omega
+  -- Absorb the constants.
+  set k := k₀ * 2 ^ d₀ + d₀ + K with hk
+  have hVk (c : List Bool × ℕ) : V c ≤ k * (c.1.length + c.2 + 1) ^ k := by
+    have hszc : sz c + 1 ≤ 2 * (c.1.length + c.2 + 1) := by
+      simp only [sz, length_encPair, encBits_apply, encUnary_apply, List.length_replicate]
+      omega
+    calc V c ≤ k₀ * (sz c + 1) ^ d₀ := hV c
+      _ ≤ k₀ * (2 * (c.1.length + c.2 + 1)) ^ d₀ :=
+          Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hszc _)
+      _ = k₀ * 2 ^ d₀ * (c.1.length + c.2 + 1) ^ d₀ := by rw [mul_pow, mul_assoc]
+      _ ≤ k * (c.1.length + c.2 + 1) ^ k :=
+          Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega))
+  refine ⟨k, csim.computes.mono_le (fun c => ?_) fun c => (hspace c).trans (hVk c)⟩
+  have hEk : E c ≤ 2 ^ (k * c.2 / Nat.sqrt (Nat.log 2 c.2)) :=
+    Nat.pow_le_pow_right (by norm_num)
+      (Nat.div_le_div_right (Nat.mul_le_mul_right _ (by omega)))
+  exact (htime c).trans (Nat.mul_le_mul (Nat.mul_le_mul_right _ (hVk c)) hEk)
+
+/-- **The count within time `2 ^ O(T / √(log T))` and polynomial space** (conditional on the
+interfaces). Let `T` be time-constructible with `max n 2 ≤ T n`, let `c ≥ 1`, and let `rule` be a
+polynomial-time function of a padded time, in unary, and a count, in binary. Given a network family
+for `count`, with `count x τ ≤ 2 ^ τ`, and a contraction algorithm, the function sending `x` to
+`rule` of the padded clock `τ = paddedTime (c * T |x|)` and of `count x τ` is computable within
+time `2 ^ (C * T n / √⌊log₂ (T n)⌋)` and space `T n ^ d` on inputs of length `n`, for constants `C`
+and `d`. -/
+theorem exists_computableInO_count (F : NetworkFamily encN value Admissible count)
+    (A : ContractionAlgorithm encN value Admissible) (hcount : ∀ x τ, count x τ ≤ 2 ^ τ)
+    {T : ℕ → ℕ} (hT : TimeConstructible T) (hTn : ∀ n, max n 2 ≤ T n) {c : ℕ} (hc : 1 ≤ c)
+    {β : Type} {encβ : β ↪ List Bool} {rule : ℕ × ℕ → β}
+    (hrule : ComputableInPolyTime rule (encPair encUnary encNat) encβ) :
+    ∃ C d : ℕ, ComputableInO
+      (fun x : List Bool =>
+        rule (paddedTime (c * T x.length), count x (paddedTime (c * T x.length))))
+      encBits encβ
+      (fun x => 2 ^ (C * T x.length / Nat.sqrt (Nat.log 2 (T x.length))))
+      (fun x => T x.length ^ d) := by
+  obtain ⟨k, hsim⟩ := exists_computableInO_simulate F A
+  -- Preparing the context `(x, c * T |x|)`, with the clock in unary.
+  have hmul : ComputableInPolyTime (fun n : ℕ => c * n) encUnary encUnary := by fun_prop
+  have htau : ComputableInPolyTime (fun p : List Bool × ℕ => paddedTime p.2)
+      (encPair encBits encUnary) encUnary := computableInPolyTime_paddedTime.comp (by fun_prop)
+  let cT : NativeCertificate (fun x : List Bool => T x.length) encBits encNat :=
+    ⟨_, _, hT.computableInO⟩
+  let cU : NativeCertificate (fun n : ℕ => n) encNat encUnary := ⟨_, _, ComputableInO.natToUnary⟩
+  let cX : NativeCertificate (fun x : List Bool => x) encBits encBits :=
+    NativeCertificate.linear (ComputableInO.of_eq fun _ => rfl)
+  let cpre : NativeCertificate (fun x : List Bool => (x, c * T x.length)) encBits
+      (encPair encBits encUnary) :=
+    cX.prod ((NativeCertificate.ofPolyTime hmul).comp (cU.comp cT))
+  let csim : NativeCertificate (simulate F) (encPair encBits encUnary) encNat := ⟨_, _, hsim⟩
+  let ctotal := (NativeCertificate.ofPolyTime hrule).comp
+    (((NativeCertificate.ofPolyTime htau).prod csim).comp cpre)
+  -- Monotone polynomial bounds of the polynomial-time pieces.
+  obtain ⟨pm, hpm, mm, bm⟩ := exists_mono_poly_cert hmul
+  obtain ⟨pt, hpt, mt, bt⟩ := exists_mono_poly_cert htau
+  obtain ⟨pr, hpr, mr, br⟩ := exists_mono_poly_cert hrule
+  let W : ℕ → ℕ := fun n => 2 * n + (n + 1) ^ 2 + pm n + pt (3 * n + 1) + pr (6 * n + 3) +
+    k * (2 * n + 1) ^ k + (n + n + pm n)
+  have hW : Cslib.PolynomiallyBounded W := by fun_prop
+  obtain ⟨a, e, hWa⟩ := Cslib.polynomiallyBounded_iff_le.mp hW
+  -- The cost at an input, in terms of the clock `t = c * T |x|`.
+  have hcost (x : List Bool) :
+      ctotal.time x ≤ W (c * T x.length) * scheduleCount F.heads (c * T x.length) *
+          2 ^ (k * (c * T x.length) / Nat.sqrt (Nat.log 2 (c * T x.length))) ∧
+        ctotal.space x ≤ W (c * T x.length) := by
+    simp only [ctotal, cpre, csim, cX, cT, cU, NativeCertificate.comp_time,
+      NativeCertificate.comp_space, NativeCertificate.prod_time, NativeCertificate.prod_space,
+      NativeCertificate.linear_time, NativeCertificate.linear_space, encBits_apply,
+      Function.comp_apply]
+    set n := x.length
+    set t := c * T n with ht
+    have hnT : n ≤ T n := (le_max_left _ _).trans (hTn n)
+    have h2T : 2 ≤ T n := (le_max_right _ _).trans (hTn n)
+    have hTt : T n ≤ t := Nat.le_mul_of_pos_left _ hc
+    have hnt : n ≤ t := hnT.trans hTt
+    have h2t : 2 ≤ t := h2T.trans hTt
+    have hτ := paddedTime_add_one_le h2t
+    have hcnt1 : 1 ≤ scheduleCount F.heads t := Nat.one_le_pow _ _ (by norm_num)
+    have hE : 1 ≤ 2 ^ (k * t / Nat.sqrt (Nat.log 2 t)) := Nat.one_le_two_pow
+    have hctx : (encPair encBits encUnary (x, t)).length ≤ 3 * t + 1 := by
+      simp only [length_encPair, encBits_apply, encUnary_apply, List.length_replicate]
+      omega
+    have hsimx : simulate F (x, t) = count x (paddedTime t) :=
+      simulate_eq F hnt h2t (hcount x _)
+    have hout : (encPair encUnary encNat (paddedTime t, simulate F (x, t))).length ≤ 6 * t + 3 := by
+      have h1 : (encUnary (paddedTime t)).length = paddedTime t := by
+        simp only [encUnary_apply, List.length_replicate]
+      have h2 : (encNat (simulate F (x, t))).length ≤ paddedTime t + 1 := by
+        rw [hsimx]
+        calc _ ≤ (encNat (2 ^ paddedTime t)).length := length_encNat_mono (hcount x _)
+          _ = paddedTime t + 1 := by rw [length_encNat_eq_size, Nat.size_pow]
+      simp only [length_encPair]
+      omega
+    have hTu : (encUnary (T n)).length ≤ t := by
+      simp only [encUnary_apply, List.length_replicate]
+      exact hTt
+    have hmT := (bm (T n)).1.trans (mm hTu)
+    have hmS := (bm (T n)).2.trans (mm hTu)
+    have htT := (bt (x, t)).1.trans (mt hctx)
+    have htS := (bt (x, t)).2.trans (mt hctx)
+    have hrT := (br (paddedTime t, simulate F (x, t))).1.trans (mr hout)
+    have hrS := (br (paddedTime t, simulate F (x, t))).2.trans (mr hout)
+    have hpow : k * (n + t + 1) ^ k ≤ k * (2 * t + 1) ^ k :=
+      Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) _)
+    have hsq : (T n + 1) ^ 2 ≤ (t + 1) ^ 2 := Nat.pow_le_pow_left (by omega) _
+    constructor
+    · have hsimT : k * (n + t + 1) ^ k * scheduleCount F.heads t *
+          2 ^ (k * t / Nat.sqrt (Nat.log 2 t)) ≤
+          k * (2 * t + 1) ^ k *
+            (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) := by
+        rw [Nat.mul_assoc]
+        exact Nat.mul_le_mul_right _ hpow
+      have hrest : 2 * t + (t + 1) ^ 2 + pm t + pt (3 * t + 1) + pr (6 * t + 3) ≤
+          (2 * t + (t + 1) ^ 2 + pm t + pt (3 * t + 1) + pr (6 * t + 3)) *
+            (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) :=
+        Nat.le_mul_of_pos_right _ (Nat.mul_pos hcnt1 hE)
+      have hWt : W t * scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t)) =
+          W t * (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) := by ring
+      rw [hWt]
+      have hWle : (2 * t + (t + 1) ^ 2 + pm t + pt (3 * t + 1) + pr (6 * t + 3)) *
+            (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) +
+          k * (2 * t + 1) ^ k * (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) ≤
+          W t * (scheduleCount F.heads t * 2 ^ (k * t / Nat.sqrt (Nat.log 2 t))) := by
+        rw [← Nat.add_mul]
+        exact Nat.mul_le_mul_right _ (by simp only [W]; omega)
+      omega
+    · simp only [W]
+      omega
+  -- Absorb the cost into `2 ^ O(T / √(log T))` and `T ^ O(1)`.
+  obtain ⟨C, hC⟩ := Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two F.heads c e k
+  refine ⟨(a + 0 + 1) * (C + 1), a * c ^ e + 0 + 2 * e,
+    (ctotal.computes.of_enc_eq fun x => congrArg encβ ?_).mono_le (fun x => ?_) fun x => ?_⟩
+  · have hnt : x.length ≤ c * T x.length :=
+      ((le_max_left _ _).trans (hTn _)).trans (Nat.le_mul_of_pos_left _ hc)
+    have h2t : 2 ≤ c * T x.length :=
+      ((le_max_right _ _).trans (hTn _)).trans (Nat.le_mul_of_pos_left _ hc)
+    simp only [Function.comp_apply]
+    rw [simulate_eq F hnt h2t (hcount x _)]
+  · set n := x.length
+    have h2T : 2 ≤ T n := (le_max_right _ _).trans (hTn n)
+    have hcostT := (hcost x).1
+    have hWt := hWa (c * T n)
+    have hmain : 3 ^ (F.heads * (c * T n ⌈/⌉ Nat.clog 2 (c * T n + 2))) * (c * T n + 1) ^ e *
+        2 ^ (k * (c * T n) / Nat.sqrt (Nat.log 2 (c * T n))) ≤
+        2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) := hC (T n) h2T
+    have habs := Nat.mul_two_pow_div_sqrt_log_two_add_le (a := a) (b := 0) (C := C) h2T
+    calc ctotal.time x ≤ W (c * T n) * scheduleCount F.heads (c * T n) *
+          2 ^ (k * (c * T n) / Nat.sqrt (Nat.log 2 (c * T n))) := hcostT
+      _ ≤ a * (c * T n + 1) ^ e * scheduleCount F.heads (c * T n) *
+          2 ^ (k * (c * T n) / Nat.sqrt (Nat.log 2 (c * T n))) :=
+          Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ hWt)
+      _ = a * (3 ^ (F.heads * (c * T n ⌈/⌉ Nat.clog 2 (c * T n + 2))) * (c * T n + 1) ^ e *
+          2 ^ (k * (c * T n) / Nat.sqrt (Nat.log 2 (c * T n)))) := by
+          simp only [scheduleCount, numBlocks, blockLength]
+          ring
+      _ ≤ a * 2 ^ (C * T n / Nat.sqrt (Nat.log 2 (T n))) + 0 := by
+          rw [Nat.add_zero]
+          exact Nat.mul_le_mul_left _ hmain
+      _ ≤ _ := habs
+  · set n := x.length
+    have h2T : 2 ≤ T n := (le_max_right _ _).trans (hTn n)
+    have hspace := (hcost x).2
+    have hWt := hWa (c * T n)
+    have hct : c * T n + 1 ≤ c * (T n + 1) := by nlinarith
+    calc ctotal.space x ≤ a * (c * T n + 1) ^ e := hspace.trans hWt
+      _ ≤ a * (c * (T n + 1)) ^ e := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hct _)
+      _ = a * c ^ e * (T n + 1) ^ e + 0 := by rw [mul_pow, Nat.mul_assoc, add_zero]
+      _ ≤ T n ^ (a * c ^ e + 0 + 2 * e) := Nat.mul_add_one_pow_add_le_pow h2T
+
+end Cslib.Complexity.CountingSimulation
diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Interfaces.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Interfaces.lean
new file mode 100644
index 000000000..d00a0135c
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/CountingSimulation/Interfaces.lean
@@ -0,0 +1,165 @@
+/-
+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.GenericRAM.Native.Certificate
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary
+public import Complexity.Foundations.Data.Nat.CeilDiv
+public import Mathlib.Data.Nat.Log
+public import Mathlib.Data.Nat.Sqrt
+import Mathlib.Tactic.Linarith
+
+/-!
+# Interfaces of the deterministic counting simulation
+
+The deterministic simulation of nondeterministic and probabilistic time by blocking and tensor
+contraction (#1833) has two ingredients that are formalized separately. This module states them as
+interfaces, so that the assembly (`Cslib.Complexity.CountingSimulation.exists_computableInO_count`)
+can be proved from them, and each can be discharged on its own.
+
+**Parameters.** A run of `t` steps is cut into `numBlocks t = ⌈t / b⌉` intervals of
+`blockLength t = b = ⌈log₂ (t + 2)⌉` steps and padded to `paddedTime t = numBlocks t * b ≥ t`
+steps. Each of `heads` blocked heads moves by at most one block per interval, so a run has one of
+at most `3 ^ (heads * numBlocks t)` movement schedules.
+
+**Networks** (`Cslib.Complexity.CountingSimulation.NetworkFamily`). A network for each input `x`,
+clock `t` and schedule `σ`, built in polynomial time from `x`, `t` in unary and `σ` in binary,
+whose values sum to the count being simulated at the padded time. Each network is admissible for
+the contraction algorithm at size `t`, with a constant of the family. This is the block-counting
+step of #1833 (milestone H3): blocking after Hopcroft, Paul and Valiant, with a Boolean tensor
+network for each schedule whose contraction counts the accepting choice strings with that
+schedule. It is new mathematics, not a cited result.
+
+**Contraction** (`Cslib.Complexity.CountingSimulation.ContractionAlgorithm`). One native machine
+that, given a precision `P` and a network `G`, outputs `value G % 2 ^ P`, and that, on networks
+admissible at a size `s ≥ 2` with `1 ≤ P ≤ D * s`, runs within time
+`K * (n + 1) ^ K * 2 ^ (K * s / √⌊log₂ s⌋)` and space `K * (n + 1) ^ K`, where `n` is the encoded
+length of `(P, G)` and `K` depends only on the constants. This is the form in which the
+simulation uses the Boolean tensor contraction theorem [OpenAI2026ETH, Theorem D.1] with `ℓ = 1`
+and maximum degree `O(log s)` (milestone T2 of #1833), with the exponent in the natural-number
+scale of `Nat.exists_three_pow_mul_le_two_pow_div_sqrt_log_two`. Like Theorem D.1 it is
+parameterized by a size `s` bounding the number of edges and the precision, rather than by the
+number of edges itself.
+
+Both interfaces are generic in the representation of networks: their type `N`, its encoding, the
+contracted `value : N → ℕ` and the admissibility predicate `Admissible C s G` are parameters. The
+intended instance takes `N` to be an explicit Boolean tensor network with its bipartition,
+`value` its contraction, and `Admissible C s G` to say that `G` is bipartite with at most `C * s`
+edges and maximum degree at most `C * log₂ s`.
+
+## Main definitions
+
+* `Cslib.Complexity.CountingSimulation.blockLength`, `numBlocks`, `paddedTime`, `scheduleCount`:
+  the blocking parameters.
+* `Cslib.Complexity.CountingSimulation.ContractionAlgorithm`: the contraction interface.
+* `Cslib.Complexity.CountingSimulation.NetworkFamily`: the network interface.
+
+## Main results
+
+* `Cslib.Complexity.CountingSimulation.le_paddedTime`: padding never shortens a run.
+* `Cslib.Complexity.CountingSimulation.paddedTime_add_one_le`: from `t = 2` on, the padded time
+  and one more fit in `2 * t`.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem D.1 (contraction).
+-/
+
+public section
+
+namespace Cslib.Complexity.CountingSimulation
+
+open Turing.MultiTapeTM Cslib.GenericRAM
+
+/-! ### Blocking parameters -/
+
+/-- The length `⌈log₂ (t + 2)⌉` of a time interval for a clock `t`. -/
+@[expose] def blockLength (t : ℕ) : ℕ := Nat.clog 2 (t + 2)
+
+/-- The number `⌈t / blockLength t⌉` of time intervals for a clock `t`. -/
+@[expose] def numBlocks (t : ℕ) : ℕ := t ⌈/⌉ blockLength t
+
+/-- The padded running time `numBlocks t * blockLength t`, a whole number of intervals. -/
+@[expose] def paddedTime (t : ℕ) : ℕ := numBlocks t * blockLength t
+
+/-- The number `3 ^ (heads * numBlocks t)` of movement schedules of `heads` blocked heads. -/
+@[expose] def scheduleCount (heads t : ℕ) : ℕ := 3 ^ (heads * numBlocks t)
+
+/-- An interval has at least one step. -/
+theorem one_le_blockLength (t : ℕ) : 1 ≤ blockLength t :=
+  Nat.succ_le_of_lt (Nat.clog_pos one_lt_two (by omega))
+
+/-- **Padding never shortens a run**: `t ≤ paddedTime t`. -/
+theorem le_paddedTime (t : ℕ) : t ≤ paddedTime t :=
+  Nat.le_ceilDiv_mul (one_le_blockLength t)
+
+private theorem add_two_le_two_pow {t : ℕ} (ht : 2 ≤ t) : t + 2 ≤ 2 ^ t := by
+  induction t, ht using Nat.le_induction with
+  | base => norm_num
+  | succ n hn ih => rw [pow_succ]; omega
+
+/-- An interval is no longer than the clock, from `t = 2` on. -/
+theorem blockLength_le {t : ℕ} (ht : 2 ≤ t) : blockLength t ≤ t :=
+  Nat.clog_le_of_le_pow (add_two_le_two_pow ht)
+
+/-- **The padded time stays linear**: from `t = 2` on, `paddedTime t + 1 ≤ 2 * t`, since padding
+adds less than one interval. -/
+theorem paddedTime_add_one_le {t : ℕ} (ht : 2 ≤ t) : paddedTime t + 1 ≤ 2 * t := by
+  have h := Nat.ceilDiv_mul_lt (a := t) (one_le_blockLength t)
+  have := blockLength_le ht
+  unfold paddedTime numBlocks
+  omega
+
+/-! ### The interfaces -/
+
+/-- **The contraction interface** (the Boolean tensor contraction theorem, as the simulation uses
+it). One native certificate computes `value G % 2 ^ P` from the precision `P` in binary and the
+network `G`. For all constants `C` and `D` there is `K` such that on every network admissible at a
+size `s ≥ 2` with constant `C`, and every precision `1 ≤ P ≤ D * s`, the certificate's time is at
+most `K * (n + 1) ^ K * 2 ^ (K * s / √⌊log₂ s⌋)` and its space at most `K * (n + 1) ^ K`, where `n`
+is the encoded length of `(P, G)`. Outside admissible inputs the certificate need only be
+correct. -/
+structure ContractionAlgorithm {N : Type} (encN : N ↪ List Bool) (value : N → ℕ)
+    (Admissible : ℕ → ℕ → N → Prop) where
+  /-- The native contraction modulo `2 ^ P`. -/
+  certificate : NativeCertificate (fun p : ℕ × N => value p.2 % 2 ^ p.1) (encPair encNat encN)
+    encNat
+  /-- Its time and space on admissible inputs. -/
+  bound : ∀ C D : ℕ, ∃ K : ℕ, ∀ (s P : ℕ) (G : N), 2 ≤ s → 1 ≤ P → P ≤ D * s →
+    Admissible C s G →
+      certificate.time (P, G) ≤ K * ((encPair encNat encN (P, G)).length + 1) ^ K *
+          2 ^ (K * s / Nat.sqrt (Nat.log 2 s)) ∧
+        certificate.space (P, G) ≤ K * ((encPair encNat encN (P, G)).length + 1) ^ K
+
+/-- **The network interface** (the block-counting lemma, as the simulation uses it), for a count
+`count x τ` of the inputs `x` at padded time `τ`, such as the number of accepting choice strings of
+length `τ` of a fair-coin machine. The family has a number of blocked heads and an admissibility
+constant. Its network for the input `x`, the clock `t` and the schedule `σ` is computable in
+polynomial time from `x`, `t` in unary and `σ` in binary. Whenever `|x| ≤ t` and `2 ≤ t`, the
+values of the networks of the `scheduleCount heads t` schedules sum to `count x (paddedTime t)`,
+and each of these networks is admissible at size `t`. -/
+structure NetworkFamily {N : Type} (encN : N ↪ List Bool) (value : N → ℕ)
+    (Admissible : ℕ → ℕ → N → Prop) (count : List Bool → ℕ → ℕ) where
+  /-- The number of blocked heads. -/
+  heads : ℕ
+  /-- The admissibility constant. -/
+  constant : ℕ
+  /-- The network of an input, a clock and a schedule. -/
+  net : List Bool × ℕ × ℕ → N
+  /-- The networks are built in polynomial time, with the clock in unary. -/
+  polyTime : ComputableInPolyTime net (encPair encBits (encPair encUnary encNat)) encN
+  /-- **The counting identity**: the values of the networks of all schedules sum to the count at
+  the padded time. -/
+  sum_value : ∀ x t, x.length ≤ t → 2 ≤ t →
+    ∑ σ ∈ Finset.range (scheduleCount heads t), value (net (x, t, σ)) = count x (paddedTime t)
+  /-- Every network of a schedule is admissible at size `t`. -/
+  admissible : ∀ x t σ, x.length ≤ t → 2 ≤ t → σ < scheduleCount heads t →
+    Admissible constant t (net (x, t, σ))
+
+end Cslib.Complexity.CountingSimulation
diff --git a/ComplexityTests/CountingSimulation.lean b/ComplexityTests/CountingSimulation.lean
new file mode 100644
index 000000000..d6b681f0d
--- /dev/null
+++ b/ComplexityTests/CountingSimulation.lean
@@ -0,0 +1,157 @@
+/-
+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.CountingSimulation.Assembly
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryLog
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div
+import Mathlib.Data.Nat.Size
+
+/-! Checks for the conditional assembly of the counting simulation (#1833): the streamed modular
+sum on concrete terms, the blocking parameters, and toy instances of both interfaces, which show
+that the hypotheses of `Cslib.Complexity.CountingSimulation.exists_computableInO_count` can be met.
+
+The toy instances are deliberately trivial: a "network" is a natural number that is its own value,
+the contraction reduces it modulo `2 ^ P`, every network is admissible, and the counted quantity
+is `2 ^ τ`, the number of all choice strings of length `τ`, carried by the first of
+`scheduleCount 1 t` schedules. They exercise the algorithm and its bounds, not the tensor
+networks of the intended instance. -/
+
+namespace ComplexityTests.CountingSimulation
+
+open Turing.MultiTapeTM Cslib.GenericRAM Cslib.Complexity.CountingSimulation
+
+/-! ### The streamed sum -/
+
+/-- `0 + 1 + 2 + 3 = 6` below the modulus `7`. -/
+example : modSum (fun p : Unit × ℕ => p.2) (fun _ => 7) (fun _ => 4) () = 6 := by
+  rw [modSum_eq_sum_mod]
+  decide
+
+/-- The residue wraps around: `(0 + 1 + 2 + 3 + 4) % 4 = 2`. -/
+example : modSum (fun p : Unit × ℕ => p.2) (fun _ => 4) (fun _ => 5) () = 2 := by
+  rw [modSum_eq_sum_mod]
+  decide
+
+/-- With no terms the sum is zero, whatever the modulus. -/
+example : modSum (fun p : Unit × ℕ => p.2 + 1) (fun _ => 5) (fun _ => 0) () = 0 := by
+  rw [modSum_eq_sum_mod]
+  rfl
+
+/-! ### Blocking parameters -/
+
+/-- With clock `6`, intervals of `⌈log₂ 8⌉ = 3` steps, two of them, and no padding. -/
+example : blockLength 6 = 3 ∧ numBlocks 6 = 2 ∧ paddedTime 6 = 6 := by
+  refine ⟨?_, ?_, ?_⟩ <;> decide
+
+/-- With clock `7`, intervals of `⌈log₂ 9⌉ = 4` steps, and one step of padding. -/
+example : blockLength 7 = 4 ∧ numBlocks 7 = 2 ∧ paddedTime 7 = 8 := by
+  refine ⟨?_, ?_, ?_⟩ <;> decide
+
+/-- Two blocked heads over two intervals have `3 ^ 4` movement schedules. -/
+example : scheduleCount 2 6 = 81 := by decide
+
+example : paddedTime 7 + 1 ≤ 2 * 7 := paddedTime_add_one_le (by norm_num)
+
+/-! ### A toy contraction algorithm -/
+
+/-- Reducing modulo `2 ^ P` only needs the low `min (size n) P` bits. -/
+theorem mod_two_pow_min_size (n P : ℕ) : n % 2 ^ min (Nat.size n) P = n % 2 ^ P := by
+  rcases le_total (Nat.size n) P with h | h
+  · rw [min_eq_left h, Nat.mod_eq_of_lt (Nat.lt_size_self n),
+      Nat.mod_eq_of_lt ((Nat.lt_size_self n).trans_le (Nat.pow_le_pow_right two_pos h))]
+  · rw [min_eq_right h]
+
+theorem computableInPolyTime_mod_two_pow :
+    ComputableInPolyTime (fun p : ℕ × ℕ => p.2 % 2 ^ p.1) (encPair encNat encNat) encNat := by
+  have h : ComputableInPolyTime (fun p : ℕ × ℕ => p.2 % 2 ^ min (Nat.size p.2) p.1)
+      (encPair encNat encNat) encNat := by fun_prop
+  simpa only [mod_two_pow_min_size] using h
+
+/-- The contraction interface for networks that are their own values, all admissible: a
+polynomial-time reduction modulo `2 ^ P` meets every bound. -/
+noncomputable def toyContraction :
+    ContractionAlgorithm encNat (fun n : ℕ => n) (fun _ _ _ => True) where
+  certificate := NativeCertificate.ofPolyTime computableInPolyTime_mod_two_pow
+  bound C D := by
+    obtain ⟨p, hp, -, hb⟩ := exists_mono_poly_cert computableInPolyTime_mod_two_pow
+    obtain ⟨a, d, hpa⟩ := Cslib.polynomiallyBounded_iff_le.mp hp
+    refine ⟨a + d, fun s P G _ _ _ _ => ?_⟩
+    have hpow : a * ((encPair encNat encNat (P, G)).length + 1) ^ d ≤
+        (a + d) * ((encPair encNat encNat (P, G)).length + 1) ^ (a + d) :=
+      Nat.mul_le_mul (by omega) (Nat.pow_le_pow_right (by omega) (by omega))
+    have hE : 1 ≤ 2 ^ ((a + d) * s / Nat.sqrt (Nat.log 2 s)) := Nat.one_le_two_pow
+    have hT := (hb (P, G)).1.trans (hpa _)
+    have hS := (hb (P, G)).2.trans (hpa _)
+    exact ⟨hT.trans (hpow.trans (Nat.le_mul_of_pos_right _ hE)), hS.trans hpow⟩
+
+/-! ### A toy network family -/
+
+theorem computableInPolyTime_toyNet :
+    ComputableInPolyTime (fun p : List Bool × ℕ × ℕ => 2 ^ paddedTime p.2.1 * (1 - p.2.2))
+      (encPair encBits (encPair encUnary encNat)) encNat := by
+  simp only [paddedTime, numBlocks, blockLength, Nat.ceilDiv_eq_add_pred_div]
+  fun_prop
+
+/-- The count `2 ^ τ` of all choice strings of length `τ`, carried by the network of the first of
+`scheduleCount 1 t` schedules; the others have value zero. -/
+noncomputable def toyFamily :
+    NetworkFamily encNat (fun n : ℕ => n) (fun _ _ _ => True) (fun _ τ => 2 ^ τ) where
+  heads := 1
+  constant := 0
+  net p := 2 ^ paddedTime p.2.1 * (1 - p.2.2)
+  polyTime := computableInPolyTime_toyNet
+  sum_value x t _ _ := by
+    have h0 : 0 ∈ Finset.range (scheduleCount 1 t) :=
+      Finset.mem_range.mpr (Nat.one_le_pow _ _ (by norm_num))
+    rw [Finset.sum_eq_single_of_mem 0 h0 fun σ _ hσ => by
+      rw [Nat.sub_eq_zero_of_le (Nat.one_le_iff_ne_zero.mpr hσ), Nat.mul_zero]]
+    rw [Nat.sub_zero, Nat.mul_one]
+  admissible _ _ _ _ _ _ := trivial
+
+/-- The simulation computes the count on a concrete input and clock. -/
+example : simulate toyFamily ([true, false], 5) = 2 ^ paddedTime 5 :=
+  simulate_eq toyFamily (by decide) (by norm_num) le_rfl
+
+/-- On an input that is too long for its clock the simulation outputs `0`. -/
+example : simulate toyFamily ([true, false, true], 2) = 0 := by
+  simp [simulate]
+
+/-! ### The conditional endpoint on the toy instances -/
+
+/-- `T n = 2 ^ 2 ^ n` meets the bound `max n 2 ≤ T n` of the endpoint. -/
+theorem max_le_two_pow_two_pow (n : ℕ) : max n 2 ≤ 2 ^ 2 ^ n :=
+  max_le (Nat.lt_two_pow_self.le.trans (Nat.pow_le_pow_right (by norm_num)
+    Nat.lt_two_pow_self.le))
+    (calc 2 = 2 ^ 2 ^ 0 := by norm_num
+      _ ≤ 2 ^ 2 ^ n :=
+        Nat.pow_le_pow_right (by norm_num) (Nat.pow_le_pow_right (by norm_num) (Nat.zero_le n)))
+
+/-- With the toy interfaces and the time-constructible `T n = 2 ^ 2 ^ n ≥ max n 2`, the count at
+the padded clock is computable within time `2 ^ O(T / √(log T))` and space `T ^ O(1)`. -/
+example : ∃ C d : ℕ, ComputableInO
+    (fun x : List Bool => 2 ^ paddedTime (1 * 2 ^ 2 ^ x.length)) encBits encNat
+    (fun x => 2 ^ (C * 2 ^ 2 ^ x.length / Nat.sqrt (Nat.log 2 (2 ^ 2 ^ x.length))))
+    (fun x => (2 ^ 2 ^ x.length) ^ d) :=
+  exists_computableInO_count toyFamily toyContraction (fun _ _ => le_rfl)
+    Cslib.Complexity.timeConstructible_two_pow_two_pow
+    max_le_two_pow_two_pow
+    le_rfl (rule := Prod.snd) (by fun_prop)
+
+/-- The strict-majority comparison `2 ^ τ < 2 * count` used for `BPTIME` and `PPTIME` is a
+polynomial-time rule because the padded time is passed in unary. On the toy family every string
+is accepted, so the rule accepts every input. -/
+example : ∃ C d : ℕ, ComputableInO
+    (fun x : List Bool => decide (2 ^ paddedTime (1 * 2 ^ 2 ^ x.length) <
+      2 * 2 ^ paddedTime (1 * 2 ^ 2 ^ x.length))) encBits encBool
+    (fun x => 2 ^ (C * 2 ^ 2 ^ x.length / Nat.sqrt (Nat.log 2 (2 ^ 2 ^ x.length))))
+    (fun x => (2 ^ 2 ^ x.length) ^ d) :=
+  exists_computableInO_count toyFamily toyContraction (fun _ _ => le_rfl)
+    Cslib.Complexity.timeConstructible_two_pow_two_pow
+    max_le_two_pow_two_pow
+    le_rfl (rule := fun p => decide (2 ^ p.1 < 2 * p.2)) (by fun_prop)
+
+end ComplexityTests.CountingSimulation