A counter tail that escapes into a translated cycle

This package proves nonhalting from blank tape for:

1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF

The machine eventually repeats a 919-step motion shifted three cells left. The proof connects the blank-tape opening to that motion through a finite sequence of counter overflows and nested exceptional calls.

• SOBCv10Tail.v: complete Rocq proof, including the counter rules it uses.
• proof.md: mathematical explanation of the opening, finite invariant, and escape.
• verification.json: exact source hash and the results of three fresh proof checks.

Build with Coq 8.20.1 from a busycoq checkout whose framework modules are built:

coqc -Q verify BusyCoq -Q verify/BigInt BigInt -native-compiler yes SOBCv10Tail.v

The final statement is:

Lemma nonhalt : ~ halts tm c0.

The only reported assumption is the framework's permitted functional extensionality. The proof's complete dependency closure is byte-identical between the pinned framework and the checked current BB6 branch.

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