I've opened a PR proving that this machine never halts from blank tape:

```
1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF
```

https://github.com/ccz181078/busycoq/pull/29

This is another starting state of the SOBCv10 table, after reflecting the tape and renaming the states. It builds binary counters, with each overflow launching a much larger counting task. A short tail drives it through three returning exceptional rounds; the next round triggers nested overflows and eventually escapes into a repeating motion: 919 steps, shifted three cells left, forever.

The proof connects the blank-tape opening all the way to that final cycle. It tracks signed counter digits and a finite allowance of safe transformations for each ordinary column, enough to cover the three returning rounds.

The full informal write-up is in the PR description. The Rocq proof passed three checks against unmodified busycoq, including completed coqchk kernel replays. I'd appreciate any review or feedback!

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