Internal safety with an unlimited prefix

This is a local mathematical reduction, not a proof about the blank-tape orbit. It removes internal halting from the right-word obligation. The finite supply of prefix blocks remains essential.

Configurations and invariant

Take a two-sided binary tape with a head in state A or C. For head position h, call the cells strictly to its left the left prefix. Assume this entire left prefix contains no adjacent zeros:

for every i with i+1 < h, (tape[i], tape[i+1]) != (0,0).

An infinite repetition of 011 to the left satisfies the condition. The tape on and to the right of the head is arbitrary. The current cell is deliberately excluded from the invariant.

Exhaustive reduced steps

Words below are finite windows. For A rules with a final marked bit, the head starts on the final displayed bit; for A00/A01 it starts on the first bit. For C1 it starts on the displayed bit; for C10/C100 it starts on the final displayed bit. A head displacement is measured from its input position.

The A cases are exhaustive. If the scanned bit is zero, use one of the first two rows. If it is one and its predecessor is zero, the preceding cell must be one, so the window is 101. If the two final bits are 11, the next cell to the left is either one (window 111) or zero; in the latter case its predecessor must be one (window 1011).

The C cases are exhaustive for the same reason. A scanned one uses C1. A scanned zero has either a one immediately before it, giving C10, or a zero followed on the left by a one, giving C100.

Every row executes only defined transitions. The previous general A/C reduction also had the hazard windows A001 and C000. Both require two adjacent zeros strictly left of the input head, so neither satisfies the invariant.

Preservation

Each left-moving row writes only strictly to the right of its output head. Its new left prefix is therefore an unchanged subset of the input left prefix.

For A00 and A01, the new part of the left prefix is respectively 10 or 11. The first newly written cell is one, so its join with the old prefix cannot create 00. Neither appended word contains 00.

C1 appends one. C10 appends zero, but the preceding cell is one. Both preserve the condition.

The result is again an A/C configuration satisfying the same invariant. Induction supplies arbitrarily many defined transitions, since each reduced step takes a positive finite number of primitive steps. Thus every such two-sided configuration is nonhalting.

Application and limit

The virtual-reserve transducer starts in C on an arbitrary finite word w, with an infinite 011 prefix on its left and blank tape on its right. Consequently it cannot halt internally, regardless of w. It may return to the chosen finite interface, or continue forever; no termination claim is needed for this safety lemma.

A real configuration has blank tape far to its left. It does not satisfy this global invariant. The transducer agrees with the real machine only while each requested prefix block exists. At zero reserve, A-entry into the last remaining 1 can reach E0, while D0 can instead escape forever to the left. This lemma does not bound reserve consumption or exclude the unsafe zero-reserve entry on the blank-tape orbit.

The derivation above is now formalized in ../LocalSafety.v. Its general theorem and unlimited011 corollary compile with closed assumptions. The primitive local rules are also formalized in ../LocalRules.v. No whole-machine blank-start theorem follows from this note.

Exact finite-reserve boundary alternatives

For this statement start directly in C on w, immediately after L_k = 1(011)^k, with blank tape left of L_k. Let the virtual call request d prefix blocks before returning at the interface in A, E or F. The virtual call, and its interface event sequence, do not depend on k.

If k < d, the real computation agrees with the virtual call until request number k+1. It then reaches D on the final remaining prefix 1, with a zero immediately on the right. D writes zero and moves right into F. The current cell and every cell to its left are now zero, so F moves left forever. The escape is already established one step after this boundary event; two additional F0 steps put the head one cell left of the original prefix.

If k = d and the virtual exit is A, the real machine reaches A on the single remaining prefix 1. It writes zero and moves left into D on blank, then writes one and moves left into E on blank. E0 is undefined, so it halts after two more defined transitions.

If k = d and the exit is E or F, that state reads the remaining prefix 1 and moves left into A in one step. This is a genuine left return. Its future safety depends on the resulting word; it is not a nonhalting conclusion.

If k > d, the positive-prefix return rules apply. If the virtual call continues forever with only finitely many requests and the real reserve is not exhausted, the real machine follows that infinite computation. If it makes more than k requests, the finite machine escapes at the first unavailable request as above.

Consequently, for a fixed terminating A-exit core call, the single reserve value k=d halts during that call. Smaller reserves escape, and larger reserves return. This is why a cumulative lower bound is sufficient but is not the only possible route to a nonhalting proof. One could instead exclude the exact dangerous coincidence of an A exit and zero remaining reserve.