This adds a blank-tape nonhalting proof for the BB(6) holdout:

1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB

The machine increments a binary counter whose digits sit at variable gaps. At overflow, a finite tail either lets the counter wrap or triggers a long pause that rebuilds the gaps and may insert digits. The proof models the overflow's return with a four-rule token transducer, then proves closure of the tail's front-unit cycle.

Only four paths occur between normal-mode overflows. An interval invariant covers all four, whichever of the two permitted answers the tail supplies. The blank run reaches the invariant after 92,299 steps; positive progress then proves Lemma nonhalt : ~ halts tm c0.

The proof follows the sweep/carry/macro-step architecture of CounterClass3v2.v, Module TM1. Its transition table and lemmas are different. It imports only Individual62 from busycoq, plus standard Rocq libraries.

Validation: Freshly compiled with Coq 8.20.1 against unmodified busycoq BB6 at 9b1e92aead6c61d436495e6010e61eae32452879. A separate checker verifies the exact TM_from_str literal and blank configuration. Print Assumptions nonhalt is closed, and independent coqchk rechecking passes.

Write-up: https://github.com/DennisKoshta/busycoq/blob/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/spread-counter/README.md

AI assistance: the proof and original write-up were produced with the help of Claude (Anthropic), with independent review and submission preparation by GPT-6 Astra (OpenAI).

Downloads: write-ups ZIP · images ZIP.