Failure of the coding theorem for randomized stopping machines

Epistemic Status and Contributions. This post explains a technical separation result in algorithmic information theory which was derived during Mikhail Mironov's Summer 2026 PIBBSS fellowship. The result contributes to AIXI Labs' research program on how Solomonoff induction generalizes from past observations in the face of novel events.
Problem formulation: Cole Wyeth.
Proof of main Theorem 1: GPT-5.6 Sol.
Appendix proofs: the sketch of the proof for equivalence between time semimeasures and randomized stopping machines is by Cole Wyeth, the rest by GPT-6 Astra.
Writing: draft by Claude Fable 5 and GPT-6 Astra, editing and rewriting by Mikhail Mironov.
Useful discussions: Aram Ebtekar, Cole Wyeth.
Funding and organization: summer 2026 PIBBSS fellowship.

Introduction

This post studies a stopping complexity, an analogue of Kolmogorov complexity from classical algorithmic information theory. It is motivated by the Golden Handcuffs (GH) AI safety agenda of Aram Ebtekar and Michael K. Cohen. GH is a way to make a universal agent safer, by making it delegate control to a mentor in special cases described below, which prevents the agent from exploring novel high-reward schemes or novel dangerous activities. The safety guarantee of GH is formulated in terms of simple stopping events along the agent's history: no decidable low-complexity predicate is triggered by the agent before a mentor would trigger it. For instance, the agent will never trigger the low-complexity predicate "drop anvil onto its own head", unless the mentor triggers it first. The stopping complexity was introduced in earlier works, but its application to safety is a novel contribution of GH.

A cartoon example: a Golden Handcuffs agent and a simple stopping event

A GH agent believes that its possible rewards are either in or equal to the catastrophic reward . In practice agent always receives reward from , so from its perspective rewards are close to the maximum. When the estimated probability of the catastrophic reward is high (that is, the estimated future value is below some threshold), the agent must call a safe mentor.

Picture a warehouse robot whose history so far is thousands of repetitions of the same routine: lift a box, put it on the conveyor belt, get a reward. Its sensors have never once reported the belt stalled. One day the optimizing part of the robot notices a shortcut: putting a box under the belt would stall it for a moment and, by its estimate, could slightly raise the reward. The moment at which the belt first stalls is novel in a precise sense: the short computable rule "watch the sensor stream and halt at the first stall" halts exactly there. Under a universal prior, the history up to that moment is therefore explained, with non-negligible weight, by hypotheses of the form "the world behaves as before until the first stall, and then differently", where "differently" includes the catastrophic reward of GH. The robot has been collecting near-maximal rewards (from ), so the shortcut has almost nothing to gain and, subjectively, a lot to lose. The pessimistic optimizer ranks the plan far below the routine: it is afraid of its own plan and does not carry it out.

Should the belt stall through no choice of the robot, the robot finds itself at a novel moment where cannot be ruled out. Its predicted future value drops below the GH threshold, so the robot hands control to the mentor, a human operator who, say, clears the jam. From then on stalls are no longer unprecedented. The rule "the first stall" no longer picks out the present moment, and later stalls are picked out only by longer rules ("the -th stall"). The fear of stalls decreases and the optimizer is allowed back in control, potentially copying the mentor's behavior, that is, clearing the jam the next time the belt stalls.

There are two ways to score how novel a moment is: by its shortest stopping rule, or by the total weight of all stopping rules that halt there. These are the two quantities compared in this post.

Stopping complexity measures when a simple computable rule is violated, which could be interpreted as a universal measure of novelty, and this gives motivation to study stopping complexity even regardless of GH.

For ordinary prefix-free machines, Kolmogorov complexity and a priori probability are connected: Levin's coding theorem states that . That is, the largest term of the sum already captures the whole sum up to a constant factor. An explanation with a full proof is Leon Lang's post on the coding theorem.

An analogous question can be asked in the setting of stopping machines. We use randomized stopping machines, that is our programs have access to infinite random seeds. We define monotone stopping complexity as the length of the shortest program-plus-seed that stops on a particular string, and a priori stopping probability as the total weight of all programs-plus-seeds stopping on a particular string (the notation follows GH Definition 4). Then the analogue of the coding theorem is: is it true that ? This post proves that the answer is negative: the gap is not bounded by a constant ().

The gap is bounded in terms of , the following inequality holds: , where is the ordinary prefix complexity of an integer (, proved in the ).

Prior work. The separation itself is not new as a statement. Vovk and Pavlovic(remark at the end of their Section 8) attribute an unbounded gap of this kind, for their notion of intermediate time complexity, to Mikhail Andreev, citing an unpublished manuscript of Andreev and Alexander Shen. The published Andreev–Posobin–Shen paper treats the plain version and explicitly postpones the prefix versions. We know of no published proof. The shows that the result announced by Mikhail Andreev implies . The proof below is independent and self-contained. We claim no novelty for the separation itself, the contributions of this post are the accessible proof and the connection to the safety construction of GH.

Connection with GH. We adopt the GH notation , . The verifies that the definitions given below agree with GH's Definition 4 up to an additive and a multiplicative constant respectively.

The GH safety trigger (their Theorem 5) is stated in terms of , while the interpretable complexity bound (their eq. 11–12 and Corollary 6) uses . shows that and are not within an additive constant: a short stopping description always satisfies the trigger condition, but the trigger can also fire where novelty mass is spread across many stopping criteria, none of which is individually short.

Audience. Basic familiarity with Turing machines is assumed. Familiarity with Kolmogorov complexity and a priori probability is useful, but not necessary. Otherwise, the argument is self-contained.

Notation

. and are the finite binary strings and infinite binary sequences, is the empty string, and is the uniform measure on . We write if is a prefix of , and if moreover . Strings are comparable if one is a prefix of the other and incomparable () otherwise, which happens exactly when they disagree at some position not exceeding both lengths. A set of pairwise comparable strings is a chain, a set of pairwise incomparable strings is an antichain (= prefix-free set). A cell of depth is a string , viewed as the cylinder of measure , or as the dyadic subinterval of whose binary representation starts with . Note that two cells are disjoint iff their strings are incomparable.

1. The coding-theorem formulation

A randomized stopping machine is a deterministic machine with a one-way read-only input tape and a one-way read-only random tape. In the course of its computation, it may issue three special instructions: request the next input bit, request the next random bit, or halt. Between two requests it may compute for arbitrarily many steps (formally, it is a Turing machine with the two read-only tapes and a two-way work tape), and a run may never halt and never make another request. The machine sees only the bits it has requested, so its behavior up to any moment depends only on the strings consumed so far. A string is a witness for if the run of on any input beginning with , with any random tape beginning with , halts having consumed exactly the input and exactly the random bits ; in this case we write . For fixed the witnesses form an antichain: a run fed comparable witnesses would halt with consumption and with consumption , so . The witness cylinders are therefore pairwise disjoint, and the following stopping probability and stopping complexity are well defined:

Example 1. Let read input bits one at a time and halt as soon as the last two bits read are both . It never requests a random bit. stops exactly at the strings ending in with no earlier occurrence of , so is the indicator of that set and on it.

Example 2. Let repeat: request a random bit, halt if it is , and otherwise request an input bit. Its only witness for is , so and for every .

Fix an effective enumeration of all randomized stopping machines and a computable prefix-free code of their indices, and put . The universal randomized stopping machine reads some from its random tape (running forever if the tape extends no element of ), then simulates on the input tape and the rest of the random tape, which is informally interpreted as a random seed for . Define

We call the a priori stopping probability and the monotone stopping complexity. The notation matches GH, whose definitions agree with these up to the constants (see the ). Thus is the probability that halts consuming exactly the input , is the largest single term of the witness sum , and holds trivially. The coding-theorem question asks whether also . The answer is negative.

Informal (Theorem 1)

The best single description-plus-seed program for can be arbitrarily much longer than of the total mass that all programs together give to .

Theorem 1

For every constant there is with . Equivalently, .

The theorem is proved by reduction to a game, which relies on the following two lemmas.

Informal (Lemmas 2 and 3)

Lemma 2 shows that the intervals witnessing the stopping points along one input path are pairwise disjoint, that is they all stay inside a single unit of measure of description-plus-seed addresses.
Lemma 3 shows why interpretation of "program plus seed" is valid in our construction with universal randomized stopping machine .

Lemma 2

Let be a randomized stopping machine and . If and , then .

Proof

Suppose are comparable. Take one input beginning with and one random tape beginning with the longer of . The single deterministic run of on this data satisfies the defining condition of both witnesses, so it halts having consumed exactly and exactly , whence , a contradiction. ∎

Lemma 3

if and only if with and . Hence and .

Proof

A run of halts with exact consumption iff it first consumes exactly a prefix of , and then the simulated halts consuming exactly and exactly the rest of , i.e. . The split is unique since is prefix-free. ∎

shows, in particular, that a different choice of the enumeration changes by at most an additive and by at most a multiplicative constant. The mixture formula mirrors the classical picture of a priori probability: with probability the first random bits specify the machine , and the remaining random tape serves as its seed.

2. The coding game

In this section we formulate a combinatorial game between Alice and Bob and state that Alice has a winning strategy in it (, which we prove in Section 5). In Section 3 we prove based on Alice's winning strategy.

Informal (game )

Suppose that the coding theorem is true for some constant (equivalently, is false for this ). Alice tries to disprove the coding theorem, Bob tries to defend it. Alice declares that the total mass of at is , and then Bob answers with a short program-plus-seed of weight at least . That is, Bob has a discount factor of .

Note that total mass of along every path is at most , so Alice has the corresponding constraint on her declarations.

The constraint for Bob's answers is : for comparable strings his answers must be incomparable.

The game (). Alice's move is a declaration , , , of weight . Each string is declared at most once. Alice has the following constraint on total weight along every path:

Bob answers each declaration immediately with a string , , and the answers at distinct comparable strings must be pairwise prefix-incomparable. Alice wins if Bob has no legal answer.

Theorem 4

For every there is such that Alice has a computable winning strategy in , with all path loads at most (we define exactly in ).

Theorem 4 is proved in Section 5. For now let us assume is true, and prove based on it.

3. The diagonalization: Theorem 4 ⇒ Theorem 1

Informal (Theorem 4 ⇒ Theorem 1)

(proved in Section 5) states that for every Alice has a winning strategy for . Run Alice's strategy for every simultaneously in disjoint subtrees at tags , that is at Her declarations assemble into one lower-semicomputable time semimeasure. By the proved in the Appendix, an l.s.c. time semimeasure is the same as the stopping probability of some machine . Denote the description length of by . Note that is included in with coefficient (by ). Alice's victory at tag with parameter produces such that its exceeds by more than . Thus its also exceeds by more than . Since Alice wins for every this proves .

The algorithm runs forever and enumerates the mass function from below (initially everywhere). The algorithm dovetails, for every , Alice's -strategy of , played inside the subtree rooted at the tag . The tags form an antichain, so every infinite path enters at most one subtree. When Alice's -strategy for parameter declares , the algorithm:

1. assigns where (thus each receiving mass at most once),
2. dovetail-searches through all strings with for one that is a witness for w.r.t. ,
3. if one is found, records it as Bob's answer and lets the strategy continue. If no such witness exists the search runs forever, corresponding to Alice's victory at this tag.

Suppose step 2 finds for the current , and let be any earlier recorded answer at a vertex comparable with . Then and are comparable and distinct, so applied to gives . This holds for every the search might find, so at every tag the recorded transcript is a legal play of by some Bob.

For every Alice's strategy defeats Bob in within finitely many declarations. During the run of our algorithm, for each , define as the first declaration for which Bob has no answer. That is, there is no witness for with . Therefore:

Lemma 5

for some machine .

We prove in Section 4, via a characterization of the stopping probabilities of randomized machines.

Fix with and let . Note that does not depend on . The term of the mixture () gives for all , and , so

Combining (2) and (3): . Since this is true for all , is proved.

Remark 6

The gap of is bounded in terms of , the following inequality holds: , where denotes the ordinary prefix complexity of an integer. The proof is in the . Whether this upper bound is sharp remains open.

4. Proof of Lemma 5: time semimeasures

Call a time semimeasure if for every .

Consider any randomized stopping machine . Along one input stream the events " halts consuming exactly " are mutually exclusive, so is a time semimeasure. Also is lower semicomputable by enumerating witnesses. The converse is also true:

Equivalence theorem (proved in the ). A function is a lower semicomputable time semimeasure if and only if for some randomized stopping machine . Moreover, can be computed from an index of an approximation of .

Proof of . By the equivalence theorem, it is enough to prove that is an l.s.c. time semimeasure. Indeed on a path extending , the masses are declarations of one strategy for , of total at most (), and a path extending no tag carries no mass. Therefore is an l.s.c. time semimeasure, thus for some machine . ∎

5. Proof of Theorem 4: Alice wins

We introduce an auxiliary palette game and construct Alice's winning strategy for . After that we translate game into , thus proving that Alice wins .

Informal (palette game )

The same game as , except that Bob answers with exact size cells, and Bob uses separate unit intervals, where takes the role of the discount factor . We introduce because it is easier to attack by induction on .

The palette game (). Bob is given disjoint copies of the unit interval (palettes). Alice's declarations are as in , with the same path budget (1). Bob answers with a cell , , , and cells answered at distinct comparable vertices must be disjoint. Alice wins as before.

Note the exact weight: since , Bob's answer occupies measure exactly in , corresponding to exactly in (not at least ).

Informal (Lemma 7)

Alice beats Bob in however many palettes Bob owns. She keeps a fraction of her budget unspent on every path, which is a slack that the induction step on needs.

Lemma 7

(Palette elimination.) For every there is a computable strategy for Alice in that defeats Bob, with all path loads at most , where .

We formally derive from in the end of this section. For now we provide a short informal proof. After that we prove by induction.

Informal (proof of Theorem 4 from Lemma 7)

Lemma 7 says that Alice wins (we use ), Theorem 4 says that Alice wins .

We want to translate all moves of both players from to , and use Alice's winning strategy in . Alice's declarations are the same in both games, so no translation needed. Bob's legal -answer is with . We pad it with zeros to length exactly . Geometrically, is a dyadic interval of length at least , and zero-padding trims it to its leftmost subinterval of length exactly , which can only make disjointness easier for Bob to satisfy.

An interval of length lies inside exactly one of the blocks , . We rescale each block to a unit interval to get the palettes of . So the first bits of the padded string name the block (the palette index) and the remaining bits are the address inside it.

So is with the unit interval cut into pieces and Bob's answers trimmed to exact size.

Let us prove by induction on , constructing strategies all of whose declarations have less or equal (so all Bob's answers are cells of depth at most ), and with all path loads at most .

Base . Declare . There is no palette, hence no answer; and .

Step. Let be the strategy for palettes, with exponents at most and load bound . We construct Alice's winning strategy . Fix

Depth- cells are called coarse, so each palette contains coarse cells, and there are total coarse cells in all palettes. Depth- cells are called fine, so each coarse cell contains fine cells.

Phase 1 shows how Alice could make a situation where she used only weight along some path, and Bob's answers along this path touch N distinct coarse cells of total measure 1 (one palette's worth of weight), which cannot be used in Phase 2. Precisely, Phase 1 constructs a vertex of the form , such that

• it consists of blocks, each block is several 's and a single at the end of the block,
• the declarations of Alice on this prefix are only on last zeros before ones (bold),
• each of Alice's declarations has weight , with the total weight of all declarations ,
• Bob's answers to these declarations belong to different coarse cells, whose total measure is .

Phase 2 shows that the space left to Bob is isomorphic to intact palettes, and runs on the descendants of the vertex constructed in Phase 1.

Phase 1: forcing markers into distinct coarse cells

Informal (Phase 1)

Suppose Alice has declarations (markers), each of weight , and Bob's answers are in different coarse cells (marked cells). Alice makes enough new declarations each of weight such that Bob's answers can not fit in marked coarse cells, so for some declaration Bob places his answer in a new coarse cell. Alice names this declaration the th marker. The construction allows to drop all non-marker declarations, which we used to overfill Bob's coarse cells. Alice repeats this until she has markers.

Alice keeps an active vertex and weight- declarations (markers) at ancestors of , answered in distinct coarse cells (marked cells). Alice starts from , . Given , set and let

a chain below listed deepest first. Alice declares in this order, stopping at the first whose answer lies in a coarse cell different from the marked ones. Such exists (else Bob already failed and Alice has won): the chain vertices are pairwise comparable and comparable with all markers, so if all answers stayed inside the marked coarse cells, those cells would contain pairwise disjoint fine cells, but coarse cells contain only fine cells.

Alice retains as the -st marker and sets . Note that all declared for lie at or below the -child of , while all future play will happen below the -child. Thus all for are incomparable with everything Alice will ever declare again (this is the point of the deepest-first order), while the marker at , an ancestor of , stays comparable with all future declarations and keeps constraining Bob.

Repeat this procedure for all .

Path weights. For each the construction above has at most declarations of weight on each path. For maximal the maximal weight on a path is at most

thus Alice's declarations are legal. A path through carries only markers, total load .

Phase 2: repacking the clean cells and induction step

Informal (Phase 2)

Below Alice wants to play . Bob can answer only by cells which are coarse or larger, since coarseness was defined using the exponent bound . Marked coarse cells can not be used. The total measure of unmarked coarse cells is exactly , but they are spread across palettes. It gives no advantage to Bob, that is he will play at most as well as with palettes without marked cells ( and translation map ). Thus Alice can run the inductive strategy and win.

A cell of depth is clean if it contains no marked coarse cell.

Lemma 8

Every legal answer of depth to a declaration at a descendant of is clean.

Proof

Such a declaration is comparable with every marker vertex, so its answer must be disjoint from all fine answers to the markers. Suppose met a marked coarse cell . A cell of depth meets a depth- cell only by containing it, so . But contains Bob's fine answer, so also contains this answer, contradicting disjointness. ∎

Exactly coarse cells are unmarked. Let be the set of maximal clean cells (clean with unclean parent, palette roots having depth ). Within each palette is an antichain, and the depth- cells below are exactly the unmarked coarse cells, hence

that is the same total measure as palettes. The clean region is ragged while expects intact palettes. The next lemma and translation map fix it.

Informal (Lemma 9 and translation map )

Sort the maximal clean cells from largest to smallest and lay them left to right into fresh unit intervals. Dyadic sizes in nonincreasing order guarantee that every maximal clean cell will be mapped to a cell of one of these fresh unit intervals.

Lemma 9

(Repacking.) Take fresh palettes: new copies of the unit interval, unrelated to Bob's palettes. There are pairwise disjoint cells () of fresh palettes with .

Proof

Identify the palettes with and process by nondecreasing depth (ties broken by palette index, then lexicographically), allocating consecutive intervals of lengths left to right. When a length- interval is placed, all earlier lengths are multiples of , so its left endpoint is one too. Thus the interval cannot cross an integer, since integers are multiples of as well. By (5) the intervals tile exactly . ∎

Let () be the cells produced by the proof of ; we call the repacked copy of . We now define a translation map from clean cells to cells of fresh palettes, under which the clean region left to Bob maps to intact palettes. Every clean has a unique maximal clean ancestor . If then . Writing , set

the cell at the same relative address below the repacked copy of . Then preserves depth, and preserves comparability and disjointness in both directions.

Induction step. Alice plays translated by , feeding of Bob's answers (clean of depth by and the exponent bound ) to a virtual -palette game. By the properties of , legal real plays become legal virtual plays, so reaches a declaration with no legal virtual answer. A legal real answer would be clean and would -map to a legal virtual one, so none exists and Alice wins .

Loads. Paths in Phase 1 which do not go through obey (4), so their load is at most

Paths through carry the marker weight plus a path load of , in total at most

Hence all path loads are at most .

The strategy uses declarations with at most , is finite by construction, and is computable uniformly in .

It remains to derive from : Alice's win in the palette game yields her win in the game (an informal version of this proof is given above, after the statement of ).

Proof of Theorem 4 (from Lemma 7)

Set . Alice wins via translating it to : she runs her -strategy, copies her declarations from into (declarations have the same format and the same budget (1) in both games), and translates Bob's answers into their shadows in , defined as follows. Given a legal -answer to , extend it by zeros to of length exactly (possible since ) and split , , . The shadow of is cell in palette , of depth exactly as requires. Note that zero-padding preserves incomparability, since incomparable strings disagree at a position within both lengths and padding changes no bit there. Also padded strings , are incomparable iff (a disagreement within the first bits) or and .

Thus shadows of legal Bob's -answers at distinct comparable vertices are legal in : if in , then the padded strings are incomparable, so the shadows in lie in different palettes or are disjoint cells in the same palette. So Alice's -strategy applies to the shadow translation of and eventually makes a declaration with no legal Bob's answer in . Bob then has no legal answer in either: the shadow of such an answer would be a legal answer in , which does not exist. So Alice wins . ∎

The construction belongs to the family of gap theorems initiated by Gács and Day , with a game-theoretic method in the spirit of Vereshchagin .

Appendix

Time semimeasures and randomized stopping machines

Recall from Section 4 that a time semimeasure is a function with for every . It is lower semicomputable (l.s.c.) if there is a computable , nondecreasing in the second argument, with for all . We normalize and assume that at each step the approximation increases at one string only, by a dyadic amount. This is no loss of generality: replacing by the largest multiple of not exceeding it keeps computable and nondecreasing in with the same supremum , and a step at which several strings increase can be split into several steps.

Equivalence theorem. A function is a lower semicomputable time semimeasure if and only if for some randomized stopping machine . Moreover, can be computed from an index of the approximation .

Proof, machines to semimeasures

Fix a machine . The witness property is semidecidable: run feeding it and , and watch whether it halts having consumed exactly . Enumerating witnesses by dovetailing lower semicomputes , uniformly in . For the path bound, fix an input and a random tape : the single deterministic run of on halts at most once, so the events " halts consuming exactly " are pairwise disjoint over , thus .

Proof, semimeasures to machines: allocating the seeds

Given , we first construct, uniformly effectively, sets such that

Cells are read as dyadic subintervals of , as in the Notation section, so every set below is a finite union of half-open dyadic intervals at each finite stage. Process the increments of one at a time. For each vertex define the ancestor and descendant allocations and , and maintain the invariant: is an initial segment of in the linear order inherited from .

The invariant implies that and are initial segments of one common ordered set , hence nested, so . Unfolding this recursion from the deepest occupied vertices, and using that the sets over a chain of vertices are pairwise disjoint by (6), we get

Suppose the next increment is a dyadic at the string : allocate to the leftmost set of measure inside the available set . There is enough room: the increased approximation still obeys the path budget, so (7) gives ; and is an effectively computable finite union of cells, since all sets and lengths involved are dyadic. Disjointness (6) is preserved, since avoids the allocations at all vertices comparable with . The invariant is checked in four cases:

• at itself: grows by exactly the next available measure after its end, remaining an initial segment of ;
• at a strict descendant of : grows by and is unchanged; an initial segment stays initial in any subset containing it;
• at a strict ancestor of : grows by and is unchanged. Every vertex comparable with is comparable with , so . Hence a point of outside lies after (the old invariant) and, being available, after the leftmost as well. So has no gap and is initial;
• at a vertex incomparable with : nothing changes.

Passing to the increasing unions over all stages, each is an effectively open set of measure , uniformly in , and (6) survives.

Proof, semimeasures to machines: the machine

Define the machine : at current consumed input prefix , it enumerates — dovetailing, restarting from scratch at each new prefix, and requesting one further random bit per round — the cells of the two sets and , disjoint by (6). A certificate is an enumerated cell which is a prefix of the consumed random string . If a cell of is certified, halts; if a cell of is certified, it requests the next input bit; if neither event ever occurs, it reads random bits forever. Two certified cells would be comparable prefixes of with intersecting cylinders, so by disjointness at most one kind of certificate can ever fire at a given .

Fix a string , an input extending and a random tape . Suppose , i.e. some cell of is a prefix of . At every we have and, by (6), : no -certificate can fire (a certificate with a cell of would put ), while a -certificate eventually does — the cell of containing is eventually enumerated and eventually a prefix of the growing . So the machine walks to , where the roles swap: , no -certificate ever fires and some -certificate does, so the machine halts having consumed exactly the input . Conversely, halting at exhibits a certificate, so Hence the event " halts consuming exactly " is exactly , and . The construction is uniform in an index of . Note that may consume more random bits than the certified cell is long; only the halting events matter for , not the witness lengths. ∎

Remark (the deterministic case). For a machine that never requests random bits, is the indicator of , a computably enumerable antichain. Conversely, every c.e. antichain is realized deterministically: at consumed input prefix , enumerate until some member appears; if , halt, and otherwise request the next input bit and repeat (by the antichain property is then ruled out for good). So the deterministic stopping machines realize exactly the -valued l.s.c. time semimeasures, and randomization extends this class to all of them.

The upper bound

We prove : every satisfies , where is the ordinary prefix complexity of an integer. (Both sides are finite: some machine reads input bits and halts, so for every .)

For an integer , enumerate without repetitions the set ; this is effective, uniformly in , since is lower semicomputable. Every input path contains fewer than members of , because . Let us assign equal weights to the members of as they are enumerated. Since every path contains fewer than of them, every path's budget is less than . Feed these increments to the allocator of the previous subsection. All requests have the same dyadic weight, so every allocation is a single depth- cell: the available set is the complement of finitely many depth- cells, so its leftmost part of measure is its leftmost cell. Write for the cell allocated to .

This is an effective coloring of in colors under which comparable strings get different colors, their cells being disjoint by (6). So every color class is a computably enumerable antichain, uniformly in , and the deterministic procedure of the Remark above stops exactly at the members of , consuming no random bits. This coloring construction is due to the proof of Theorems10 and 18 from Vovk and Pavlovic.

One stopping machine now reads from its random tape a self-delimiting program computing (with respect to a fixed optimal prefix-free machine), then more bits giving , and runs the procedure for . Its witnesses at are exactly the strings (program for ) followed by , so gives, with one constant for all <