This adds blank-tape nonhalting proofs for two BB(6) holdouts:

• 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---
• 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA

They are different start states of the same transition table, up to state renaming. A binary counter drives a moving front through a row of blocks. Each cycle doubles the counter range; the scaled block counts follow two affine branches, both preserving the same six-facet hexagon. The proof covers counter overflow during conversion, including the case where the next front starts before the current conversion finishes.

The two blank-start runs enter that invariant after 17,215 and 16,590 steps. Each file proves Lemma nonhalt : ~ halts tm c0. directly on its exact machine string. The files import Individual62 and standard Rocq libraries; neither proof depends on the other file.

The moving particles and binary digits build on SBCv7.v, Module TM4. Both holdouts appear in dyuan01's October 1 longitudinal-filter list; this proof uses direct window lemmas and arithmetic rather than the Longitudinal library.

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-ups: https://github.com/DennisKoshta/busycoq/blob/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/sync-counter/README.md

AI assistance: the proofs and original write-ups 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.