Partial proof: local rules and the left boundary
This is an informal specification for reusable local lemmas. It is not a complete proof from the blank tape. The missing step is a preserved language for the changing left word, or a potential that excludes its halting boundary. The completed invariant study is recorded separately.
The machine is 1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA. A right-facing head reads the first symbol on its right; a left-facing head reads the last symbol on its left. Finite words below are written in tape order. Unspecified exterior tapes are arbitrary unless a blank tail is stated.
Confined left and right sweeps
An A head entering 111 from the right leaves 011 and exits left after five transitions. Entering 101 similarly leaves 110 after three. More generally, entering 1 0^n 11 from the right leaves 0 1^(n+2) and exits left after n+5 transitions. The latter follows by the initial four transitions into F, n applications of F0, and the final F1 transition.
A C head crosses a 1 without changing it. Reading the zero of 10, it exits right after five transitions with the word unchanged. Reading the final zero of 100, it turns left in A after three transitions, leaving 111. These rules retain the undefined E0 branch rather than assuming it is absent.
The prefix and its zero case
Let L_k = 1 (011)^k. When k is positive, entering its last symbol in A, E, or F gives the interface table in the completed study. The k=0 case is different and cannot be discarded.
For L_0 = 1 with a wholly blank left tail:
| Entry | Local result |
|---|---|
| A on the 1 | Reaches undefined E0 after two defined transitions |
| E on the 1 | Writes 1 and moves left in A after one transition |
| F on the 1 | Writes 0 and moves left in A after one transition |
| D on the 1, next symbol 0 | Replaces 10 by 11 and enters F on the blank left tail after three transitions |
| D on the 1, next symbol 1 | Replaces 11 by 10 and exits right in C after four transitions |
The F sweep reached by the D0 row never halts: F0 writes 1, moves left, and stays in F. Each next cell is still blank. The table's separate F-on-1 row merely returns to A and is not by itself a nonhalting result. Thus exhaustion of the prefix has both a halting A branch and a nonhalting D0 branch. A complete proof must distinguish them.
Uniform bulk roundtrip
The fixed words Q, P, R, W, G, and T are defined bit for bit in the completed study's study/bulk-right-rule.json and study/right-reflection-rule.json. Q, P, and R each have 51 cells, W has 70, G has 24, and T has 94. The Coq definitions Qblk, Pblk, Rblk, Wguard, Gguard, and Ttail use those same tape-order words.
Entering Q from the right in A transforms it to P and exits left. A C head immediately after W consumes one P on its right, replacing WP by RW and ending after W. A final C reflection consumes G, W, T, and eight following zero cells, replacing the whole 196-cell window by PPT and exiting left in A. Each of these finite runs is confined to its stated window, so both external tails are arbitrary.
The finite word identity G R = Q G implies G R^n = Q^n G by induction. Apply the C sweep n times, rewrite the left word using that identity, reflect at the right tail, and apply the A sweep n times. This gives the uniform transition
left G W C> P^n T 00000000 right
-->+
left <A P^(n+2) T right
This holds for every natural n, including zero, and arbitrary exterior streams. The finite reflection makes the combined execution nonempty even when n=0. The machine-local modules certify reachability and progress. The independently checked reusable finite-window composition additionally certifies exactly 906n+2881 transitions.
Ordered run sweeps
The new run-word reduction groups an A sweep by the length of its current run of ones modulo three. Each trailing triple becomes 011 after five transitions, with A three cells farther left. Once those triples have been removed, four finite cases remain:
| Remaining input before the emitted triples | Result |
|---|---|
0 111 |
1011, C reading its third cell |
1 0 1 |
110, A immediately left |
0 0 1 |
010, E reading its first zero, hence halting |
1 0^z 11 |
0 1^(z+2), A immediately left |
The suffix of emitted 011 blocks is unchanged by these residual cases. This gives exact conditional run transformations for any number of triples. It does not show which case the blank orbit will reach.
A C head crosses any word assembled from the tokens 1 and 10 without changing it. Appending 100 then gives the first double-zero reflection. Induction on the token sequence proves this symbolic scan; the final reflection is confined and leaves A immediately to the left of the final 111.
Unbounded prefix lookahead
The complete compositional derivation in invariant-study-20261014/lookahead-obstruction.md gives pairs of finite inputs sharing arbitrarily long left prefixes whose first left exits differ. The stronger pair exits in A or D. Attaching a single one and a blank left tail makes the A example halt and the D example escape forever in F. These are constructed inputs, not claimed reachable from the blank start. LocalObstruction.v formalizes these conditional families and has passed a separate kernel recheck. Their purpose is to rule out deciding this interface from a fixed-length prefix alone.
Concrete finite entrance
The saved primitive run reaches normal form k=1 with the explicit 81-bit residual word in invariant-study-20261014/earlier-common-entrance.json after 5,104 transitions. The head is in A on the leading zero, with blank tape farther left. A finite-window computation can certify this exact entrance from blank tape; LocalEntrance.v proves it with the full residual word and counted reachability, with closed assumptions and a separate kernel check. This establishes a concrete starting point for a future invariant and does not establish its safety.
Formal scope
LocalRules.v establishes the local statements and finite bulk components. LocalBulk.v composes the uniform roundtrip; LocalSweep.v states the ordered run transformations. These use the pinned, unmodified busycoq framework. All six machine-local modules compile, and independent kernel checks completed successfully. The receipt is ../../astra/autonomous-20261014/local-rules/verified-components-final.json. None supplies a theorem that the blank initial configuration never halts.
The additional internal-safety proof is given before formalization in invariant-study-20261014/internal-safety.md. At an A/C boundary, assume the infinite strict-left tape contains no adjacent zeros. Rightward macro steps append either a 1 or a zero preceded by 1; leftward macro steps write only to the right of the new head. The complete case split therefore preserves this condition and always supplies positive progress. LocalSafety.v proves that conditional nonhalting result. Its infinite-left premise does not hold for the blank tape and does not settle the finite-prefix problem.
AI assistance: this proof sketch, the scripts and the checks were produced with the help of GPT-6 Astra (OpenAI).