1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB halts

This machine halts. Its computed step count, about 1.77 × 10^44, is not part of the formal proof (§9).

Watched at the moments when its head reaches new ground on the right, the machine is a binary counter. Each digit is a stretch of tape with one marker for its bit, possibly some extra walls, and a supply of fuel. Every carry that touches a digit flips its bit and burns some of its fuel.

Walls drift from digit to digit toward the head and refill digits that run low, and new digits are born at the right end. Measured against the fuel, the refills arrive sometimes earlier and sometimes later, and these swings grow. After about 1.16 × 10^22 increments, a digit with no spare wall has bit 0 and no fuel left, and the next carry into it halts the machine.

The proof is a computation checked in Coq. Each kind of carry step is a general lemma about the machine, long stretches of increments are applied in closed form, and a checker replays the whole run from step 342 to the halting carry in 107,781 checked moves.

Machine and status

• Machine: 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB, viewer https://bbchallenge.org/1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB
• Holdout: on the BB(6) holdout list, class "Skelet 1-like Class 2".
• Statement: Lemma halt: halts tm c0. with tm the TM_from_str of this string.
• Status: formalized in the accompanying verify/Skelet1LikeC2Halt_1RB0RD_1LC0RA.v (1,142 lines). It compiles in Coq 8.20.1 against unmodified busycoq (commit 0940bb9) in about 70 s with -native-compiler yes. coqchk re-checks it, the computed run included, in about 535 s.
• Print Assumptions halt: functional_extensionality_dep only. It comes from the framework lemma flip_halts_iff.
• Template: busycoq verify/Sk1Machines.v, Module TM91 (a halting Skelet 1 machine) and Module Sk1Auto: a certificate checker iterated with Eqb.N_iter_until and proved sound once.
• Framework pieces used:
• the call predicates segRR, segLL, segRL, segRLs, sideRL of verify/Individual.v, as instantiated in verify/Individual62.v;
• the tactics solve_seg, es, solve_init, solve_halt of verify/Individual62.v;
• sideRLs_halt of verify/LongitudinalHalt.v, flip_halts_iff of verify/Flip.v and N_iter_until_spec of verify/Eqb.v.
• Step count: 176,522,930,997,643,289,094,015,905,898,381,767,890,130,463 steps, the halting step included. This count is computed (§9); the .v proves only that the machine halts.

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 each right record (§2) the tape reads as walls and gaps. The 11-walls cut it into units, and each unit is a binary digit whose lead wall, 00 or 1111, is its bit.
• One increment is one carry from the right (§3). It passes the digits with bit 1 and stops at the first digit with bit 0. In every touch the digit's passive walls move two cells to the right and the right end of its lead one cell, so its fuel shrinks.
• Between structural events (glue, unglue, resets, edge events) all changes are linear in the number of touches, so long runs of increments are applied in closed form (§4).
• From step 342 the run reaches a digit with a single marker, bit 0 and no fuel (§5, §6). The next carry into it halts the machine (§7).

1. When the machine can halt

The transition table:

      0     1
A   1RB   0RD
B   1LC   0RA
C   ---   1RD
D   1RA   1LE
E   1RC   0LF
F   1LE   0LB

The only halting transition is C reading 0. State C is entered only by B0 (1LC) and by E0 (1RC).

• E is entered by D1 and F0. Both write 1 and move left. If E then reads 0, it moves right onto the 1 just written, so C reads 1.
• B is entered by A0 and F1. After A0 (write 1, move right), B0 moves left onto the 1 that A wrote, so C reads 1.
• After F1 (write 0, move left), B0 moves left once more, so C reads the second cell to the left of F's cell.

So the machine halts exactly when the head is in F on a 1 whose two left neighbours are 0 0:

0 0 1      with F on the 1

2. The wall view

Records and increments

A right record is a configuration in which the head is in state A on a blank cell and every cell to its right is blank. An increment is the run from one right record to the next one. All of the analysis looks at the tape at right records.

Walls and gaps

Read the tape to the left of the head.

• A wall is a maximal run of at least two equal symbols: 00, 11, 1111, 1^7, and so on.
• A gap is the number of cells between two neighbouring walls. Those cells alternate, so a gap is fixed by its length.

A gap between two 1-walls is odd, and a gap between a 1-wall and 00 is even.

The 1-walls are sorted by their length modulo 3:

The tape at a right record

At every right record of the run the tape has this form:

0^∞  E  U_0  b_1  U_1  b_2  …  b_n  U_n  b_T  [t]  A>

• E is the edge, b_1, …, b_n and b_T are boundaries, and [t] is the tail, an odd gap of t cells between b_T and the head.
• During a reset there is, for one increment, no tail: the tape ends with U_n at the head (§3.5).
• Each U_i with i ≥ 1 is a digit:

[x, M, m_1, Q_1, m_2, Q_2, …, Q_r, y]

• Here M is the lead, Q_1, …, Q_r are passive stacks, x is the gap between the left boundary and M, the m_i are the inner gaps, and y, the last gap, is the fuel.
• A digit with r = 0 is single-marker: [x, M, y]. A digit with r ≥ 1 is multi-marker.
• U_0 lies between the edge and b_1. It is a digit when e ≡ 1 (mod 3). When e ≡ 0 it is leadless, [x, Q_1, m_2, …, Q_r, y], or empty, [y].

The digits form a binary number with U_n, next to the tail, as its least significant digit.

The start: step 342

From the blank tape the machine reaches this right record after 342 steps:

0^∞ 111 0 1111111111 0 11111 01 00 101 A>

In the wall view:

E = 111,   U_0 = [1, 1^10, 1],   b_1 = 1^5,   U_1 = [2, 00, 3],   no tail

This is the middle of a reset (§3.5): there is no tail yet, and the next increment creates one.

3. The rules

An increment is one carry. It enters at the right end and moves left one unit at a time. Each unit it reaches is touched: it changes as below and either stops the carry or passes it on to the left.

3.1 Stop and pass

In every touch of a digit, all of its passive stacks move two cells to the right and the right end of its lead moves one cell to the right. The lead flips.

The fuel changes the same way in a stop and in a pass:

The inner gaps m_2, …, m_r do not change.

3.2 Glue

A multi-marker digit touched with y = 1 would get y = −1. Instead its last stack runs into the boundary on its right:

… m_r  1^(3j+1)  [1]  1^(3g+2) …    ->    … m_r  1^(3(g+j)+2) …

The digit loses its last stack Q_r = 1^(3j+1), and the boundary to its right now carries g + j glued walls.

The digit's new fuel is the gap that was left of the lost stack, as it stands after the touch: m_r if r ≥ 2 (the touch leaves it unchanged), and m_1 + 1 if r = 1 (the touch adds 1 to m_1).

3.3 Unglue

A digit with lead 1111 whose left boundary carries g ≥ 1 glued walls is not passed as in §3.1. The glued walls came from the left neighbour, and now they enter this digit:

1^5      [x, 1111, m_1, Q_1, …, y]   ->   11 [2, 00, x+1, 1111, m_1, Q_1, …, y−2]
1^(3g+2) [x, 1111, m_1, Q_1, …, y]   ->   11 [2, 00, 0, 1^(3g−2), x, 1111, m_1, Q_1, …, y−2]     (g ≥ 2)

• The first glued wall becomes the new lead. It has just been passed, so it is 00.
• For g ≥ 2 the other g − 1 glued walls follow as one stack.
• The old lead 1111 becomes a passive wall.
• The boundary is plain 11 again, and the carry goes on to the left.

For a single-marker digit the part m_1, Q_1, … is empty, so [x, 1111, y] becomes [2, 00, x+1, 1111, y−2]. As always, y − 2 = −1 means a glue instead (§3.2).

3.4 The unit next to the edge

An increment whose carry passes every digit U_1, …, U_n is an overflow; it touches U_0.

Fossilization. The old edge becomes a passive stack, the old lead becomes a passive wall, and a new edge 111 starts at the left end:

1^e [x, 1111, m_1, Q_1, …, y]   ->   111 [1, 1^e, x, 1111, m_1, Q_1, …, y−2]        (e ≡ 1 mod 3)

U_0 is then leadless and the edge is ≡ 0 again. The stacks left behind by the fossilizations form the far left part of the tape.

3.5 Tail and resets

Every increment adds 2 to the tail: t becomes t + 2.

A reset takes two increments. It starts when the least significant digit has glued its last stack onto the tail boundary, so that b_T = 1^5:

… 1^5 [t] A>          ->   … 11 [2, 00, t+2] A>                   (first increment)
… b [2, 00, y] A>     ->   … b [1, 1111, y−2] 11 [1] A>           (second increment)

• In the first increment the old tail becomes the fuel of a new least significant digit. Its lead is the glued wall, already passed, so the carry goes on into the digits to the left.
• In the second increment the new digit stops the carry at once, and a new tail [1] appears.
• The boundary b left of the new digit is 11, unless the carry of the first increment glued walls onto it.

The configuration at step 342 is the state between the two increments of a reset, with b = 1^5.

3.6 The halt

A carry that touches a single-marker digit [x, 00, 0] halts the machine. There the tape reads

… 00 11 …

the lead 00 followed at once by the digit's right boundary. By §1 this is the halting pattern: the head reaches the left 1 of 11 in state F, with 0 0 to its left.

3.7 What the rules exclude

No rule covers these shapes:

• a stop with x = 0;
• a tail boundary with two or more glued walls;
• an absorption when there is no digit left to become U_0;
• the halting shape [x, 00, 0] in U_0.

If the run ever reached such a shape, the checker of §8 would stall and never report the halt. It does report it, so these shapes never occur on the run.

The edge class always matches U_0: an absorption leaves a U_0 digit with e ≡ 1, a fossilization leaves a leadless U_0 with e ≡ 0, and edge growth keeps e mod 3.

4. Batching

Touch counts

Call the least significant digit depth 0, its left neighbour depth 1, and so on. A digit at depth q is touched by a carry exactly when the q digits to its right all have bit 1.

So the touches follow binary counting. If the q digits to the right of a digit form the number C < 2^q, then in d increments that digit is touched

floor((C + d) / 2^q)

times, as long as no structural event (glue, unglue, reset, absorption, fossilization, halt) happens.

The .v counts the same way, digit by digit. A digit with bit b that is touched n times passes on

p = floor((n + b) / 2)

carries to its left neighbour, which is therefore touched p times.

Closed forms

Take a digit touched n times without a structural event. Its bit flips at every touch, and its touches are p passes and s = n − p stops. The rules of §3.1 add up to:

For U_0 with an edge ≡ 0, m overflows give: e grows by 3m, and the last gap (y of a leadless U_0, or the gap of an empty one) shrinks by 2m.

When a batch is allowed

A batch of d increments applies these closed forms to every unit at once. It is used only when the closed forms are exact, that is, when for every touched unit:

• no glue happens: a multi-marker y stays ≥ 1, and so does the last gap of U_0;
• no unglue happens: a digit that gets a pass has a plain 11 on its left;
• a single-marker digit keeps y ≥ 0, and is never touched with lead 00 and y = 0;
• a digit whose first touch is a stop has x ≥ 2;
• U_0, if it is touched, is leadless or empty (edge ≡ 0);
• the tail boundary is 11 (no reset is under way).

These are exactly the guards of closedU and closedZ in the .v. Under them closedU_spec, closedZ_spec and batchL_spec prove that the batch equals d single increments.

Choosing d

A batch size d is proposed by a function propose. It finds, for each unit, the first increment at which that unit would meet a structural event, using the touch count formula above, and takes one less than the earliest.

propose is untrusted: whatever d it returns, the guards above are checked. If a guard fails, or d = 0, the checker does one exact increment instead.

5. The run

From the step-342 configuration the checker repeats one move, next: a batch if one is allowed, otherwise one exact increment by the rules of §3.

• The 107,781st move is the halting touch.
• The halt happens during increment 11,631,266,794,472,450,654,093, counted from the step-342 configuration. The .v does not count increments: this number adds up the increments of the same 107,781 moves, computed outside Coq.
• About half of the moves are batches. The others are single increments, at the structural events.
• The run passes 82 resets.

When the counter runs dry, the tape holds the edge 1^998730056409855, a leadless U_0 with 1,302 passive walls and stacks (the fossils), and 22 digits. Its right end, three increments before the halt, is shown in §7.

6. Why the run reaches a fuel-out

The proof does not need this section: the checker simply runs. It explains why a halt is reached at all.

Only single-marker digits can halt

The halt rule (§3.6) needs a single-marker digit. A multi-marker digit never halts: when its fuel runs out it glues its last stack onto the boundary to its right instead (§3.2). That stack then enters the right neighbour at its next pass (§3.3).

So walls flow to the right, from digit to digit, toward the head. A single-marker digit loses one fuel cell per touch and survives only if walls arrive from its left neighbour before its fuel is gone.

The race at the right end

At reset n a new least significant digit is born:

[1, 1111, 2 a_n − 1]

Its fuel 2a_n − 1 is the old tail. It is touched at every increment, so it lasts about 2a_n increments unless walls reach it. The next reset comes a_{n+1} + 1 increments later.

Roughly, the counter survives as long as each time between resets stays below twice the one before, a_{n+1} < 2 a_n. The ratio a_{n+1}/a_n oscillates, and its swings grow:

The peaks at resets 45 and 62 are 17 resets apart, and the troughs at resets 53 and 75 are 22 apart. Over the same stretch the number of digits grows slowly.

The third swing crosses 2

After reset 82 the next reset would need about 2 a_82 increments. It never comes. The digit at depth 1 runs low on fuel, and its left neighbour is single-marker, so it has no wall to hand on.

The configuration three increments before the halt (§7) comes 5,712,816,071,814,019,770,034 increments after reset 82.

7. The halt

Increments are counted from the step-342 configuration, and …090 stands for increment 11,631,266,794,472,450,654,090.

After increment …090, three increments before the halt, the right end of the tape is (U_22 is the least significant digit):

… 11 [1495536819214692213317, 1111, 4812803520428781749]       U_20
  11 [2901296570081134732223, 1111, 1]                         U_21
  11 [5712816071814019770035, 1111, 3]                         U_22
  11 [11425632143628039540069] A>                               tail

Digits U_20, U_21 and U_22 are single-marker and all have bit 1.

Increment …091. The carry passes U_22, U_21, U_20, and further digits with bit 1, and stops at U_17. U_21 is passed with fuel 1:

11 [2901296570081134732226, 00, 0]                             U_21
11 [5712816071814019770038, 00, 2]                             U_22

Increment …092. The carry stops at U_22:

11 [5712816071814019770037, 1111, 1]                           U_22

Increment …093, number 11,631,266,794,472,450,654,093 after step 342. The carry passes U_22, whose fuel becomes 0, and touches U_21 = [2901296570081134732226, 00, 0]. That is the halt of §3.6.

8. How the .v states it

8.1 The mirror and the words

The .v works in the mirrored machine tmf = flip tm, where the counter lies to the right of the head. flip_halts_iff turns halts tmf c0 into halts tm c0.

Words are lists of cells, written starting next to the head. In the original orientation they read from right to left:

A unit is

uw bs b a x far  =  cw bs ++ leadw b a x ++ far

the passive stacks first (the one next to the fuel first), then the lead, then the far boundary. For a single-marker digit, bs is empty and the lead's first gap is the fuel.

The two kinds of configuration at a record are below. In both the head is in state A on a blank cell with only blanks on its far side, next to the word.

root t X  =  0^∞ <A (01)^t 0 11 X                tail [2t+1]
NT s g X  =  0^∞ <A (10)^s 1 00 10 1^(3g+2) X    no tail: the digit [2, 00, 2s+1]

8.2 One shift for every touch

In the mirror every touch removes the first two cells of the unit's word, [0;1], the two nearest the head: all passive walls move two cells toward the head. consume says what that does to the stack list:

consume ((c+1, j) :: r) a  =  (0, (c, j) :: r, a)      the fuel gap shrinks by 2
consume ((0, j) :: r)   a  =  (j, r, a)                glue: j walls go to the boundary nearer the head
consume []          (a+1)  =  (0, [], a)               single-marker: the fuel shrinks
consume []              0  =  none                     single-marker without fuel

With it each rule of §3 is one lemma:

Each lemma is proved from short fixed-word lemmas and generic composition:

• the fixed-word cores are proved by solve_seg or es;
• a run of passive stacks is crossed by blkRR_F and blkLL, lifted to whole lists by induction (chainRR, chainLL);
• gen_RL, gen_fwd and gen_side, with their glue variants, put a core word behind any such run of stacks.

8.3 Records and one increment

A configuration is stored as a record with binary numbers:

• unitN: the stack list, the bit, the parameters a and x, and the far boundary's g;
• zN: U_0, either Z0 (edge ≡ 0, leadless or empty) or ZD (edge ≡ 1, a digit);
• tailN: TT t g (a tail with tail boundary tailw g) or NTl s g (no tail);
• cfg, and denote, which maps a record to a tape.

One increment on records is computed by touchN (a digit), ztouch (U_0), callN (the carry through the list) and inc1 (the tail and resets).

• inc1_ok: if inc1 c returns c', then denote c -->* denote c'.
• inc1_halt: if inc1 c reports the halt, then halts tmf (denote c).

8.4 Batches and the checker

• pairK and pair1 do 2q touches of one digit (q stops and q passes) by induction on q. clK0, clK1, cl10 and cl11 add the odd last touch and the start from bit 1.
• closedU_spec turns these into the closed forms of §4 on records, and closedZ_spec does the same for U_0.
• batchL_spec chains the units: n touches of the first one forward p calls to the next.
• batch_step asks propose for d and applies batchL; batch_step_spec proves the result.
• next is a batch if batch_step succeeds, else inc1. When inc1 fails, next stays at the same configuration, which is trivially sound. next_spec covers all three cases.

8.5 The run

run T c iterates next at most T times with N_iter_until.

Its two soundness lemmas, run_ok and run_halt, follow from N_iter_until_spec and next_spec.

The run is cut into pieces of 5,000 moves: 21 full pieces, and a 22nd that reaches the halt at its 2,781st move.

k_i  :=  the configuration after 5,000 moves from k_{i−1}       (k_0 = c342; Eval vm_compute)
s_i  :   run 5000 k_{i−1} = inl k_i                              (i = 1 … 21)
s22  :   run 5000 k21 = inr tt                                   (the halt)

Each s_i is proved by vm_cast_no_check (eq_refl _). The kernel checks it when the lemma is closed, and coqchk checks it again. The k_i are plain definitions, and the s_i certify them, so their values need no trust.

The final chain:

• init: the blank tape reaches denote c342 in 342 steps of tmf (solve_init);
• halt_tmf: init, then run_ok over s1 … s21, then run_halt on s22;
• halt: flip_halts_iff applied to halt_tmf.

8.6 What is trusted

Only the framework and the kernel. propose only chooses d, and every batch it proposes is checked by the guards of closedU and closedZ. The final theorem uses no custom notation, and Print Assumptions halt lists only functional_extensionality_dep.

9. Step count (computed, not proved)

Adding up per-rule step costs over the same run, the machine halts after

N = 176,522,930,997,643,289,094,015,905,898,381,767,890,130,463  ≈ 1.765 × 10^44

steps, counting the halting step, from the blank tape. 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.

In the table, Σm is the sum of a unit's inner gaps, and Qc sums (14L − 8)/3 over the unit's passive walls 1^L (16 for a 1111). The costs are computed from the values before the touch.

Glue and absorption add no steps beyond these.

These costs are not derived in the .v. They agree with direct simulation on all 276,427 increments from step 342 to 10^11 steps. On every single-stepped increment of the run they were also checked on smaller tapes of the same shape. A batch sums them in closed form.

For scale, summing only the two sweeps of the tail, 2t per increment, already gives more than 8.7 × 10^43 steps.

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