An exact word/counter normal form, including zero reserve
This reduction preserves the whole right word. It is not an arithmetic recurrence or a nonhalting proof. It gives a complete boundary case split and identifies the one unresolved halting branch.
Normalized configurations
Write N(k,w) for A on the first zero of
0 (011)^k w,
with blank exterior. The finite word w is stored without trailing zeros, and leading 011 blocks are absorbed into k. The domain is
k >= 1 and arbitrary w,
or k = 0 and w begins with0 (including the empty word on blank tape).
The blank initial configuration is N(0,empty). A zero-reserve word beginning with one is outside this chosen section. The rules below preserve the section, so no such missing case is encountered between normalized steps.
The virtual core
Run C on w with an unlimited 011 reservoir on the left. At the finite interface, a D call with right bit zero consumes one reservoir block; its word replacement is 0v ->1011v, with C on the fourth output bit. A D call with right bit one replaces 1v ->0v and returns C on the second output bit. The times are seven and four respectively.
Let d count the consuming calls, let tau be the virtual core time, let v be its final right word, and let s be the terminal interface state A, E or F. The core is independent of k. At E or F exit, v necessarily begins with one: the preceding D0 or F0 transition just wrote that first cell.
The formal strict-left no00 invariant excludes internal halting. A core that never returns is an infinite computation unless the real finite reserve encounters an unavailable consuming call; that call takes the certified left escape. An implementation with a finite cap may return “unfinished”, which is not a nonhalting certificate.
Entering the core
For k>=1, the initial C sweep takes 7k-3 steps and leaves the prefix L_k=1(011)^k, with C on the first bit of w.
For k=0, w begins with zero. A00 reaches C on the second cell of w in two steps. Starting the virtual core in C on its first zero reaches the same configuration by C10 in five steps, without consuming a block. Therefore the virtual core has a three-step head start in its accounting. The same formula can be used with entry offset 7k-3=-3; this is an accounting offset, not a negative transition sequence.
The first left return or terminal event
If a consuming call is requested after the reserve is empty, the real machine enters F on a zero with an all-zero left tail and moves left forever. This occurs when the virtual call has more than k consuming events, at event number k+1. It is already certified one transition after that event.
Otherwise put r=k-d. If s=A and r=0, the real machine halts at E0 two transitions after the core endpoint. This is the only halting branch in the reduction.
In all other cases there is a first left return, with A one cell left of the old initial head. Its finite tape is:
| Core exit | Domain | Tape beginning at new head | Time after core endpoint |
|---|---|---|---|
| A | r>=1 | 0 (110)^(r-1) 0111 v |
3r+3 |
| E | r>=0 | 0 (110)^r 1 v |
3r+1 |
| F | r>=0 | 0 (110)^r 0 v |
3r+1 |
Add the entry offset and tau to these times.
Returning to the normalized section
If the first-return tape starts with 011, the seven-step A011 rule leaves those bits unchanged and places A one further cell left. The tape is obtained simply by prepending a zero. This happens for A when r>=2, for every E exit including r=0, and for F when r>=1. For E at r=0, it follows from the fact that v begins with one.
The resulting two-return formulas, before stripping leading 011 blocks from the indicated residual word, are:
| Exit | Raw reserve | Raw residual word | Total time from N(k,w) |
|---|---|---|---|
| A, r>=2 | r-1 | 00111v |
10k+tau-3d+7 |
| E, r>=0 | r | 01v |
10k+tau-3d+5 |
| F, r>=1 | r | 00v |
10k+tau-3d+5 |
If the raw residual starts with c copies of 011, move those copies into the reserve. The reserve update is therefore
k' = k - d - [s=A] + c.
There are two one-return boundary cases. For A with r=1, the first-return tape is already N(1,1v). For F with r=0, canonicalize 0v: strip its leading 011 blocks into the new reserve. If no such block exists, the new reserve is zero and its residual still begins with zero. Both outcomes satisfy the entry domain.
For E at r=0 the ordinary two-return formula applies, and canonicalization adds at least one block because 01v begins with 011. Thus zero-reserve E does not require a separate unresolved continuation.
The common word trajectory and its boundary
In the two-return domain, the next word depends only on w. Write its reserve debit as
delta(w) = d + [s=A] - c.
Its reserve threshold is d+2 for A, d+1 for F, and d for E, together with the entry-domain requirement k>=1 if w starts with one. If D_i is the sum of earlier debits on this common word trajectory, every initial reserve K satisfying
K >= sup_i (D_i + threshold(w_i))
follows that trajectory indefinitely and remains safe. A finite bound for this supremum would suffice for the blank-orbit problem after a suitable entrance state. No such infinite bound has been proved.
Below a threshold, a finite-reserve computation can halt, escape, or make one of the explicit boundary restarts. The A/r=1 and F/r=0 restarts can change the word trajectory. Consequently there is no justified claim that one k-independent word trajectory classifies every initial reserve forever.
Validation
astra/study_593_normal_form.py starts from (k,w)=(0,empty). Its 399 normalized steps reproduce all 792 saved primitive new-left records exactly, including every tape bit up to blank-tail equivalence, absolute head positions, and transition counts. There are 393 two-return steps and six one-return boundary steps. The last saved record is at step98,148,758, head-792, reserve25.
The separate common-trajectory ledger starts at record100 with reserve7. Across the next346 two-return steps, its smallest initial reserve that keeps every step in the common domain is5. The cumulative debit is-18 and the final actual reserve is25. This is a finite-prefix pumping statement, not an infinite safety bound.
The exact remaining task is to show that the normalized blank orbit never takes s=A,r=0, or to prove that it eventually takes the infinite F escape. Local safety and finite replay do not establish either alternative.