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

`1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---` halts

Machine: 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---, a BB(6) holdout (line 700 of the 740-machine list, line 738 of the 778 list). Viewer: https://bbchallenge.org/1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---
Class: "Shift-overflow bouncer counter".
Result: Lemma halt: halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9), importing Individual62, BinaryCounter_v2, NatMod, SimplTape, Longitudinal and Eqb. Print Assumptions halt lists only functional_extensionality_dep.
Check time: it compiles in 25.6 s with -native-compiler yes, and coqchk re-checks it, the computed chain included, in 43.3 s (check_kill.txt).
Halting time: informally estimated on the scale of a power tower of height about 195. Neither computed nor proved; the .v proves halting, not a step count.
Equivalent machines: busycoq's verify/Eqv_v3.v (TM636, TM637) proves 1RB0RE_0LB1RC_1LD1RA_1LA0LE_0RC0RF_0LC--- and 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LB--- equivalent to this machine, so they halt too.

Mechanism

Counter and register. Left of the head is a binary counter in the words W0 = 001 and W1 = 111 (W1 W0 = digit 0, W1 W1 = digit 1, a lone W0 a separator). Right of the head is the register 1 (011)^n 01. Each increment is one bounce and adds one 011.
Shift-overflow. When the counter is full after c increments, the overflow re-reads it shifted by one word, and the register becomes (c−1)/2 new zero digits. So c grows like 2 to the power of the previous c: cycle 2 already makes a block of 654,311,423 pairs.
The halt. From the blank tape the machine runs 194 cycles. In the 195th overflow, an increment inside the re-read carries off the far end of the counter, and 1,368 steps later F reads a 1.

How the proof works

Rules. TM3's rules (LInc_spec, LOv_spec, Incs, Ov, the lpow block lemmas) are proved again on this table with TM3's own scripts, after renaming the two head notations.
Abstract lists. Blocks W10 l / W11 l stand for (W1 W0)^(1+l+n) / (W1 W1)^(1+l+n) with a lower bound l. step_rec is one cycle on abstract lists, and step_rec_spec proves it sound.
The run. init reaches the first abstract configuration in 38,573 steps (solve_init). final_check_ok : final_check 192 = true (vm_compute) runs 192 cycles, the last Incs, and a checker on the final counter.
The halt. Doomed x says the overflow run from Lmp x halts for every right part. Two walk lemmas (19 and 12 steps, es) carry it through separators, pairs and blocks, from the 13-token far tail (far_halt, 1,368 steps, solve_halt).

Template

verify/SOBCv6.v, Module TM3 (1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD---, halts): the same table under ours A B C D E F = TM3 B C A E D F, no mirror, started in TM3's state B. - Kept: the words, the counter, all rules, and the abstract-list checker (LInc_rec, LIncs_rec, LOv_rec, step_rec, P). - Changed: a new start; 192 abstract cycles instead of 2; lower bounds in the blocks, so an increment can stop inside a (W1 W0) block; a peel case in LOv_rec that splits the far pair off a block on demand (LOv_peel); a binary count bound saturating at 256; and a far-end halting predicate (Doomed, doom_rec) in place of TM3's short direct run near the head.

Files

1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v (the proof, 838 lines), proof.md (informal proof; its first table maps it to the .v), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).