Nonhalting by a nested counter overflow

1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF

This machine builds binary counters and repeatedly replaces a counter overflow with a much larger counting task. A short tail changes those tasks in a predictable way. Eventually an overflow happens inside an overflow routine, sending the head into a repeating motion that continues forever.

The final motion repeats every 919 steps and shifts three cells to the left. The proof establishes that the blank-tape computation reaches this motion; it does not rely on simulating the enormous intermediate counters.

The counter representation

It is convenient to reflect the tape and rename the states. The resulting transition table is the one formalized in SOBCv10.v, with initial state D. The state map from the displayed machine is:

A B C D E F
D E F A B C

In this reflected frame, the counter is to the right of a wall and a unary tally. A signal travels right through the counter and returns left. Each successful return adds one unit to the tally.

The counter uses the following tape words. These capital letters name words, rather than machine states.

Digits are ordered from least to most significant. A signal carries through B, changes A to B, changes D to A, or changes E to D. Separators transmit signals unchanged.

An overflow can turn the left tally into a new source of calls. This is an exceptional call. The proof tracks both the counter word and the exact number of calls supplied by this left side.

The opening

A finite execution of 43,119 primitive steps reaches the third completed exceptional call, with index 28. The counter rules then give the fourth index:

n4 = 3*2^29 - 2 = 1610612734.

The fourth exceptional call and its following marker traversal produce a word containing adjacent D digits and a later E digit. The following rule handles it for every positive p and even m:

A^p C A^m D D A U E A  ->  B^(p+m+5) U B t

number of returning signals = 2^(p-1)*(1292*2^m+4)/3 - 1.

Apply this rule with p equal to n4 and m equal to 30. Combining its count with the preceding marker traversal gives exactly the tally for the fifth exceptional call:

Q  = (1292*2^30+4)/3 = 462424812204
n5 = 2^n4 - 2 + 2^(n4-2)*Q.

The fifth decode is proved with a symbolic primary width and an exact 36-digit suffix. Its output feeds a marker traversal that reaches the first configuration in the next table. All large powers stay symbolic in the proof.

Three returning rounds

The rightmost column may contain negative digits. Keeping its signed value is essential: its residue alone does not record how many calls are needed before a carry reaches the tail.

The tail has the form shown in the last column below. Each returning round shortens the rightmost column by one digit and adds a new ordinary column near the primary counter.

Every newly created ordinary column supports at least three further safe transformations, independently of the parity supplied by the next column. A round consumes one such transformation. This finite allowance suffices because only three returning rounds are needed before phase 4.

The invariant also bounds the combined column widths by the two most recent exceptional indices. Those bounds keep the next primary counter wide enough. Separate arithmetic identities show that the odd left tally supplies the required even number of calls. The formal round theorem proves the actual machine traversal and every condition needed by its successor.

The fourth round triggers a nested exception

In phase 4, the raw pass leaves a 25-digit last column and tail U^11 A t. The supplied calls fill the counter and change the tail to B t while another call is still available. That next call starts a nested exception.

The count comparison can be made without evaluating the large column widths. Let the widths of all columns before the last one be the list w. Propagate a count from right to left through each width using:

T_width(x) = (x+2)*2^width - 3.

For the actual fill, start with 134217725 and apply these transformations through w. For the calls needed by the nested counter, start with:

3*(2^24-1) = 50331645.

Each transformation is increasing, so the completed-call count is sufficient for the nested counter. A separate decode comparison starts from 158684500; since this exceeds 134217725, the first trigger occurs before the outer call supply runs out. The formal caller lemma retains the remaining outer calls and proves the exact configuration at the trigger.

Escape and infinite motion

The nested exception makes another raw pass, leaving a 24-digit last column and tail U^13 B t. Its proved call supply fills the counter again. The next overflow exits the counter system instead of returning to the left tally.

The exit reaches a fixed 70-cell word Y next to blank tape. In the reflected frame, a direct 919-step rule proves:

L Y B> 0...  ->  L 100 Y B> 0...

This holds for every left context L, which the routine does not read. Repeating the rule proves nonhalting. Reflection turns the three-cell rightward displacement into the claimed leftward motion of the original machine.

The final theorem applies this result to the exact transition string and the standard blank configuration. Its assumptions are limited to the functional extensionality already permitted by the framework.

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