1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC--- halts

This machine halts after 1,816,824,067,232,869,945 ≈ 1.82 × 10^18 steps. The count is computed (§10); the formal proof shows only that the machine halts.

Left of the head the tape holds a counter, written in digits of three cells. Right of the head is a long "bell": a run of three-cell blocks with one defect in it. In each round the head adds 1 to the counter and then moves the defect one block to the left.

When the defect reaches the counter, the bell eats a few cells off the low end of the counter, and the defect starts again near the far end of the bell. That is one cycle. The cells left in the counter are then grouped into digits differently, and this can make digit shapes that ordinary counting never produces.

In cycle 611,577 one of these shapes, 111, sits directly below a digit whose last cell is 1. Two carries reach it. The first turns it into 110, and at the second the machine reads a 1 in state F, its only undefined transition.

The proof is a computation checked in Coq. Rounds whose carry stays inside ordinary digits are general lemmas, applied many at a time in closed form. Eats and all other rounds are run by a verified run-length simulator of the machine. A checker replays the whole run from step 288 in 4,942,483 checked moves.

Machine and status

• Machine: 1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---, viewer https://bbchallenge.org/1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---
• Holdout: line 29 of the 740-machine BB(6) holdout list, class "Bell eats counter".
• Statement: Lemma halt: halts tm c0. with tm := TM_from_str "1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---". The proof is for the string itself, with no mirror and no renaming.
• Status: formalized in the accompanying .v (2,976 lines).
• It compiles in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9) in about 610 s with -native-compiler yes.
• The 751 computed chunks are closed by vm_check_eq of verify/Helper.v (vm_cast_no_check of eq_refl). The kernel checks each of them with its virtual machine at Qed.
• coqchk does not finish on this file within 600 s, so the chunks are checked by coqc's kernel only.
• Print Assumptions halt: Closed under the global context.
• Template: busycoq verify/Sk1Machines.v, Module Sk1Auto: one step function iterated with Eqb.N_iter_until and proved sound once with N_iter_until_spec, where untrusted proposals are checked at each use.
• Kept: that architecture (here the step next, iterated by run, with run_ok and run_halt from N_iter_until_spec), and run-length configurations.
• New: this machine's rounds and digits (proved with es of verify/Individual62.v), and closed-form batches of rounds.
• New: a macro simulator whose block rules are found while it runs, by window simulation, and crossed with shift_rule_L / shift_rule_R of verify/Individual62.v. Sk1Auto instead takes a fixed list of validated scans.
• New: a parser for the round-start configuration, and the run cut into 751 chunks between literal states.
• Equivalent machines: busycoq's verify/Eqv_v2.v (TM291, TM392, TM1913) proves three machines equivalent to this one, and verify/Eqv_v3.v (TM558, TM605) proves two machines equivalent to its mirror image. So they halt too.
• Step count: 1,816,824,067,232,869,945, the halting step included. Computed, not proved (§10).

Where each part lives in the .v

A comment at the end of the .v restates the rules in the .v's own notation.

Summary

• At the start of every round the tape is a K-form (§2): a counter of three-cell digits, a boundary cell, and the bell 101 (001)^b 0001 (001)^c with its defect 0001 after b blocks.
• A round (§3) takes b to b − 1 and c to c + 1. It adds 1 to the counter, which on ordinary digits is +1 in balanced base 4 with digits −1, 0, 1, 2.
• At b = 0 the round becomes an eat (§4). The counter loses a few low cells, and the next K-form has b close to the old c. A cycle is one eat followed by its rounds.
• Long stretches of rounds are applied at once in closed form (§5). Eats and rounds whose carry reaches an unusual digit are simulated by a verified run-length simulator (§6).
• A checker (§7) replays the run from step 288 to the halt, in 751 chunks.
• The halt (§8, §9) comes in cycle 611,577, from a digit 111 that two eats in a row produced by regrouping cells.

1. When the machine can halt

The transition table:

      0     1
A   1RB   0RE
B   1RC   0RA
C   0LD   0RB
D   1LA   0LE
E   1LC   1LF
F   0LC   ---

The only halting transition is F reading 1. State F is entered only by E1 = 1LF, which writes 1 and moves left. So the machine halts exactly when E reads a 1 whose left neighbour is also 1:

1 1      with E on the right 1

2. Notation

Tapes

Configurations are written left to right, with 0^∞ for the blank part of the tape. A state letter followed by > stands for the head, in that state, on the cell just right of the mark. A word in parentheses with an exponent is repeated, so (001)^b is b copies of 001.

Digits

The counter is read in digits of three cells. A digit is written x m y (its three cells from left to right), and the lowest digit is the one next to the head.

A digit is clean when its middle cell m is 0. Clean digits have values in balanced base 4:

So a clean digit x 0 y has value 2x − y. A blank digit is 000, so the counter can grow upward for free.

A word w of clean digits has the value Σ e_i 4^i, where e_0 is the lowest digit. A digit with m = 1 (010, 011, 110, 111) is dirty.

K-forms

A K-form is the configuration

K(w, b, c)  =  0^∞ w 0 E> 101 (001)^b 0001 (001)^c 0^∞

• w is the counter, and the single 0 after it is the boundary.
• Right of the boundary is the bell: 101, then b blocks 001, then the defect 0001, then c more blocks 001.
• A cycle start is a K-form with b = 0:

K0(w, c)  =  K(w, 0, c)  =  0^∞ w 0 E> 101 0001 (001)^c 0^∞

From the blank tape the machine reaches K0('', 2) (an empty counter) after 288 steps.

In the .v, K X b c is X <* [0] {{E}}> bellw b c *> 0inf. There X is a busycoq side, so its cells are listed nearest the head first, and a digit x m y appears as [y; m; x]. For example, dcell Dm = [1;0;0] is the digit 001.

3. Rounds

A round goes from K(w, b, c) with b ≥ 1 to K(w', b − 1, c + 1). It has two parts: a call into the counter, then a trip over the bell.

3.1 The call and the bell part

At a K-form, E reads the first 1 of the bell and its left neighbour is the boundary 0. So E1 = 1LF leads to F reading 0, and F0 = 0LC enters the counter in state C on its lowest cell.

A call is the run from there until the head is back on the boundary in state B:

callw X X'  :  for every r,   X <{{C}} 0 >> r  -->*  X' {{B}}> 0 >> r

In busycoq's notation, X <{{C}} 0 >> r has the head in state C on the cell of X next to it, with the boundary 0 and then r to its right. The call holds for every right part r, so it never looks at the bell, and w' depends on w alone.

The bell part then walks right to the defect and back, and moves the defect one block to the left (bellpart, proved by es):

0^∞ w B> 0 101 (001)^(b+1) 0001 (001)^c 0^∞   -->+   K(w, b, c + 1)

It takes 12(b + 1) + 19 steps. Its rightmost cell is inside the defect, so the c blocks after the defect play no part.

Together they give round:

callw X X'   ->   K X (S b) c  -->+  K X' b (S c)

3.2 The carry on clean digits

On clean digits the call is a carry. It enters the lowest digit and either stops there or passes on to the next digit up.

So the call adds 1 in balanced base 4. inc computes this on a list of digits, and callw_inc proves it, by induction on the list, for any higher part H above the digits:

inc ds = Some ds'   ->   callw (cells ds *> H) (cells ds' *> H)

inc fails only when the carry would leave the list. A round on clean digits therefore costs

12b + 22 + 14t + 4[the digit that stops the carry is 000 or blank]

steps, where t is the number of 100 digits the carry passes.

These step counts, like the one in §3.1, are facts about the machine used only in §10. The lemmas state reachability, not step counts.

3.3 Dirty digits

The table above does not cover a carry into a dirty digit. The proof never needs to: such rounds are simulated (§6). Two cases explain the halt, and both follow from the transition table.

• Into 111. C reads y = 1, and C1 = 0RB turns it into 110 and stops the carry, as for 101.
• Into 110. C reads y = 0 and moves left; D reads m = 1 (D1 = 0LE); E reads x = 1 (E1 = 1LF); F reads the last cell y of the digit above. If that cell is 1, the machine halts (§1).

The other dirty digits, 010 and 011, are what eats usually create (§8). In the run, a carry into them turns them back into clean digits, often a whole run of them at once, with a large carry upward.

4. Eats and cycles

The eat

At b = 0 there is no block between 101 and the defect. The round then does not return to a K-form at once. The head makes a few long trips over the whole bell, and the boundary moves left into the counter: a few low cells of the counter are taken into the bell. The run ends at the next K-form

K0(w, c)   -->*   K(w', b', c')

with b' close to c and c' small. The proof does not need a rule for this. The checker runs every eat on the simulator of §6, at its true c (up to 1,218,828), until it reaches a K-form with b ≥ 1.

In half of the eats of the run, b' = c − 1 and c' = 2. Over all eats with c > 250, b' − c lies between −1 and 115 and c' between 2 and 13.

The cycle

A cycle is an eat followed by b' rounds:

K0(w, c)  -->*  K(w', b', c')  -->*  K0(w'', c' + b')

so the next cycle starts with c' + b' blocks after the defect. On average c grows by about 2 per cycle: it is 2 at cycle 0 and 1,218,828 at cycle 611,577.

The rounds of a cycle cost about 12b each for b = b', b' − 1, …, 1, about 6c² steps per cycle. This is where almost all of the 1.82 × 10^18 steps go.

5. Batches of rounds

Closed form

Many rounds in a row only add to the clean low part of the counter. rounds applies n of them at once. If ds and ds' are lists of clean digits of the same length, and val ds' = val ds + n, then for any higher part H

K (cells ds *> H) (n + b) c   -->*   K (cells ds' *> H) b (n + c)

The proof is an induction on n. Each step is one round_inc. The carry never leaves ds, because val_le_maxv bounds every value of a list of k digits by

maxv k  =  2 (4^k − 1) / 3

the value of k digits 100, and val_inj closes the case n = 0.

The batch step

batch uses this at a K-form K(w, b, c):

• split 16 w takes up to 16 clean digits D off the low end of w, stopping at the first dirty one. Past the end of w the blank tape gives 000 digits.
• propose suggests n = min(b, maxv |D| − val D), the number of increments before the carry would leave D.
• addn D n adds n digit by digit in balanced base 4, and fails if a carry would leave D. addn_spec gives the same length and val D' = val D + n.
• If n ≥ 1, n ≤ b and addn succeeds, batch_spec gives K(w, b, c) -->* K(w', b − n, c + n), where w' is w with D replaced by D'.

propose is untrusted: whatever n it returns, the other conditions are checked. When it returns 0, because the next carry would reach a dirty digit or go past 16 digits, the checker simulates one round instead (§7.1).

6. The macro simulator

6.1 Run-length sides

A side of the tape (sd, sdn) is a list of runs (u, n), a block u of cells repeated n times, followed by blanks.

• pop and push take or put one cell next to the head, and push merges equal blocks back into runs.
• pop3 takes a whole three-cell block, which is how the counter is read in digits.

6.2 Macro steps

A macro step (mstep) is either a block rule or a single step of the machine.

• Single step (single): one transition of tm. When the transition is undefined, the result is halts tm of the current configuration (halted_halts).
• Block rule (try_rule): the head faces a run u^n with n ≥ 2 and |u| ≥ 2.
• wsim simulates the head crossing one copy of u, with 0, 1 or 2 cells d already behind it (at most 64 steps).
• If the head leaves the window forward, in the same state, with d unchanged, then one copy obeys a rule d q> u -->* u' d q>.
• shift_rule_R (or shift_rule_L on the left) of verify/Individual62.v then crosses all n copies at once:

d q> u^n   -->*   u'^n d q>

Rules are found while the checker runs and are checked where they are used, so no list of rules is trusted. wsim_spec, try_k_spec, try_rule_spec and mstep_spec prove each part.

6.3 Running to the next K-form

isK recognises a K-form: state E, the boundary 0 behind the head, and ahead of it the bell of §2 followed by blanks. isK_spec proves that it returns the right (w, b, c).

urun bmin FUEL makes macro steps until isK finds a K-form with b ≥ bmin (it looks after every macro step), a halt, or 65,535 macro steps (FUEL). urun_spec proves the result. An eat is urun 1, and a simulated round is urun 0.

The block rules make the long trips cheap. The 611,578 eats of the run take 115,095,507 macro steps in all, about 190 per eat, although the late ones cross more than a million blocks several times.

7. The checker and the run

7.1 One move

A checker state krec is a triple (w, b, c) with w a run-length side, and kden maps it to K(w, b, c). One move, next, is:

A halt found by the simulator ends the run. If urun runs out of macro steps, next keeps the same state, which is trivially sound. next_spec covers every case:

next k = inl k'   ->   kden k  -->*  kden k'
next k = inr tt   ->   halts tm (kden k)

7.2 The run

run T k iterates next at most T times with N_iter_until. Its two soundness lemmas follow from next_spec by N_iter_until_spec:

run T k = inl k'   ->   kden k  -->*  kden k'          (run_ok)
run T k = inr tt   ->   halts tm (kden k)              (run_halt)

init proves by solve_init that the blank tape reaches kden k0 = K('', 0, 2) (at step 288, §2). From there the run is cut into 751 chunks of about 400,000 macro steps:

k_i   :=  a literal state                                  (i = 1 … 750)
s_i   :   run T_i k_{i−1} = inl k_i                        (i = 1 … 750)
s751  :   run 7514 k750 = inr tt                           (the halt)

Each s_i is proved by vm_check_eq. The k_i are written with mk, as a list of runs (block, count) and the numbers b and c. A block is a positive number whose binary digits, from the lowest bit, are its cells, with the top bit as a sentinel. The values of the k_i need no trust, since the s_i certify them.

The final chain is

• h750 : halts tm (kden k750), from run_halt on s751;
• h_i, from h_{i+1} and run_ok on s_{i+1} by halts_evstep, down to h0;
• halt, from h0 and init.

7.3 What the run contains

The 751 chunks hold 4,942,483 moves in all, the sum of the T_i. The last one is the halting round; each of the 4,942,482 moves before it returns a checker state (inl).

8. Why the halt comes so late

This section explains the run; the proof does not need it. Its counts are computed from the same run, outside Coq.

Eats regroup the counter

An eat removes d cells from the low end of the counter, most often 2, 5, 8 or 11. In 610,646 of the 611,445 eats with c > 250, d ≡ 2 (mod 3); the others are deep bites of 15 cells or more. Apart from a few cells near the new boundary when d = 2, the cells above the bite are unchanged.

The digits are counted from the low end. So when d ≡ 2 (mod 3), the remaining cells fall into new groups of three. Each new digit is the last two cells of one old digit, followed by the first cell of the old digit to its right:

old digits:   x1 m1 y1 | x2 m2 y2 | …
new digit:          m1 y1 x2

Which digits this makes

With d ≡ 2 (mod 3), regrouped clean old digits (m = 0) give new digits that start with 0: only 000, 001, 010 and 011. The carries of the next rounds turn the dirty ones back into clean digits.

A dangerous digit 110 or 111 then needs an old digit with m = 1 and y = 1, that is 011 or 111. Such a digit must survive a whole cycle without a carry converting it, and then be regrouped by the next eat.

Even then, by §3.3 the new digit halts the machine only when the digit directly above it ends in 1, and only once the carries reach it. Counted over the run:

• right after the eat, a digit 110 or 111 appears in 369 of the 611,578 cycles, each time after a bite with d ≡ 2 (mod 3), and each of these cycles starts with a 011 or 111 digit in its counter;
• in 331 of the 369 it is the top digit (blank above), and in 37 the digit above ends in 0;
• only in cycle 611,577 does the digit above end in 1.

The last three cycles

The counters around the halt, highest digit first:

cycle 611,576 starts   001 011 100 001 100 101 101 000 001 000 001 001 000 000    c = 1,218,827
after its eat          010 111 000 011 001 011 010 000 010 000 010 010 001        b = 1,218,826, c = 2
cycle 611,577 starts   010 111 100 100 001 101 000 000 000 001 001 000 101        c = 1,218,828
after its eat          101 111 001 000 011 010 000 000                            b = 1,218,830, c = 3

• The 011, the second digit from the top, was made by the eat of cycle 611,575 and survived that cycle's rounds unconverted.
• The eat of cycle 611,576 removed 2 cells and regrouped the rest: the cells 1 1 of that 011 and the first cell 1 of the 100 after it became the digit 111.
• In cycle 611,576 no carry got past the third digit from the top, so the 111 survived.
• The eat of cycle 611,577 removed 14 cells (14 ≡ 2 mod 3) and regrouped again. The 111 came back as 111, from its own last two cells and the 1 that starts 100. Above it, the cells 1 0 of 010 and the 1 that starts 111 became 101, a digit ending in 1.

This bite was deep, so the counter is only 8 digits long, and the carries of the cycle reach the 111 early in the cycle.

9. The halt

The counter of cycle 611,577 at the start of four of its rounds:

round     1    101 111 001 000 011 010 000 000
round    12    101 111 001 100 001 001 001 001
round 3,340    101 110 001 001 001 001 001 001
round 7,435    101 110 100 100 100 100 100 100      b = 1,211,396, c = 7,437

• Rounds 1 to 11. Rounds 1 to 10 count in the two lowest digits. In round 11 the carry reaches the dirty 010, and that one round turns 000 011 010 100 100 into the clean 100 001 001 001 001.
• Rounds 12 to 3,339. The six low digits count up from value −597 at round 12 and reach 2,730, the largest value of six digits, at round 3,339. The carry of that round passes all six, leaves them as 001 001 001 001 001 001 (value −1,365) and reaches 111, which becomes 110 (§3.3).
• Round 7,435. After 4,095 more increments the six low digits are 100 each (value 2,730) again.

In round 7,435 the carry passes the six 100 digits and reaches 110. There C reads 0, D reads the middle 1, E reads the first 1, and F reads the last cell of 101 above it, which is 1:

… 1 0 1 | 1 1 0 | …
      ^   ^
      F   E

That is the halting transition F1, the 36th step of the round. The checker's last move is this round: urun 0 returns Halt, so run 7514 k750 = inr tt.

10. Step count (computed, not proved)

Adding up the steps of the same run, the machine halts after

N  =  1,816,824,067,232,869,945   ≈  1.82 × 10^18

steps from the blank tape, counting the halting step. In busycoq's convention (halts_in tm c0 n: n steps, then a halting configuration) this is n = N − 1. The .v does not prove this number.

The counts use these facts about the machine, each checked against direct simulation:

• a round on clean digits costs the formula of §3.2;
• a round whose carry reaches a dirty digit costs 12b plus a part that does not depend on b;
• an eat's cost is affine in c, and its result does not depend on c, for every eat of the run.

Direct simulation of the machine agrees with the count at every cycle start up to 3 × 10^10 steps (1,573 of them), on 14 whole cycles further out, and on the whole halting cycle. That cycle starts at step 1,816,823,958,776,312,687 and halts 108,456,557,258 steps later: an eat of 58,503,988 steps, 7,434 complete rounds, and the 36-step halting round.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).