/machines/1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---/submission/README.md · raw

`1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---` halts

Machine: 1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---, a BB(6) holdout (line 29 of the 740-machine list). Viewer: https://bbchallenge.org/1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---
Class: "Bell eats counter".
Result: Lemma halt: halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9), importing Individual62 and Eqb. Print Assumptions halt: Closed under the global context.
Check time: it compiles in about 610 s with -native-compiler yes. Its 751 computed chunks (vm_check_eq) are checked by the kernel at Qed; coqchk does not finish within 600 s.
Halting time: 1,816,824,067,232,869,945 ≈ 1.82 × 10^18 steps, the halting step included. Computed from per-round step costs over the same run (section 10 of the write-up); the .v proves halting, not the count.
Equivalent machines: verify/Eqv_v2.v (TM291, TM392, TM1913) and, through the mirror image, verify/Eqv_v3.v (TM558, TM605), so those five machines halt too.

Mechanism

At each round start the tape is 0^∞ w 0 E> 101 (001)^b 0001 (001)^c 0^∞: a counter w of three-cell digits (001 000 101 100 = −1 0 1 2, balanced base 4), and a bell whose defect 0001 sits after b blocks.
A round adds 1 to the counter and moves the defect one block left. At b = 0 the bell eats a few low cells of the counter, and the next round start has b close to c: a new cycle.
An eat usually bites 2 (mod 3) cells, so the cells left in the counter are regrouped into new digits. In cycle 611,577 this leaves a digit 111 under a digit ending in 1. One carry turns it into 110, and the next one makes F read a 1.

How the proof works

Rules. The round (bellpart, round) and the carry on clean digits (absm, abs0, abs1, pass2, callw_inc) are general lemmas: short runs proved with es, and callw_inc by induction on the digits. rounds applies n rounds at once in closed form.
Simulator. Eats and rounds whose carry reaches a dirty digit run on a verified run-length macro simulator: single steps, plus block rules found by window simulation and crossed with shift_rule_L / shift_rule_R.
The run. init (solve_init) proves that the blank tape reaches the first cycle start, which the machine does at step 288. The checker next (eat, batch with an untrusted propose, or one simulated round) is iterated by N_iter_until: 4,942,483 moves in 751 chunks s1 … s751, the last of which reports the halt.

Template

verify/Sk1Machines.v, Module Sk1Auto: one checker step iterated by Eqb.N_iter_until and proved sound once with N_iter_until_spec, with untrusted proposals checked at each use. - Kept: that architecture and run-length configurations. - Changed: this machine's rounds and digits, closed-form batches of rounds, block rules found while the simulator runs instead of a fixed list of scans, and a parser for the round-start configuration.

Files

1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---.v (the proof, 2,976 lines), proof.md (informal proof; its first table maps it to the .v), check_kill.txt (the full output of the automated checks).