This adds a blank-tape nonhalting proof for 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC. A moving marker increments a counter, consumes its low digit, and leaves a residue whose cleanup can run a nested epoch.

The proof formalizes the local pass and epoch map as mutually inductive relations. Weighted potentials bound the cleanup cost, created counter positions, and merged block exponents. An invariant shows that cleanup finishes before the next unsafe consumption.

The checked finite prefix runs 691 epochs to budget 17,713. Beyond that point, the invariant applies with threshold 17,705 and gives nonhalting through progress_nonhalt_cond.

This is the blank-start case stated by the exact machine string above. PR #22 treats two other starts of the same transition table; those are separate blank-start machines.

The marker-bounce construction is adapted from FractalBEC.v, tm10. The counter representation, partial consumption and nested cleanup require a different invariant. 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.