This adds a blank-tape nonhalting proof for 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB. The machine shuttles between a wall and a binary counter, consuming a bell of 10 pairs. A bite at the counter can open nested copies of the same process.

The proof combines a size bound with a nonzero residue modulo 3 that each completed cycle negates. The left tape is represented as a stack of frames. Phase invariants preserve the arithmetic bounds through counter rounds, and stack lemmas handle nested bites.

Nonhalting follows by strong induction on the number of steps; the argument does not require termination of every nested level. The blank run reaches the invariant after 327 steps, at cycle parameters (6,5,0).

The low-level rule layout is adapted from BECv5.v, TM1. This machine uses a decrementing counter with three-cell digit spacing, width-dependent overflow rules, and nested levels. The proof imports Individual62 and the standard library, with top-level theorem:

Lemma nonhalt: ~halts tm c0.

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.

Informal proof · Space-time image

AI assistance: the original proof, proof sketch and checks were produced with the help of Claude (Anthropic); independent audit and submission preparation with GPT-6 Astra (OpenAI).

Downloads: write-ups ZIP · images ZIP.