1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---: never halts (informal proof)

Internal informal proof for W4-3 (740 list line 341) and its two siblings, lines 512 and 588, which run the same table from other start states. It assembles the results of the rules, macro, induction and close-out stages into one induction. Every claim is checked by check_proof.py in the machine directory; section 9 says which check backs which claim, and the appendices list the finite data (right table, interval programs, base configuration) verbatim.

Status: all three strings KILLED_NONHALT (2026-10-12). Section 10.3 says how the formalization followed and departed from the lemma plan, and gives the sibling plan (this kill file with the table renamed tmP, plus perm_halts / flip_halts).

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

Overview

The machine is a ternary counter that never finishes counting.

The tape is almost everywhere an alternating pattern ...0101.... The only interesting places are defects: two equal neighbouring cells. The head sweeps back and forth, and it can only change the tape at defects.

The defects form three regions:

• a left word of 10 defects next to the left end, which counts to 81 and then moves 3 cells left;
• a chain of K digit blocks, a base-3 counter that the head increments once per visit from the right;
• a right region: old blocks ("fossils"), and two growing blocks X and Y next to the right end.

Every 81 x 3^K visits the left word overflows. At that moment the chain is regrouped, K changes, and the right region starts the next of six phases. After six phases the whole picture repeats with K larger by 2 and every long block 9 times longer.

The proof is an induction over these six-phase periods. Each step is assembled from three finite lemmas (one per region) and a symbolic computation that is exact for every period.

1. The machine

     0    1
A   1RB  0RF
B   1RC  0RB
C   1LD  0RA
D   1LE  0LD
E   1RB  0LC
F   1LA  ---

The only undefined transition is F reading 1. F is entered only from A reading 1.

The siblings are the same table started in another state:

2. The defect model

2.1 Defects and the head phase

Number the cells by integers. Edge e lies between cells e and e+1. Edge e is a defect if cells e and e+1 hold the same symbol.

• Far to the left and far to the right the tape is blank, so every edge there is a defect. Write lo and hi for the ends of these two blank zones: every edge below lo and every edge at or above hi is a defect.
• D is the finite set of defects strictly between them.

A sweep of the head over alternating cells runs through a fixed 4-cycle of states, and every sweep step writes the complement of the cell it reads:

moving right: B0 C1 A0 B1 B0 ...      (1RC, 0RA, 1RB, 0RB)
moving left : D1 D0 E1 C0 D1 ...      (0LD, 1LE, 0LC, 1LD)

So between defects the head is described by its direction and a phase φ in Z/4:

moving left : D1 at cells = φ,   D0 at φ-1,  E1 at φ-2,  C0 at φ-3   (mod 4)
moving right: B0 at cells = φ,   C1 at φ+1,  A0 at φ+2,  B1 at φ+3   (mod 4)

A sweep complements every cell it crosses, which keeps every defect where it is. So D changes only at the events below. D is read in the frame "before the current sweep": the edge between the head and the cell it has just left is counted as it was before the sweep complemented that cell.

2.2 The eight rules

At a defect e the head sees d = (e - φ) mod 4. Here ^ is symmetric difference.

Turns keep φ. A turn moves the defect by one cell, a wiggle by two.

Each rule is a run of two to five transitions at the defect. The state on the near cell follows from the phase; the far cell holds the same symbol as the near one, which breaks the cycle:

Halting. The machine halts only through F reading 1, and F is entered only by A1, which occurs only in the wiggle. There F reads cell e+2, and cell e+2 holds 1 exactly when e+1 is also a defect. So the machine halts exactly when the head moves right, sees d = 1, and e+1 is also a defect.

Collisions. A turn or wiggle whose toggled edge is already a defect makes two defects cancel. Any proof step below that runs "without collision" never meets this case or the halting case.

The model was compared with direct simulation of the table (check S2):

• exhaustively, on every tape word of length 1 to 12 between blank ends, with the head on every cell within 2 of the word and in every sweep state (122,884 runs, 34,134 of them ending in the halt);
• on 10,000 random tapes of up to about 2,400 cells;
• on the run from the blank tape: the record-exit configurations of section 8 are reproduced exactly.

2.3 Decisions depend on residues only

Every decision uses only d, that is the defect position mod 4 relative to the phase, plus the order of the defects.

So two tapes whose defects have the same order and the same residues mod 4 behave identically, as long as no collision happens. A collision needs two defects within 2 cells of each other. This is the reason long gaps can be treated as counters that only matter mod 4. Lemma 2.4 makes this precise.

2.4 Stretching a gap (the transfer lemma)

Several lemmas are checked at small gap values and then used for every larger value with the same residue. One argument covers all of them.

Lemma 2.4 (transfer). Take a run of the defect model and an edge m such that during the run no defect ever sits on the edges m - 1, m, m + 1. Make a second tape by inserting 4j cells between cells m + 1 and m + 2 that continue the alternation. In defect terms:

D'  =  { e : e in D, e <= m }  ∪  { e + 4j : e in D, e >= m + 1 }

and the head, if it is right of m, moves up by 4j with the same phase. Then the two runs have the same events (same rule, same d, at corresponding defects), and after every event the configurations correspond in the same way.

Proof. Induction on the events.

• The inserted stretch holds no defect, so the head's next defect is the corresponding one.
• A shift by 4j does not change d = (e - φ) mod 4.
• A rule at a defect e toggles or tests only edges in [e - 1, e + 2]. By the hypothesis e is never m - 1, m or m + 1. For e <= m - 2 all these edges are at most m (not shifted); for e >= m + 2 all are at least m + 1 (shifted). So the toggles correspond, and the halting test (is e + 1 a defect?) has the same answer.

Use. If a run with a gap g keeps three consecutive edges of that gap free of defects throughout, then the runs with g + 4j, j >= 0, have the same events. This is applied to the gaps inside a block (4.1), to the long gaps of the right region (4.3), and to the deep chain gaps (only residues and minimums matter).

3. The configuration at a record exit

3.1 Records and classes

Let λ be the leftmost cell that has held 1 at some step so far, and lo = λ - 1. Then λ only moves left.

In the run of line 341 from the blank tape, λ moves left

• by 1 or 2 cells at steps 1, 6-7, 838-839, 7820 and 17531-17532 (the start-up), and
• otherwise always by 3 cells, in 3 consecutive steps.

A left record is a move of λ by 3 cells. Only these moves are numbered: n = 1, 2, 3, ... in order. Record 16 is the move at steps 398,088,768-770 (check S10, direct simulation).

Line 512 has the same numbering. Line 588 has one more 3-cell move in its start-up, so record n of line 588 is its (n + 1)-th 3-cell move. From record 16 on, lo moves only in left episode 81 (Lemma L81), by 3 cells, so there is exactly one record per interval and the numbering stays aligned.

The class of record n is r = (n - 11) mod 6, written r0, ..., r5. The epoch is e = (n - 16) div 6, so records 16-21 have e = 0, records 22-27 have e = 1, and so on. Classes come in the order r5, r0, r1, r2, r3, r4 within an epoch.

The record exit of record n is defined in 3.3 (H): the first moment after left record n at which the head, moving right, has just passed the chain end B - 2.

3.2 Blocks

A block is one digit defect followed by m separator defects, m = 1 or 3. Its base b is the digit's position in state U0, and its separators sit at b + g1 < b + g2 < b + g3 with g_i = 1 mod 4.

Eight block states for m = 3, as offsets from b:

For m = 1 the states are Us = (-s, g1) and Dk = (-2, g1+k). There U2 and D0 are the same configuration, and there is no W state.

A block is full in state U2 or D0. The phase that belongs to a block is c = b + 1 mod 4, the residue of its separators.

Read in the U0 state, every gap of a chain has a role:

3.3 The invariant

Fix a record exit of class r and epoch e. Let K = K0(r) + 2e with

The configuration C_r(e) consists of the following, for some cell A.

(L) Left word. lo = A - 34, and the defects left of A are

A - 32, -27, -26, -21, -20, -15, -14, -9, -8, -4

(C) Chain. The defects in [A, B] are K blocks, all in state U0:

• block 1 is (A+2; A+3) with m = 1;
• blocks 2..K have m = 3, and each base is 2 more (mod 4) than the one before;
• every chain gap has the residue and at least the smallest value of its role (table above);
• the last separator of block K is at B - 2.

(W) Window. The last J(r) chain gaps, and the gaps from B through the right-region defects up to hi, are given exactly by the vector V_r(u) of section 3.4, where u = 9^(e-2).

(H) Head. The head is on cell B - 1 in state B, and cell B - 1 holds 1. State B moves right.

• In phase terms: the head moves right with phase φ = c_K + 2, where c_K is the phase of block K. Cell B - 1 is c_K + 1 = φ + 3 mod 4, the B1 place of the right cycle.
• It has just passed the last separator B - 2 with d = 3 (transitions B1, B1 on cells B - 2 and B - 1).
• On the actual tape cells B - 2 and B - 1 differ, because the sweep has just complemented cell B - 2. Edge B - 2 is a defect in the pre-sweep frame of 2.1, and it is counted as one.

Locating A and B. A = lo + 34 and K = K0(r) + 2e. The chain holds 4K - 2 defects, from A + 2 (the digit of block 1) to B - 2, so

B  =  (the (4K - 2)-th defect at or right of A)  +  2

The record exit, operationally. The record exit of record n is the first configuration after left record n in which

• the head is in state B reading 1, and
• exactly 10 + 4K - 2 edges in (lo, h - 1] are defects in the pre-sweep frame (h = head cell; the edges up to h - 2 as on the tape, edge h - 1 toggled).

Then B = h + 1. The 10 are the left word, the 4K - 2 the chain. This is the moment of (H): after the record the head runs the carry back from left to right, and before it first reaches cell B - 1 the defect at B - 2 is not yet behind it; directly after passing B - 2 it reads B1 on cell B - 1. Check S10 finds the record exit 16 of all three strings by this definition on the direct simulation, and checks (H) and the formula for B at every record exit 16-39 (line 341) and 16-33 (lines 512, 588).

3.4 The window vectors

Each entry of V_r(u) is affine in u = 9^(e-2), and is valid for e >= 2 (u = 1, 9, 81, ...). The chain part lists the last J(r) chain gaps; the right part lists the gaps B -> x_1 -> ... -> hi.

For example, at record exit 28 (class r5, u = 1) the right region reads

B  -224493-  x1  -673559-  x2  -7-  x3  -9841-  x4  -1942040-  x5  -3-  hi

Reading the right part:

• the first gaps are fossils, old Y blocks. Their exact lengths never matter, only their residues mod 4 and that they are long;
• then comes a short gap (2 to 8 cells) at the left end of X;
• then the blocks X and Y, whose exact lengths are tied to K (section 5.4);
• the last gap (2 or 3) is the distance to the blank right end.

For e = 0 and e = 1 (records 16-27) the same description holds with concrete numbers instead of V_r(u). Appendix C lists them. There the window still contains start-up values, such as the first fossil (969 to 973 cells).

4. Three regions, three lemmas

Between record exits, the head moves inside one region at a time and crosses the boundaries A and B with a known phase. Each region has its own lemma.

4.1 The chain lemma

A visit is the head entering the chain from the right at phase c_K. Read the chain as a ternary number, with the block values as digits and the least significant digit on the right.

Lemma C (visit). Suppose the chain word has the shape D^a [W] U^b (left to right). Then:

• Not all full. The value goes up by 1, and the head leaves to the right.
• The rightmost non-full block moves to its successor: U0 > U1 > U2, W0 > W1 > D0, D2 > D1 > D0.
• The full blocks right of it are reset to value 0. After a U or W turn they all become U0. After a D turn, the D0 blocks become D2, the first U2 becomes W0, and the other U2 become U0.
• Exit phase: c_K if the turned block is a D block and the last block is D afterwards, else c_K + 2.
• All full. The head leaves to the left at phase c_1 + 2, and the chain is unchanged (a carry-out).

Lemma C' (carry back). If all blocks are full and the head enters from the left at phase c_1 + 2, every block is reset to value 0 with the D-turn labels. The head leaves to the right at phase c_K if the chain is then all D, and at c_K + 2 otherwise.

The shape D^a [W] U^b is preserved by both lemmas.

The single-block runs. The lemmas are compositions of 18 runs on one block. Each entry gives the exit side, the change of phase between entry and exit, and the new state; entry phases are relative to the block's c.

Appendix D lists the events of each run: for every event the direction, the defect (dg = digit, s1-s3 = separators, sp = the m = 1 separator), d and the rule of 2.2. A reader can replay each run with the table of 2.2.

Lemma B (one block). Let a block have digit gap at least 1 and separator gaps at least 4, with the residues of 3.2 (for m = 1 the digit gap is the only gap). For each of the 18 runs:

1. Events. The run has the event list of Appendix D, whatever the gaps.
2. Footprint. During the run each defect stays within these offsets of its U0 place:

m = 3: digit -2..0 s1 0..+2 s2 0..+3 s3 0..+2 m = 1: digit -2..0 separator 0..+2

Every edge the run toggles or tests (the wiggle's e + 1) lies between two places of one defect. So the run touches only edges in [b - 2, b + g_last + 2], where g_last is the offset of the last separator. 3. No halt. A wiggle at e tests e + 1, which lies strictly between the old and the new place of the moved defect. By the footprint no other defect of the block is there, so no wiggle halts.

Proof. Check S3 runs every combination of the gaps in {tight, tight + 4, long}, plus 40 random choices per run (1,045 runs on the exact model). All give the same event list and stay in the footprint.

Larger gaps follow from the transfer lemma 2.4. By the footprint, a digit gap of 5 or more keeps the edges b + 1, b + 2, b + 3 free of defects, and a separator gap of 8 or more keeps three edges in its middle free (s1 stays at most g1 + 2 and s2 at least g2; s2 stays at most g2 + 3 and s3 at least g3). So a gap of tight + 4 + 4j runs like tight + 4. The tight values (digit gap 1, separator gap 4) are their own cases.

Lemma B' (blocks in a chain). In a chain with inter gaps at least 5 (U0 frame), each single-block run is exactly the run of Appendix D, and a visit is a sequence of such runs.

Proof. By the footprint, the defects of block j always lie in [b_j - 2, b_j + g3_j + 2]. These intervals are disjoint for different blocks: an inter gap of at least 5 leaves at least one edge between the end of one interval and the start of the next. (With inter gap 5 two neighbouring D blocks can touch, at distance 1, but their intervals still do not overlap.)

So a run on block j never toggles or tests an edge of another block's interval. Between two of its events the head meets no defect of another block, because those lie outside block j's interval, in their order. When the run ends, the head leaves block j's interval and its next event is the first event of the neighbour's run, at the phase where block j's run left.

At the two ends of the chain: block 1's interval starts at A, and the left word ends at A - 4. Block K's interval ends at B, and the right region starts at x_1, which is never touched (4.3).

Proof of Lemma C and C'. By Lemma B' a visit is a list of single-block runs, so Lemma C is an induction on the list, keeping track of the phase at each hand-over. Consecutive bases differ by 2 mod 4, so the c of the left neighbour is c + 2.

• A full block passed leftward exits at c + 2, which is the entry phase of the block on its left.
• A U or W turn sends c + 0 to the right block (its c + 2), and each reset U2 -> U0 passes that on.
• A D turn sends c + 2, D0 -> D2 keeps it, and the first U2 -> W0 switches it.
• The rightmost non-full block is the one that turns; the exit phase follows from the last run.

Cross-checks on the exact model (check S3): every word of the lemma's shape for K <= 2, and the pair (2, 3) at K = 3 entered from block 1, with every gap in {tight, tight + 4, long} and both entries (1,432,212 runs); 4,000 random chains with K = 3..10 and tight gaps (5,210 runs). All give the lemma's result, with no collision. No defect is ever left of A.

Lemma T (counting). Start from the record-exit chain: one m = 1 block and K - 1 blocks with m = 3, all U0. Then:

• the first T(K) = (3^(K+1) - 5)/2 visits exit at phase c_K + 2, and every later visit exits at phase c_K;
• carry-outs happen exactly every 3^K visits;
• from the second carry-out on, the chain is all D0 at every carry-out and all D2 after every carry back.

Proof: a suffix starting at W0 U0^(j-1) needs 2 x 3^(j-1) visits to reach D0 U0^(j-1), then 3^(j-1) more to reach D2 W0 U0^(j-2), then the (j-1)-suffix. So T(1) = 2 and T(j) = 3^j + T(j-1). The leading m = 1 block plays the role of W. Exit phase c_K happens exactly when the word is all D, and an all-D word stays all D. Since T(K) < 2 x 3^K, the chain is all D before the second carry-out.

Check S4: on chain words for K = 2..9, and on the exact defect model for K = 2..8 (the chain alone, re-entered from the left at c_1 + 2 after each carry-out, 81 x 3^K visits each).

4.2 The left end

At every carry-out the head crosses A leftward with phase 1 relative to A. It runs a left episode and crosses A rightward again.

The left word is a ternary counter. It consists of the two fixed defects A - 32 and A - 4 and four m = 1 blocks with digit gap 1. Write i = 1..81 and v = i - 1 = (v1 v2 v3 v4) in base 3, v1 most significant. Then

W_i  =  { A-32, A-4 }  ∪  { A+p_j-v_j , A+p_j+1 : j = 1..4 },      p = (-27, -21, -15, -9)

So block j is in state U_(v_j), with its base at A + p_j. W_1 is the word of (L).

Lemma L.

• Left episode i (i = 1..80) turns W_i into W_(i+1): it adds 1 to the counter. It is entered and left at phase 1 relative to A, which is the carry-out phase and the carry-back phase c_1 + 2 of Lemmas C and C'.
• Episode 81 (v = 2222) is the left record. The counter overflows into the blank zone: lo moves 3 cells left, and the word becomes W_1 moved 3 cells left, plus one new defect at A - 1. Lemma L81 states it exactly.

The left word contains no long gap, so each episode is a fixed finite computation of at most 31 events.

Lemma L81 (the left record). At the 81st carry-out of an interval:

• Input. lo = A - 34, the left word W_81, the chain all D0 (Lemma T) with block 1 at (A; A + 3), and the head moving left, about to read cell A - 1, at phase 1 relative to A.
• Output, after 31 events (Appendix E). lo = A - 37, the left word W_1 - 3 plus a new defect at A - 1, and the head on cell A, moving right at phase 1 relative to A. Its next defect is block 1's digit at A, with d = 3.
• On the way. No event is at a defect >= A, so the chain is untouched. Each of the six rightward d = 1 events (wiggles) finds no defect at e + 1, so none halts.

The new defect at A - 1 is made by the wiggle at A - 3 (event 30), whose test edge A - 2 is free. It is then passed with d = 3 (event 31). A rightward head with d = 1 at A - 1 would halt, since A is a defect; this never happens.

Phase 1 relative to A is c_1 + 2 (c_1 = A + 3). So the state after episode 81 is the entry of Lemma C' for block 1: D0, entered from the left at c + 2. The carry back starts from this state. By Lemma B the run D0 -> D2 of block 1 touches only edges in [A, A + 5], so the defect at A - 1 is neither toggled nor tested, and the head does not come back to it before the record exit.

• Left region alone (check S5): all 81 episodes, run in a row from W_1 on a tape that holds only the left region, give exactly the words above and the record. None halts.
• With the chain present: each episode is re-run with the first three chain blocks in their full states at the tightest gaps (4 contexts each, 324 runs). The result is the same and the chain is untouched. Episodes 1-80 have no event at a defect >= A - 3; episode 81 is Lemma L81, run with the whole chain in D0 at the tightest gaps.
• Conversely, chain events never move a defect left of A (4.1). While the chain is active, the left word's last defect is at A - 4, so the two never come within 2 cells of each other.

4.3 The right region

An episode starts when the head, moving right, has passed the chain's last defect B - 2, and ends when the head, moving left, has passed x_1 and its next defect is B - 2 again. In between it touches only defects right of B. There is no defect between B - 2 and x_1, so the head's phase there is well defined; it is the exit and return phase.

The shape of the right region is its list of gaps B -> x_1 -> ... -> hi. A gap below 24 is kept exactly; a gap of 24 or more is kept as ("long", gap mod 4), written Lc for residue c.

Lemma R. The result of an episode depends only on the exit phase and the shape. The result is the new defects (each as an old defect plus an offset), the new hi, and the return phase. Appendix A lists the 81 entries that occur, grouped by the class in which they occur:

Every entry returns the head at phase c_K, which is the entry condition of Lemma C.

Proof. Each entry is one finite run, the base run, made valid for all long gaps by the transfer lemma 2.4 (check S6).

1. The base run. On a tape that holds only the right region, with every long gap at its smallest value (24 to 27, by residue), the entry gives the table's result: the new defects, the new hi, the return phase and the counts.
2. Free stretches. In every base run, every long gap keeps at least 11 consecutive edges that never hold a defect and are never toggled or tested. No edge left of x_1 is ever touched.
3. Every longer gap. A long gap of value min + 4j is the base gap with 4j cells inserted in its free stretch. By 2.4, applied once per long gap, the run has the same events, so the entry's result holds unchanged: each new defect is the same old defect plus the same offset.

In simulation terms: the event sequences of the two runs are identical, by induction on the events, because two defects on opposite sides of a long gap always stay at least 12 cells apart, so no rule ever sees across the gap. 4. The chain plays no part. Nothing left of x_1 is touched, and the first gap B -> x_1 is long in every entry, so the chain (whose last defect is B - 2) is never reached.

Cross-checks: every combination of the long gaps in {min, min + 4} (5,376 runs), and every long gap increased by 4j, j up to 10^6 (810 runs), give the table's result. No run halts. The largest shrink of a long gap within an episode is 12.

The table was built from records 16-27 (262,430 episodes). It also predicts every one of the 2,125,759 episodes of records 28-33.

5. One record interval

5.1 The order of events

Start at a record exit in C_r(e). From there the head alternates between the three regions:

1. one episode (the record-exit episode, entered at phase c_K + 2);
2. then repeatedly: a chain visit (Lemma C), then an episode at the visit's exit phase (Lemma R);
3. every 3^K visits a carry-out instead: a left episode (Lemma L), a carry back (Lemma C'), and then an episode.

5.2 Counts

By Lemma T:

• the episode exit phases are c_K + 2 for the first T(K) visits and c_K afterwards;
• the interval has 81 carry-outs, the 81st being the left record;
• there are 81 x 3^K - 1 episodes after the record-exit episode, up to the next record exit.

5.3 The right region over a whole interval

With u fixed, the right region over an interval is a run of Lemma R entries with known exit phases. Long gaps are affine in u, so this run can be done symbolically. Appendix B lists the run for each class as a program:

• single entries, at the start, around the regime switch and at the end (20 to 30 per class);
• two 4-cycles, one per regime: four entries whose shapes come back after the fourth, with some long gaps changed by fixed multiples of 4. Each is repeated c times, c affine in u.

Gap maps. An entry puts every new defect at an old defect plus a fixed offset (Appendix A). On gap vectors this is an affine map: each new gap is a sum of consecutive old gaps plus a constant. With the small gaps of the shape written as numbers and the long gaps as variables g_i, for example

r1.1   (g1, 7, g3, g4, 3) -> (g1, 7, g3 - 1, g4 + 8, 2)

Appendix F writes out the maps of all nine r1 entries and runs the whole r1 interval with them.

Lemma J (the jump). Let a 4-cycle have shapes s_1, ..., s_4 and gap maps f_1, ..., f_4, and let f be their composite.

1. Translation. For each of the 12 cycles of Appendix B, f(h) = h + d: each long gap maps to itself plus its increment, and each small gap to its own value (check S7, composed symbolically). In particular f(h + d) = f(h) + d, so k cycles from h give h + k d, as long as the shapes hold.
2. Shapes in between. Inside cycle k, each of the four intermediate vectors is affine in k. Its slope is a sum of entries of d (the linear parts only add consecutive gaps), so it is a multiple of 4, and small gaps have slope 0. If the four shapes hold at k = 0 and at k = c - 1, then every long gap is at least 24 at both ends, hence at least 24 in between, with the same residue. So the shapes hold for every k from 0 to c - 1.
3. Count. When the cycle is found, R visits of the regime are left. The jump does c = (R - m)/4 cycles, with m = 4 + ((R - 4) mod 4) visits left for single entries (4 to 7). c is an integer and at least 1 for every u = 1 mod 8.

Uniformity in u. Write u = 1 + 8t with t >= 0. A gap a + bu then equals

(a + b)  +  8b t

In every vector of the run, 8b is an integer divisible by 4 and b >= 0. So the gap is an integer, its residue mod 4 is that at u = 1, and it is at least its value at u = 1. Hence every vector has the same shape for every u, and the choice of entries made at u = 1 holds for all u. The visit counts V1 and E are affine in u as well (5.2, with 3^K = 3^(K0 + 4) u).

Worked example. Appendix F runs class r1 step by step: the vector after each of the 20 single entries, the two cycles with their composites f(h1, 7, h3, h4, 3) = (h1, 7, h3, h4 + 36, 3) and f(h1, 8, h3, h4, 3) = (h1, 8, h3 - 4, h4 + 32, 3), their counts c, and the vectors at the first and the last jumped cycle.

5.4 Why X and Y stay in step with the counter

The X/Y synchronization is an exact cancellation. In this section w = 9^e = 81u; for example 24948w - 36 = 2020788u - 36.

Class r5 is an example. X is gap 4 of the Appendix B program.

• At the start of the interval, X = 3 V1 + 2 = (19683u - 11)/2 cells, where V1 = T(K) is the number of phase-(c_K + 2) visits.
• Each 4-cycle of those visits eats 12 cells of X: the first cycle runs as four single entries, then c = (6561u - 25)/8 cycles are jumped.
• So the u-terms cancel exactly. After the last jumped cycle

X = (19683u - 11)/2 - 12 - 12 (6561u - 25)/8 = 20

(and X = 32 at the start of that cycle). These are the 20 cells of entry r5.5 (shape L1 L3 8 20 L2), the entry that comes next. - The X-exhausted transient then runs inside the table (r5.5 r5.4 r5.3 r5.1 r5.7 r5.6 are the last phase-(c_K + 2) visits), and the old Y becomes a fossil of length 24948w - 36.

The other classes work the same way. The per-visit rates are the 4-cycle increments of Appendix B divided by 4:

These give X' = 3X + 8 and F' = 3F + 72 for the frozen blocks and the fossils (X_k = 6804 x 3^(k-4) - 4, F_j = 24948 x 3^j - 36), which matches the observed epoch laws.

6. The record step

Lemma S. From a record exit in C_r(e), the machine reaches the next record exit, without halting, in C_(r+1)(e). After r4 the next class is r5, with e + 1.

6.1 What happens at the record

• The 81st carry-out leaves the chain all D0 (Lemma T).
• The left episode 81 moves the left word 3 cells left and adds a digit at A - 1 (Lemma L81).
• The carry back sweeps the chain from left to right and turns every D0 block into D2 (Lemma C').

In D2 every defect has moved from its U0 place:

digit  -2      s1  +1      s2  +1      s3  +2        (D0: the same, but s3 +0)
digit  -2      separator +2                          (the m = 1 block)

6.2 The regrouping

The new parse groups the same defects one defect later:

new block j  =  (s3 of old block j ; digit, s1, s2 of old block j+1)

Under this shift each gap moves to the next role. Its value changes by the D2 offsets:

So every residue and every lower bound of (C) is preserved: digit gap >= 1 becomes >= 4, separator gaps stay >= 4, the second becomes an inter gap >= 5, and an inter gap >= 5 becomes a digit gap >= 1. At the left end, the new digit at A - 1 and the old first digit form the new m = 1 block (A'+2; A'+3) with A' = A - 3. The old m = 1 separator becomes the digit of the new block 2, at inter gap 5 from A.

6.3 The exchange at the right end

At the right end the chain gives defects to the right region, or takes some from it:

A chain of K blocks has 4K - 2 defects. With the new left digit and the exchange this gives 4K' - 2 in every step. Over one epoch K grows by 2 (the 6 new left digits plus 2 net defects from the right make 8 = 2 x 4).

The new record exit is the moment of (H) for the new end B'. Two cases, both decided by residues.

Defects leave the chain (r5 and r3 drop 1, r1 drops 5). The new last block is (old s3 of block j - 1; digit, s1, s2 of block j), with j = K for r5, r3 and j = K - 1 for r1. Its last defect is the old s2 of block j, which has the same place in D0 and D2 (+1). So B' lies inside the old chain.

• The carry back enters block j in D0 from the left at phase c_j + 2. By Appendix D its run is: pass the digit (d = 3), pass s1 (d = 2), pass s2 (d = 3), wiggle s3 (d = 1), pass s3 (d = 3).
• After the pass at s2 the head is on cell s2 + 1 = B' - 1 in state B reading 1, with phase c_j + 3.
• The new block's separators are the old digit, s1 and s2 of block j at their D2 places, all c_j + 1 mod 4. So c' = c_j + 1, and the phase c_j + 3 is c' + 2, as (H) requires.
• The defects that leave (s3 of block j, and for r1 all of block K) are not reached yet: they are still at their D0 places.

Defects join the chain (r0, r2, r4 take in x_1, x_2, x_3). The carry back turns the whole chain into D2 and leaves block K to the right at phase c_K (Lemma C', all D).

• The new last block is (old s3 of block K at its D2 place; x_1, x_2, x_3). Its base is b' = b_K + g3 + 2, which is c_K + 2 mod 4, so its phase is c' = c_K + 3.
• In all three classes the interval ends with E_1 = 1 and E_2 = E_3 = 0 mod 4 (Appendix B), and B = c_K + 2 mod 4. So x_1, x_2, x_3 are all c_K + 3 mod 4.
• Arriving at phase c_K, the head sees d = 3, 2, 3 at x_1, x_2, x_3: three passes, with phases c_K + 1, c_K, c_K + 1. The gaps around them are long, so no other defect is near.
• After the pass at x_3 the head is on cell x_3 + 1 = B' - 1 in state B reading 1, with phase c_K + 1 = c' + 2.

6.4 The window closes

Check S7 does the whole step symbolically in u:

1. the record-exit episode, using a Lemma R entry;
2. the interval, using sections 5.2 and 5.3 (the programs of Appendix B);
3. the record visit, using the D2/D0 offsets and the exchange.

For all six classes the result is exactly V_(r+1)(u); after r4 it is V_r5(9u). The chain gaps that leave the window for the deep chain have the residues and lower bounds of their roles.

The record-visit map. Write the window at the record exit as c_1, ..., c_J (the last J chain gaps, c_J ending at B - 2), and the right region at the end of the interval as E_1, ..., E_n (B -> x_1 -> ... -> hi, the end line of Appendix B). The record visit

• moves every chain defect that stays in the chain from its U0 place to its D2 place (digit -2, s1 +1, s2 +1, s3 +2),
• leaves every chain defect that leaves at its D0 place (the same, but s3 +0),
• leaves x_1, ..., x_n and hi where they are.

Reading the gaps from the new end B' gives, per class:

r5 -> r0 (drop 1): chain window (c1 + 3, c2) | right (c3 - 3, E1 + 2, E2, E3, E4, E5)
r0 -> r1 (take in 3): chain window (c1, c2 + 1, E1, E2, E3) | right (E4 - 2, E5, E6, E7, E8)
r1 -> r2 (drop 5): chain window (none) | right (c1 - 3, c2 - 2, c3 + 3, c4, c5 - 1, E1 + 2, E2, E3, E4, E5)
r2 -> r3 (take in 3): chain window (E3) | right (E4 - 2, E5, E6, E7, E8, E9, E10) | to the deep chain (E1, E2) as (digit gap, separator gap)
r3 -> r4 (drop 1): chain window (none) | right (c1 - 3, E1 + 2, E2, E3, E4, E5, E6, E7, E8)
r4 -> r5 (take in 3): chain window (E1, E2, E3) | right (E4 - 2, E5, E6, E7, E8, E9)

For example, r5 -> r0. The window has c_1 (digit gap), c_2, c_3 (separator gaps) of block K.

• The old s3 leaves at its D0 place (+0). The new chain ends at the old s2 (+1), so B' = old s2 + 3, and the first right gap is c_3 - 3.
• The next right gap runs from the old s3 to x_1 = B + E_1 = old s3 + 2 + E_1, so it is E_1 + 2.
• The chain gaps change as in 6.2: c_1 + 3 (digit -2 to s1 +1) and c_2 + 0 (s1 +1 to s2 +1).

Substituting V_r5(u) and the r5 end of Appendix B gives V_r0(u) entry by entry: c_1 + 3 = 8316u - 36, c_2 = 24948u - 36, c_3 - 3 = 74844u - 39, E_1 + 2 = 224532u - 37, and E_2, ..., E_5 unchanged. Check S7 evaluates all six lines in the same way.

In the take-in classes the gap from the old s3 (at +2) to x_1 = old s3 + 2 + E_1 is E_1, and the new end is B' = x_3 + 2, so the first right gap is E_4 - 2. At r2 -> r3 the gaps E_1 and E_2 leave the window for the deep chain as the digit gap and the first separator gap of the new last block; they are 8316u - 39 (1 mod 4, at least 1) and 24948u - 36 (0 mod 4, at least 4).

The window sizes J(r) are the smallest that let the window reproduce itself: a step that drops d defects needs J(r) at least d + J(r+1), and a step that takes in 3 needs J(r) at least J(r+1) - 3.

The same computation on exact numbers, with every one of the 81 x 3^K - 1 episodes run singly (no 4-cycle jumps):

• reproduces every next record exit from record exits 16-27, for each of 341, 512 and 588 (12/12 each);
• maps V_r(1) to V_(r+1)(1) and V_r(9) to V_(r+1)(9) at record exits 28-39 (up to 4,782,968 episodes per step).

7. Progress and halting

Progress. Lemma S is a finite run of at least one step.

• An interval has 81 x 3^K visits and as many episodes, plus 81 left episodes.
• In a visit each block takes part in at most two of the single-block runs of 4.1 (one leftward, one rightward), each of at most 8 events. A left episode has at most 31 events, and an episode is one table entry, a fixed finite run.

So from every record exit the machine reaches the next record exit in finitely many steps, and that next record exit is again in the invariant. The record exits never end, so the run is infinite.

Halting is unreachable. By 2.2 a halt needs a rightward head with d = 1 at a defect e with e + 1 also a defect, that is two defects at distance 1. After the base case every step lies in one of the following runs:

• a chain visit or carry back (Lemma C, C'), including the record visit: by Lemma B' it is a list of single-block runs, each of which is the run of Appendix D and does not halt (Lemma B, part 3);
• a left episode (Lemma L): a fixed finite run, checked without halt, alone and with the chain present; episode 81 is Lemma L81, whose six rightward d = 1 events all find e + 1 free;
• an episode (Lemma R): the base run of its entry, transferred to the actual gaps by 2.4; the base runs do not halt.

The regions never come close to each other: the left word ends at A - 4 and block 1's interval starts at A; block K's interval ends at B, and x_1, at least 24 cells right of B, is never touched. The one close pair across a region boundary is the new defect at A - 1 next to block 1's digit at A, during the record visit; Lemma L81 and Lemma B show that no rule ever tests or toggles it. The base case itself is a direct simulation of the table, which does not halt.

8. Base case and conclusion

Base case. The run from the blank tape reaches record exit 16 in C_r5(0) after 398,090,000 steps (line 512: 398,095,384 steps from its start; line 588: 397,796,108). Appendix C gives this configuration exactly. Check S10 compares it with direct simulation of each of the three machine strings, cell by cell.

Steps 16 -> 28. These are twelve concrete instances of Lemma S, on the exact numbers of Appendix C.

Record exit 28 onwards. At record exit 28 the window equals V_r5(1) for all three machines (step 2,629,088,227,408 for line 341). Section 6.4 closes Lemma S symbolically for every u, in all six classes.

The run itself agrees: record exits 28-33 of all three machines, and 34-39 of line 341, have exactly the windows V_r(1) and V_r(9).

Theorem. None of the three machines halts.

Proof. By induction over record exits, the configuration is in C_r(e) at every record exit n >= 16. Between two record exits every step lies in a run covered by Lemma C, C', L or R, or in the record visit of 6.1. None of these runs halts or collides (section 7). The three machines differ only in the deep part of the chain, where only residues and lower bounds matter, and in their base runs.

9. What is checked how

check_proof.py (machine directory; nice -n 10 python3 -B check_proof.py, about 2-3 minutes; --full adds the compressed-TM chain check, Lemma T up to K = 9, and more perturbations). Each line prints PASS or FAIL.

Points a referee should look at

• The window vectors V_r(u) were read off the run at e = 2 and e = 3. That is only how they were found. The proof is that the six symbolic steps close.
• The record visit: Lemma L81 (Appendix E), Lemma C' block by block, the residue derivation of the new record exit (6.3), and the explicit record-visit formulas (6.4).
• Lemma R and the single-block runs rest on the transfer lemma 2.4: one base run per entry, plus a free stretch in every gap that is varied.
• Lemma C for every K rests on Lemma B': the footprints of different blocks are disjoint, so a visit is a list of single-block runs.
• What is still only computed, not written out: the 81 base runs of Appendix A (up to 25 right-edge trips each) and the symbolic runs of the five classes other than r1 (Appendix B gives their programs, Appendix F shows r1 in full).

10. Lemma plan for a busycoq proof

The nearest template is kill #11 (1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, TM21 architecture from verify/SBCv6.v): macro rules on a digit list, one invariant INV, and a closure lemma step : INV s -> exists s', Kc s -->+ Kc s' /\ INV s', finished by multistep_nonhalt and progress_nonhalt_cond. Kill #3 (1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---) adds the per-step invariant J with a ghost phase and projected values p + Rt, q - Rt.

The correspondence:

New compared with both templates:

• the 81 right-region entries (Appendix A), each a finite run with the long gaps as variables;
• the left counter, which is the chain lemma on four m = 1 blocks plus a finite overflow run;
• the gaps kept as 4k + c with only residues and minimums known (the deep chain and the fossils);
• the long base case.

10.1 Layers

L0. Tape encoding and window lemmas. A configuration is 0inf, then the cells from the left blank zone to the right one, written as stretches between defects. A gap g = 4k + c is (1010)^k (or (0101)^k) plus a c-cell remainder. Lemmas:

• two shift rules over 4-cell units, B> (0101)^k --> (1010)^k B> (4k steps) and its leftward twin (shift_rule_R / shift_rule_L);
• the 8 defect rules of 2.2, each a 2- to 5-step es run;
• the turns on 0inf at both ends (the right-edge turn is the rightward d = 0 rule on the blank zone).

L1. Block lemmas. The 18 single-block runs of 4.1, quantified over the gaps (g1 = 4a + 1, separator gaps 4b, inter gap 4c + 1), composed from L0 with follow. The tight gaps (digit gap 1, inter gap 5) must be instances, so the remainders are written out and k >= 0. The event lists of Appendix D are the proof scripts; the footprints of Lemma B are what makes the list induction of L2 go through (Lemma B').

L2. Chain lemma. An inductive predicate for words of shape D^a [W] U^b over a block list, and Lemma C, C' by induction on the list. The exit phase is part of the statement. Lemma T is arithmetic on the word value.

L3. Left end. The left word is four m = 1 blocks plus the fixed defects A - 32 and A - 4 (4.2). Episodes 1-80 are Lemma C on that list; episode 81 adds one finite es run at the blank left end (Lemma L81, the 31 events of Appendix E). Alternatively, 81 finite es lemmas of fewer than 100 steps each.

L4. Right region. One lemma per Appendix A entry: R(gaps) -->+ R(gaps'), with every long gap a variable 4k + c, k >= 6. This layer has no template. It is mechanical: a script can emit each lemma and its proof from the entry's event list. In Coq the transfer lemma 2.4 is replaced by quantifying over k: every long gap is passed by a shift rule, and the free stretch of S6 is where that shift happens.

L5. The interval. A per-visit state (class, epoch, chain word, left counter, right gaps) and a per-visit invariant J in #3's style:

• the chain word is the one that Lemma T assigns to the visit number v;
• the right gaps are the Appendix B program evaluated at v: inside a 4-cycle, g0 + d x floor((v - v0)/4) plus the offset of the cycle position, which is #3's projected value;
• the deep chain keeps only residues and minimums.

Each macro step is one visit plus one episode, or a carry-out with its left episode, carry back and episode. The 4-cycles need no acceleration lemma in this form; the cycle count enters only through the affine formulas.

L6. Record step. Carry-out at all-D0, left episode 81, carry back to all-D2 (L2, L3). The regrouping and the exchange are tape equalities on the list (no steps), like #11's drop re-reading.

L7. Arithmetic. The window identities of 6.4 are affine in u = 9^(e-2) and close by lia after rewriting 3^K = 3^(K0 + 4) x u. Records 16-27 need their own concrete programs, or a weaker window (see L8).

L8. Base case. 398,090,000 steps is far beyond a direct es run (#3's 78,710-step init takes about 30 s). Two options:

• a verified interpreter: define the defect model on gap lists, prove once that one model event is a -->+ run of the table, and run the model by vm_compute from an early configuration (a few hundred thousand events to record exit 16);
• or start the induction earlier, with the left word as part of the invariant. That needs the start-up records 12-15, where the left word is still forming.

A verified interpreter would also discharge L1, L3 and the concrete steps 16-27 by computation. It is the recommended route: one simulation theorem, then all finite pieces by vm_compute, and only L2, L4 (symbolic gaps), L5 and L7 by hand.

10.2 Size and risk

• This is several stages of work: L0-L2 are about #11's size, L4 is 81 generated lemmas, L5 is about #3's J.
• Making the fossil gaps abstract (residue and minimum only, like the deep chain) may let the symbolic step start at e = 0 and remove the 12 concrete steps. This is not checked yet: with fits from e = 1, 2, five of six steps close and r4 -> r5 fails only on the first fossil, which is inert.
• The largest risk is L4's volume and the base case, not the mathematics.

10.3 How the plan was carried out (kill, 2026-10-12)

This machine is killed: 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---.v (2,583 lines, sha256 7bda36dc...3f4c) proves Lemma nonhalt : ~ halts tm c0., check_kill PASS, Print Assumptions closed. The public write-up (submission/proof.md, section 10 and the table "Where each section lives in the .v") maps every section here to its lemmas. The .v departs from the plan above at four points.

The closure lemma is inv_step : Inv s -> exists s', cfgI s -->+ cfgI s' /\ Inv s' (Lemma S per class: S_r5 .. S_r4), and nonhalt is multistep_nonhalt + progress_nonhalt_cond, as in TM21.

Siblings (740 lines 512 and 588). The nearest template for them is this kill file. Because Inv leaves the deep chain free, and all three starts have the window V_r5(1) at record exit 28 (section 8) and differ only in deep gaps, the plan is:

1. Copy the file verbatim. The table above becomes tmP; tm is the sibling string.
2. New base case: init28 from B;; tape0 (512) or F;; tape0 (588) to record exit 28 of that start (18,571,902 and 18,571,554 simulator steps), with the same window and new deep gaps nus28: 512 block 3 [10; 5; 4; 1] (ours [10; 5; 3; 1]); 588 block 2 [233; 8; 9; 8] (ours [242; 8; 9; 8]) and block 3 [12; 1; 0; 0].
3. nonhalt_P : ~ halts tmP (B;; tape0) (or F;; tape0) by progress_nonhalt_cond with the unchanged Inv, inv_step.
4. The conjugacy, by computation and busycoq: 512 perm_sib : Perm tm tmP phi, phi = A->B, B->C, C->D, D->E, E->A, F->F, then perm_halts (Permute.v); 588 perm_sib : Perm (flip tm) tmP phi, phi = A->F, B->A, C->B, D->C, E->D, F->E, then flip_halts (Flip.v) and perm_halts.

This is the pattern of #7 over #30 and #3b / #33b. Both sibling files exist and pass check_kill (one run each; their status.json files record the open re-verification).

Appendix A. The right-region table

One line per entry: id, exit phase class (2 = c_K + 2, 0 = c_K), shape (gaps B -> x_1 -> ... -> hi, Lc = long with residue c), the defects after the episode (x_i+o, hi+o = old defect plus offset), the new hi, and the counts of right-edge trips, turns inside the region and wiggles. Every entry returns at phase c_K.

class r5: 23 entries
r5.1   2 | L1 L3 7 13 L0 3                          | x1 x2 x3+1 x4-4                    | hi = hi+23   | trips 8, mid turns 5, wiggles 8
r5.2   2 | L1 L3 7 L1 L0 3                          | x1 x2 x3+1 x4-4                    | hi = hi+23   | trips 8, mid turns 5, wiggles 8
r5.3   2 | L1 L3 8 13 L1 3                          | x1 x2 x3-1 x4-1 hi+11              | hi = hi+14   | trips 5, mid turns 4, wiggles 4
r5.4   2 | L1 L3 8 18 L0 3                          | x1 x2 x3 x4-5 hi+25                | hi = hi+28   | trips 10, mid turns 5, wiggles 8
r5.5   2 | L1 L3 8 20 L2                            | x1 x2 x3 x4-2 hi+16                | hi = hi+19   | trips 7, mid turns 4, wiggles 5
r5.6   2 | L1 L3 8 6 L0 3                           | x1 x2 x3 x3+1 hi+25                | hi = hi+28   | trips 10, mid turns 5, wiggles 8
r5.7   2 | L1 L3 8 8 L2                             | x1 x2 x3 x4-2 hi+16                | hi = hi+19   | trips 7, mid turns 4, wiggles 5
r5.8   2 | L1 L3 8 L0 L2                            | x1 x2 x3 x4-2 hi+16                | hi = hi+19   | trips 7, mid turns 4, wiggles 5
r5.9   2 | L1 L3 8 L1 L1 3                          | x1 x2 x3-1 x4-1 hi+11              | hi = hi+14   | trips 5, mid turns 4, wiggles 4
r5.10  2 | L1 L3 8 L2 L0 3                          | x1 x2 x3 x4-5 hi+25                | hi = hi+28   | trips 10, mid turns 5, wiggles 8
r5.11  0 | L1 L0 L0 3 13 2                          | x1 x2 x3 x4+1 hi+3                 | hi = hi+6    | trips 2, mid turns 0, wiggles 2
r5.12  0 | L1 L0 L0 3 L1 2                          | x1 x2 x3 x4+1 hi+3                 | hi = hi+6    | trips 2, mid turns 0, wiggles 2
r5.13  0 | L1 L0 L0 4 11                            | x1 x2 x3 x4-1 hi+1                 | hi = hi+3    | trips 1, mid turns 1, wiggles 0
r5.14  0 | L1 L0 L0 4 17 3                          | x1 x2 x3 x4 x5+1                   | hi = hi      | trips 0, mid turns 1, wiggles 0
r5.15  0 | L1 L0 L0 4 18 2                          | x1 x2 x3 x4                        | hi = hi+3    | trips 1, mid turns 0, wiggles 1
r5.16  0 | L1 L0 L0 4 23                            | x1 x2 x3 x4-1 hi+1                 | hi = hi+3    | trips 1, mid turns 1, wiggles 0
r5.17  0 | L1 L0 L0 4 5 3                           | x1 x2 x3 x4 x5+1                   | hi = hi      | trips 0, mid turns 1, wiggles 0
r5.18  0 | L1 L0 L0 4 6 2                           | x1 x2 x3 x4                        | hi = hi+3    | trips 1, mid turns 0, wiggles 1
r5.19  0 | L1 L0 L0 4 L1 3                          | x1 x2 x3 x4 x5+1                   | hi = hi      | trips 0, mid turns 1, wiggles 0
r5.20  0 | L1 L0 L0 4 L2 2                          | x1 x2 x3 x4                        | hi = hi+3    | trips 1, mid turns 0, wiggles 1
r5.21  0 | L1 L0 L0 4 L3                            | x1 x2 x3 x4-1 hi+1                 | hi = hi+3    | trips 1, mid turns 1, wiggles 0
r5.22  0 | L1 L0 L0 5 2                             | x1 x2 x3 x4-1 hi+2                 | hi = hi+5    | trips 2, mid turns 0, wiggles 0
r5.23  0 | L1 L3 8 1 L1 3                           | x1 x2+1 x5-1 hi+1                  | hi = hi+3    | trips 1, mid turns 2, wiggles 1
class r0: 13 entries
r0.1   2 | L1 L3 L0 L0 3 L1 2                       | x1 x2 x3 x4 x5+1                   | hi = hi+9    | trips 3, mid turns 1, wiggles 4
r0.2   2 | L1 L3 L0 L0 4 L1 3                       | x1 x2 x3 x4 x5-1 hi+4              | hi = hi+6    | trips 2, mid turns 2, wiggles 2
r0.3   2 | L1 L3 L0 L0 4 L2 2                       | x1 x2 x3 x4 x5 hi+9                | hi = hi+12   | trips 4, mid turns 1, wiggles 4
r0.4   2 | L1 L3 L0 L0 4 L3                         | x1 x2 x3 x4 x5 hi+7                | hi = hi+9    | trips 3, mid turns 2, wiggles 3
r0.5   0 | L1 L0 L0 L3 4 L3                         | x1 x2 x3 x4 x5+3 hi-1 hi+4         | hi = hi+6    | trips 2, mid turns 2, wiggles 2
r0.6   0 | L1 L0 L0 L3 7 L0 15                      | x1 x2 x3 x4 x5 x6 hi+7             | hi = hi+9    | trips 3, mid turns 2, wiggles 3
r0.7   0 | L1 L0 L0 L3 7 L0 22 2                    | x1 x2 x3 x4 x5 x6 hi+9             | hi = hi+12   | trips 4, mid turns 1, wiggles 4
r0.8   0 | L1 L0 L0 L3 7 L0 L1 3                    | x1 x2 x3 x4 x5 x6-1 hi+4           | hi = hi+6    | trips 2, mid turns 2, wiggles 2
r0.9   0 | L1 L0 L0 L3 7 L0 L2 2                    | x1 x2 x3 x4 x5 x6 hi+9             | hi = hi+12   | trips 4, mid turns 1, wiggles 4
r0.10  0 | L1 L0 L0 L3 7 L0 L3                      | x1 x2 x3 x4 x5 x6 hi+7             | hi = hi+9    | trips 3, mid turns 2, wiggles 3
r0.11  0 | L1 L0 L0 L3 7 L3 5 2                     | x1 x2 x3 x4 x5 x6+1                | hi = hi+9    | trips 3, mid turns 1, wiggles 4
r0.12  0 | L1 L0 L0 L3 7 L3 L1 2                    | x1 x2 x3 x4 x5 x6+1                | hi = hi+9    | trips 3, mid turns 1, wiggles 4
r0.13  0 | L1 L3 L0 L0 3 L1 2                       | x1 x2+1 x3+1 x4 x5+1               | hi = hi+9    | trips 3, mid turns 2, wiggles 5
class r1: 9 entries
r1.1   2 | L1 7 L0 L1 3                             | x1 x2 x3-1 hi+4                    | hi = hi+6    | trips 2, mid turns 2, wiggles 2
r1.2   2 | L1 7 L0 L2 2                             | x1 x2 x3 hi+9                      | hi = hi+12   | trips 4, mid turns 1, wiggles 4
r1.3   2 | L1 7 L0 L3                               | x1 x2 x3 hi+7                      | hi = hi+9    | trips 3, mid turns 2, wiggles 3
r1.4   2 | L1 7 L3 L1 2                             | x1 x2 x3+1                         | hi = hi+9    | trips 3, mid turns 1, wiggles 4
r1.5   0 | L1 7 L0 L2 2                             | x1 x2+1 x3+2 hi+3                  | hi = hi+6    | trips 2, mid turns 1, wiggles 3
r1.6   0 | L1 7 L1 L0 3                             | x1 x2+1 x3-3 hi+11                 | hi = hi+14   | trips 5, mid turns 2, wiggles 4
r1.7   0 | L1 8 L0 L2                               | x1 x2-1 x3 hi+2                    | hi = hi+5    | trips 2, mid turns 1, wiggles 0
r1.8   0 | L1 8 L1 L1 3                             | x1 x2 x3+1 x4                      | hi = hi      | trips 0, mid turns 1, wiggles 0
r1.9   0 | L1 8 L2 L0 3                             | x1 x2 x3-2                         | hi = hi+9    | trips 3, mid turns 2, wiggles 3
class r2: 13 entries
r2.1   2 | L1 L3 L0 L0 L3 L3 7 L1 L0 3              | x1 x2 x3 x4 x5 x6 x7+1 x8-11 hi+67 | hi = hi+70   | trips 25, mid turns 14, wiggles 22
r2.2   2 | L1 L3 L0 L0 L3 L3 8 20 L2                | x1 x2 x3 x4 x5 x6 x7-1 x8-8 hi+58  | hi = hi+61   | trips 22, mid turns 13, wiggles 18
r2.3   2 | L1 L3 L0 L0 L3 L3 8 L0 L2                | x1 x2 x3 x4 x5 x6 x7-1 x8-8 hi+58  | hi = hi+61   | trips 22, mid turns 13, wiggles 18
r2.4   2 | L1 L3 L0 L0 L3 L3 8 L1 L1 3              | x1 x2 x3 x4 x5 x6 x7 x8-7 hi+53    | hi = hi+56   | trips 20, mid turns 13, wiggles 18
r2.5   2 | L1 L3 L0 L0 L3 L3 8 L2 L0 3              | x1 x2 x3 x4 x5 x6 x7 x8-10         | hi = hi+65   | trips 23, mid turns 14, wiggles 21
r2.6   0 | L1 L0 L0 L3 L3 L0 L0 3 L1 2              | x1 x2 x3 x4 x5 x6 x7 x8+1          | hi = hi+9    | trips 3, mid turns 1, wiggles 4
r2.7   0 | L1 L0 L0 L3 L3 L0 L0 4 17 3              | x1 x2 x3 x4 x5 x6 x7 x8-1 hi+4     | hi = hi+6    | trips 2, mid turns 2, wiggles 2
r2.8   0 | L1 L0 L0 L3 L3 L0 L0 4 6 2               | x1 x2 x3 x4 x5 x6 x7 x8 hi+9       | hi = hi+12   | trips 4, mid turns 1, wiggles 4
r2.9   0 | L1 L0 L0 L3 L3 L0 L0 4 L1 3              | x1 x2 x3 x4 x5 x6 x7 x8-1 hi+4     | hi = hi+6    | trips 2, mid turns 2, wiggles 2
r2.10  0 | L1 L0 L0 L3 L3 L0 L0 4 L2 2              | x1 x2 x3 x4 x5 x6 x7 x8 hi+9       | hi = hi+12   | trips 4, mid turns 1, wiggles 4
r2.11  0 | L1 L0 L0 L3 L3 L0 L0 4 L3                | x1 x2 x3 x4 x5 x6 x7 x8 hi+7       | hi = hi+9    | trips 3, mid turns 2, wiggles 3
r2.12  0 | L1 L0 L0 L3 L3 L3 8 1 L1 3               | x1 x2 x3 x4 x5 x6+1 x9-1 hi hi+6   | hi = hi+8    | trips 3, mid turns 3, wiggles 2
r2.13  0 | L1 L3 L0 L0 L3 L3 7 13 L0 3              | x1 x2+1 x3+1 x4 x5 x6 x7+1 x7+2 hi+67 | hi = hi+70   | trips 25, mid turns 15, wiggles 23
class r3: 13 entries
r3.1   2 | L1 L3 L0 L0 3 L1 2                       | x1 x2 x3 x4 x5+1                   | hi = hi+9    | trips 3, mid turns 1, wiggles 4
r3.2   2 | L1 L3 L0 L0 4 L1 3                       | x1 x2 x3 x4 x5-1 hi+4              | hi = hi+6    | trips 2, mid turns 2, wiggles 2
r3.3   2 | L1 L3 L0 L0 4 L2 2                       | x1 x2 x3 x4 x5 hi+9                | hi = hi+12   | trips 4, mid turns 1, wiggles 4
r3.4   2 | L1 L3 L0 L0 4 L3                         | x1 x2 x3 x4 x5 hi+7                | hi = hi+9    | trips 3, mid turns 2, wiggles 3
r3.5   0 | L1 L0 L0 L3 4 L3                         | x1 x2 x3 x4 x5+3 hi-1 hi+4         | hi = hi+6    | trips 2, mid turns 2, wiggles 2
r3.6   0 | L1 L0 L0 L3 7 L0 15                      | x1 x2 x3 x4 x5 x6 hi+7             | hi = hi+9    | trips 3, mid turns 2, wiggles 3
r3.7   0 | L1 L0 L0 L3 7 L0 22 2                    | x1 x2 x3 x4 x5 x6 hi+9             | hi = hi+12   | trips 4, mid turns 1, wiggles 4
r3.8   0 | L1 L0 L0 L3 7 L0 L1 3                    | x1 x2 x3 x4 x5 x6-1 hi+4           | hi = hi+6    | trips 2, mid turns 2, wiggles 2
r3.9   0 | L1 L0 L0 L3 7 L0 L2 2                    | x1 x2 x3 x4 x5 x6 hi+9             | hi = hi+12   | trips 4, mid turns 1, wiggles 4
r3.10  0 | L1 L0 L0 L3 7 L0 L3                      | x1 x2 x3 x4 x5 x6 hi+7             | hi = hi+9    | trips 3, mid turns 2, wiggles 3
r3.11  0 | L1 L0 L0 L3 7 L3 5 2                     | x1 x2 x3 x4 x5 x6+1                | hi = hi+9    | trips 3, mid turns 1, wiggles 4
r3.12  0 | L1 L0 L0 L3 7 L3 L1 2                    | x1 x2 x3 x4 x5 x6+1                | hi = hi+9    | trips 3, mid turns 1, wiggles 4
r3.13  0 | L1 L3 L0 L0 3 L1 2                       | x1 x2+1 x3+1 x4 x5+1               | hi = hi+9    | trips 3, mid turns 2, wiggles 5
class r4: 10 entries
r4.1   2 | L1 L3 L0 L0 L3 7 L0 L1 3                 | x1 x2 x3 x4 x5 x6 x7 hi+22         | hi = hi+24   | trips 8, mid turns 5, wiggles 10
r4.2   2 | L1 L3 L0 L0 L3 7 L0 L2 2                 | x1 x2 x3 x4 x5 x6 x7               | hi = hi+27   | trips 9, mid turns 4, wiggles 11
r4.3   2 | L1 L3 L0 L0 L3 7 L0 L3                   | x1 x2 x3 x4 x5 x6 x7-1 hi+25       | hi = hi+27   | trips 9, mid turns 5, wiggles 10
r4.4   2 | L1 L3 L0 L0 L3 7 L3 L1 2                 | x1 x2 x3 x4 x5 x6 x7+1 hi+27       | hi = hi+30   | trips 10, mid turns 4, wiggles 12
r4.5   0 | L1 L0 L0 L3 L3 7 L0 L2 2                 | x1 x2 x3 x4 x5 x6+1 x7+1           | hi = hi+15   | trips 5, mid turns 4, wiggles 7
r4.6   0 | L1 L0 L0 L3 L3 7 L1 L0 3                 | x1 x2 x3 x4 x5 x6+1 x7-4           | hi = hi+23   | trips 8, mid turns 5, wiggles 8
r4.7   0 | L1 L0 L0 L3 L3 8 L0 L2                   | x1 x2 x3 x4 x5 x6 x7-2 hi+16       | hi = hi+19   | trips 7, mid turns 4, wiggles 5
r4.8   0 | L1 L0 L0 L3 L3 8 L1 L1 3                 | x1 x2 x3 x4 x5 x6-1 x7-1 hi+11     | hi = hi+14   | trips 5, mid turns 4, wiggles 4
r4.9   0 | L1 L0 L0 L3 L3 8 L2 L0 3                 | x1 x2 x3 x4 x5 x6 x7-5 hi+25       | hi = hi+28   | trips 10, mid turns 5, wiggles 8
r4.10  0 | L1 L3 L0 L0 L3 7 L0 L1 3                 | x1 x2+1 x3+1 x4 x5 x6 x7 hi+22     | hi = hi+24   | trips 8, mid turns 6, wiggles 11

Appendix B. The interval programs

For each class: the right region after the record-exit episode (at record exit e = 2 + log_9 u), the entries run one by one (single), the 4-cycles with their repeat counts and increments (gap i = the i-th gap from B), and the right region at the end of the interval, before the record visit.

class r5: start  224532u-39, 673596u-37, 8, (19683u-11)/2, 1942056u+14
   single: r5.8 r5.10 r5.9 r5.2
   cycle (r5.8 r5.10 r5.9 r5.2) x (6561u-25)/8: gap 4 -12, gap 5 +96; 30 trips per cycle
   single: r5.5 r5.4 r5.3 r5.1 r5.7 r5.6 r5.23 r5.22 r5.17 r5.18 r5.13 r5.11 r5.14 r5.15 r5.16 r5.12 r5.19 r5.20 r5.21
   cycle (r5.12 r5.19 r5.20 r5.21) x (347733u-37)/8: gap 5 +12; 4 trips per cycle
   single: r5.12 r5.19 r5.20 r5.21 r5.12 r5.19 r5.20
   end    224532u-39, 673596u-36, 2020788u-36, 4, (1043199u+7)/2
class r0: start  74844u-39, 224532u-37, 673596u-36, 2020788u-36, 4, (1043199u+21)/2, 2
   single: r0.3 r0.2 r0.1 r0.4
   cycle (r0.3 r0.2 r0.1 r0.4) x (6561u-25)/8: gap 6 +36; 12 trips per cycle
   single: r0.3 r0.2 r0.1 r0.4 r0.3 r0.2 r0.13 r0.5 r0.11 r0.6 r0.7 r0.8 r0.12 r0.10 r0.9
   cycle (r0.8 r0.12 r0.10 r0.9) x (347733u-29)/8: gap 7 +36; 12 trips per cycle
   single: r0.8 r0.12 r0.10 r0.9 r0.8 r0.12 r0.10
   end    74844u-39, 224532u-36, 673596u-36, 2020788u-37, 7, 551124u-4, (3129597u-1)/2, 2
class r1: start  2020788u-39, 7, 551124u-4, (3129597u+21)/2, 3
   single: r1.1 r1.4 r1.3 r1.2
   cycle (r1.1 r1.4 r1.3 r1.2) x (19683u-27)/8: gap 4 +36; 12 trips per cycle
   single: r1.1 r1.4 r1.3 r1.2 r1.1 r1.4 r1.3 r1.5 r1.8 r1.9 r1.7 r1.6
   cycle (r1.8 r1.9 r1.7 r1.6) x (1043199u-15)/8: gap 3 -4, gap 4 +32; 10 trips per cycle
   single: r1.8 r1.9 r1.7 r1.6
   end    2020788u-39, 8, (59049u-7)/2, 5826168u-7, 3
class r2: start  8316u-39, 24948u-37, 74844u-36, 224532u-36, 673596u-37, 2020788u-37, 8, (59049u-21)/2, 5826168u+56, 3
   single: r2.5 r2.3 r2.1 r2.4
   cycle (r2.5 r2.3 r2.1 r2.4) x (6561u-25)/8: gap 8 -36, gap 9 +288; 90 trips per cycle
   single: r2.5 r2.3 r2.1 r2.4 r2.5 r2.2 r2.13 r2.12 r2.8 r2.7 r2.6 r2.11 r2.10 r2.9
   cycle (r2.6 r2.11 r2.10 r2.9) x (347733u-21)/8: gap 9 +36; 12 trips per cycle
   single: r2.6 r2.11 r2.10 r2.9
   end    8316u-39, 24948u-36, 74844u-36, 224532u-37, 673596u-37, 2020788u-36, 6062364u-36, 3, (3129597u+5)/2, 2
class r3: start  224532u-39, 673596u-37, 2020788u-36, 6062364u-36, 4, (3129597u+25)/2
   single: r3.4 r3.3 r3.2 r3.1
   cycle (r3.4 r3.3 r3.2 r3.1) x (19683u-27)/8: gap 6 +36; 12 trips per cycle
   single: r3.4 r3.3 r3.2 r3.1 r3.4 r3.3 r3.2 r3.13 r3.5 r3.11 r3.6 r3.7 r3.8 r3.12 r3.10 r3.9
   cycle (r3.8 r3.12 r3.10 r3.9) x (1043199u-23)/8: gap 7 +36; 12 trips per cycle
   single: r3.8 r3.12 r3.10 r3.9
   end    224532u-39, 673596u-36, 2020788u-36, 6062364u-37, 7, 1653372u-4, (9388791u+3)/2, 3
class r4: start  74844u-39, 224532u-37, 673596u-36, 2020788u-36, 6062364u-37, 7, 1653372u-4, (9388791u+53)/2, 2
   single: r4.2 r4.3 r4.4 r4.1
   cycle (r4.2 r4.3 r4.4 r4.1) x (19683u-27)/8: gap 8 +108; 36 trips per cycle
   single: r4.2 r4.3 r4.4 r4.1 r4.2 r4.3 r4.4 r4.10 r4.5 r4.7 r4.9 r4.8 r4.6
   cycle (r4.7 r4.9 r4.8 r4.6) x (1043199u-23)/8: gap 7 -12, gap 8 +96; 30 trips per cycle
   single: r4.7 r4.9 r4.8 r4.6 r4.7 r4.9 r4.8
   end    74844u-39, 224532u-36, 673596u-36, 2020788u-37, 6062364u-37, 7, (177147u-1)/2, 17478504u-16, 3

Appendix C. The base configuration and the start-up windows

Record exit 16 of line 341, step 398,090,000.

head  : state B on cell 1154, which holds 1 (moving right)
tape  : 0 outside cells -55 .. 36257; cell -55 holds 1;
        for -55 <= x < 36257, cells x and x+1 are equal exactly when x is one of
        -54 -49 -48 -43 -42 -37 -36 -31 -30 -26   -20 -19   -10 3 27 71   108 145 181
        3888 12167 12174 12295 36255

In the defect frame of 2.1 this is:

• A = -22, lo = -56 = A - 34, and the left word W_1;
• the chain (-20; -19), (-10; 3, 27, 71), (108; 145, 181, 1153), all U0, B = 1155, K = 3;
• the right region x = 3888, 12167, 12174, 12295, 36255 and hi = 36258;
• the head at phase 3 = c_K + 2 (c_K = 1).

Edge 1153 is the last separator, B - 2. The head has just crossed it, so the current tape no longer shows it (cells 1153 and 1154 differ), while the defect frame still counts it. This is (H): the head is on cell B - 1 = 1154 in state B, reading 1. By the operational definition of 3.3 this is the first configuration after record 16 (steps 398,088,768-770) with the head in state B reading 1 and 10 + 4K - 2 = 20 pre-sweep defects in (lo, h - 1].

Windows at record exits 16-27 (line 341). Record exit, class, K, the last J(r) chain gaps, and the right region.

16 r5 K=3 | 37, 36, 972 | 2733, 8279, 7, 121, 23960, 3
17 r0 K=3 | 40, 36 | 969, 2735, 8280, 24912, 4, 6443
18 r1 K=4 | 40, 37, 969, 2736, 8280 | 24909, 7, 6800, 19318, 2
19 r2 K=3 | - | 37, 35, 972, 2736, 8279, 24911, 8, 361, 71921, 3
20 r3 K=4 | 972 | 2733, 8279, 24912, 74808, 3, 19321, 2
21 r4 K=4 | - | 969, 2735, 8280, 24912, 74807, 7, 20408, 57957, 3
22 r5 K=5 | 969, 2736, 8280 | 24909, 74807, 7, 1093, 215768, 3
23 r0 K=5 | 972, 2736 | 8277, 24911, 74808, 224496, 4, 57959
24 r1 K=6 | 972, 2737, 8277, 24912, 74808 | 224493, 7, 61232, 173866, 2
25 r2 K=5 | - | 969, 2735, 8280, 24912, 74807, 224495, 8, 3277, 647345, 3
26 r3 K=6 | 8280 | 24909, 74807, 224496, 673560, 3, 173869, 2
27 r4 K=6 | - | 8277, 24911, 74808, 224496, 673559, 7, 183704, 521601, 3

Lines 512 and 588 have their own start-up windows at 16-27 (check S7 runs their concrete steps) and the same windows V_r(1) from record exit 28 on.

Appendix D. The single-block runs

One line per run of the table in 4.1: m, state, entry side and phase (relative to the block's c), exit side, phase change and new state, then the events in order. Each event is the direction, the defect (dg = digit, s1-s3 = separators, sp = the m = 1 separator), d, and the rule of 2.2 ("turn" for a reversal, "wiggle" for the d = 1 rule). After a wiggle the moved defect is met again at once, with d = 3. The lists are the same for every gap choice (Lemma B).

m=3 U0 right c+0 -> right +2 U1 | L s3 d=0 pass, L s2 d=3 pass, L s1 d=0 pass, L dg d=2 turn, R s1 d=3 pass, R s2 d=2 pass, R s3 d=3 pass
m=3 U1 right c+0 -> right +2 U2 | L s3 d=0 pass, L s2 d=3 pass, L s1 d=0 pass, L dg d=1 turn, R s1 d=3 pass, R s2 d=2 pass, R s3 d=3 pass
m=3 U2 right c+0 -> left  +2 U2 | L s3 d=0 pass, L s2 d=3 pass, L s1 d=0 pass, L dg d=0 pass
m=3 W0 right c+0 -> right +2 W1 | L s3 d=0 pass, L s2 d=2 turn, R s3 d=3 pass
m=3 W1 right c+0 -> right +2 D0 | L s3 d=0 pass, L s2 d=1 turn, R s3 d=3 pass
m=3 D0 right c+0 -> left  +2 D0 | L s3 d=0 pass, L s2 d=0 pass, L s1 d=3 pass, L dg d=0 pass
m=3 D1 right c+0 -> right +0 D0 | L s3 d=1 turn
m=3 D2 right c+0 -> right +0 D1 | L s3 d=2 turn
m=3 U2 left  c+0 -> right +2 U0 | R dg d=1 wiggle, R dg d=3 pass, R s1 d=3 pass, R s2 d=2 pass, R s3 d=3 pass
m=3 U2 left  c+2 -> right +0 W0 | R dg d=3 pass, R s1 d=1 wiggle, R s1 d=3 pass, R s2 d=0 turn, L s1 d=2 turn, R s2 d=1 wiggle, R s2 d=3 pass, R s3 d=3 pass
m=3 D0 left  c+2 -> right +2 D2 | R dg d=3 pass, R s1 d=2 pass, R s2 d=3 pass, R s3 d=1 wiggle, R s3 d=3 pass
m=1 U0 right c+0 -> right +2 U1 | L sp d=0 pass, L dg d=2 turn, R sp d=3 pass
m=1 U1 right c+0 -> right +2 D0 | L sp d=0 pass, L dg d=1 turn, R sp d=3 pass
m=1 D0 right c+0 -> left  +2 D0 | L sp d=0 pass, L dg d=0 pass
m=1 D1 right c+0 -> right +0 D0 | L sp d=1 turn
m=1 D2 right c+0 -> right +0 D1 | L sp d=2 turn
m=1 D0 left  c+0 -> right +2 U0 | R dg d=1 wiggle, R dg d=3 pass, R sp d=3 pass
m=1 D0 left  c+2 -> right +2 D2 | R dg d=3 pass, R sp d=1 wiggle, R sp d=3 pass

Appendix E. Left episode 81

Lemma L81, event by event, with the chain all D0 (block 1 at (A; A+3)). The head starts moving left, about to read cell A - 1, at phase 1 relative to A. Positions are relative to A; lo = A - 34 at the start.

  1  L  A-4    d=3  pass
  2  L  A-8    d=0  pass
  3  L  A-11   d=0  pass
  4  L  A-14   d=0  pass
  5  L  A-17   d=0  pass
  6  L  A-20   d=0  pass
  7  L  A-23   d=0  pass
  8  L  A-26   d=0  pass
  9  L  A-29   d=0  pass
 10  L  A-32   d=0  pass
 11  L  A-35   d=0  pass
 12  L  A-36   d=2  turn at the blank end: lo A-34 -> A-37, A-35 is now a defect
 13  R  A-35   d=3  pass
 14  R  A-32   d=1  wiggle: A-32 -> A-30 (e+1 = A-31 is no defect)
 15  R  A-30   d=3  pass
 16  R  A-29   d=3  pass
 17  R  A-26   d=1  wiggle: A-26 -> A-24 (e+1 = A-25 is no defect)
 18  R  A-24   d=3  pass
 19  R  A-23   d=3  pass
 20  R  A-20   d=1  wiggle: A-20 -> A-18 (e+1 = A-19 is no defect)
 21  R  A-18   d=3  pass
 22  R  A-17   d=3  pass
 23  R  A-14   d=1  wiggle: A-14 -> A-12 (e+1 = A-13 is no defect)
 24  R  A-12   d=3  pass
 25  R  A-11   d=3  pass
 26  R  A-8    d=1  wiggle: A-8 -> A-6 (e+1 = A-7 is no defect)
 27  R  A-6    d=3  pass
 28  R  A-4    d=0  turn: A-4 -> A-3
 29  L  A-6    d=2  turn: A-6 -> A-7
 30  R  A-3    d=1  wiggle: A-3 -> A-1 (e+1 = A-2 is no defect)
 31  R  A-1    d=3  pass

After event 31 the head is on cell A, moving right at phase 1 relative to A, and its next defect is block 1's digit at A (d = 3). The left defects are W_1 - 3 plus A - 1, and lo = A - 37.

Appendix F. The interval of class r1, worked out

Gap maps. One line per r1 entry: the gap vector of its shape (long gaps as variables g_i, small gaps as their exact values) and its image. Each new gap is a sum of consecutive old gaps plus a constant, read off Appendix A.

r1.1   (g1, 7, g3, g4, 3) -> (g1, 7, g3 - 1, g4 + 8, 2)
r1.2   (g1, 7, g3, g4, 2) -> (g1, 7, g3, g4 + 11, 3)
r1.3   (g1, 7, g3, g4) -> (g1, 7, g3, g4 + 7, 2)
r1.4   (g1, 7, g3, g4, 2) -> (g1, 7, g3 + 1, g4 + 10)
r1.5   (g1, 7, g3, g4, 2) -> (g1, 8, g3 + 1, g4 + 3, 3)
r1.6   (g1, 7, g3, g4, 3) -> (g1, 8, g3 - 4, g4 + 17, 3)
r1.7   (g1, 8, g3, g4) -> (g1, 7, g3 + 1, g4 + 2, 3)
r1.8   (g1, 8, g3, g4, 3) -> (g1, 8, g3 + 1, g4 - 1, 3)
r1.9   (g1, 8, g3, g4, 3) -> (g1, 8, g3 - 2, g4 + 14)

The run, symbolically in u. start is the right region after the record-exit episode (entry r1.2 applied to V_r1). Each entry line gives the entry, its exit phase class (ph 2 = c_K + 2, ph 0 = c_K), the gap vector after it, and the visits R of the regime still to run. The first regime has V1 = (19683u - 5)/2 visits, the second E - V1 = (1043199u + 3)/2.

For each cycle: its composite f (Lemma J), the visits left, the count c, and the vector at the start of the first and of the last jumped cycle. All long gaps there are at least 24 for every u >= 1, so the four shapes hold throughout the jump.

start        2020788u-39, 7, 551124u-4, (3129597u+21)/2, 3
r1.1   ph 2  2020788u-39, 7, 551124u-5, (3129597u+37)/2, 2   (R = (19683u-7)/2)
r1.4   ph 2  2020788u-39, 7, 551124u-4, (3129597u+57)/2   (R = (19683u-9)/2)
r1.3   ph 2  2020788u-39, 7, 551124u-4, (3129597u+71)/2, 2   (R = (19683u-11)/2)
r1.2   ph 2  2020788u-39, 7, 551124u-4, (3129597u+93)/2, 3   (R = (19683u-13)/2)
cycle (r1.1 r1.4 r1.3 r1.2): f(h1, 7, h3, h4, 3) = (h1, 7, h3, h4 + 36, 3)
   R = (19683u-13)/2 visits left; c = (R - m)/4 = (19683u-27)/8 cycles, m = 7 visits left after
   first jumped cycle starts at 2020788u-39, 7, 551124u-4, (3129597u+93)/2, 3
   last jumped cycle starts at  2020788u-39, 7, 551124u-4, 1653372u-111, 3
   after the jump               2020788u-39, 7, 551124u-4, 1653372u-75, 3   (R = 7)
r1.1   ph 2  2020788u-39, 7, 551124u-5, 1653372u-67, 2   (R = 6)
r1.4   ph 2  2020788u-39, 7, 551124u-4, 1653372u-57   (R = 5)
r1.3   ph 2  2020788u-39, 7, 551124u-4, 1653372u-50, 2   (R = 4)
r1.2   ph 2  2020788u-39, 7, 551124u-4, 1653372u-39, 3   (R = 3)
r1.1   ph 2  2020788u-39, 7, 551124u-5, 1653372u-31, 2   (R = 2)
r1.4   ph 2  2020788u-39, 7, 551124u-4, 1653372u-21   (R = 1)
r1.3   ph 2  2020788u-39, 7, 551124u-4, 1653372u-14, 2   (R = 0)
r1.5   ph 0  2020788u-39, 8, 551124u-3, 1653372u-11, 3   (R = (1043199u+1)/2)
r1.8   ph 0  2020788u-39, 8, 551124u-2, 1653372u-12, 3   (R = (1043199u-1)/2)
r1.9   ph 0  2020788u-39, 8, 551124u-4, 1653372u+2   (R = (1043199u-3)/2)
r1.7   ph 0  2020788u-39, 7, 551124u-3, 1653372u+4, 3   (R = (1043199u-5)/2)
r1.6   ph 0  2020788u-39, 8, 551124u-7, 1653372u+21, 3   (R = (1043199u-7)/2)
cycle (r1.8 r1.9 r1.7 r1.6): f(h1, 8, h3, h4, 3) = (h1, 8, h3 - 4, h4 + 32, 3)
   R = (1043199u-7)/2 visits left; c = (R - m)/4 = (1043199u-15)/8 cycles, m = 4 visits left after
   first jumped cycle starts at 2020788u-39, 8, 551124u-7, 1653372u+21, 3
   last jumped cycle starts at  2020788u-39, 8, (59049u+9)/2, 5826168u-71, 3
   after the jump               2020788u-39, 8, (59049u+1)/2, 5826168u-39, 3   (R = 4)
r1.8   ph 0  2020788u-39, 8, (59049u+3)/2, 5826168u-40, 3   (R = 3)
r1.9   ph 0  2020788u-39, 8, (59049u-1)/2, 5826168u-26   (R = 2)
r1.7   ph 0  2020788u-39, 7, (59049u+1)/2, 5826168u-24, 3   (R = 1)
r1.6   ph 0  2020788u-39, 8, (59049u-7)/2, 5826168u-7, 3   (R = 0)
end          2020788u-39, 8, (59049u-7)/2, 5826168u-7, 3

The end vector equals the end line of Appendix B, and 6.4 maps it to V_r2(u).

Review log

• 2026-10-12, close-out stage 3. First version: invariant C_r(e), Lemmas C, C', T, L, R, S, base case, check table.
• 2026-10-12, completion pass (this version).
• Added: the derivation of the eight rules (2.2), the single-block table (4.1), the closed form of the left counter (4.2), the interval programs (5.3, Appendix B), the right table (Appendix A), progress and halting (section 7), the exact base configuration and start-up windows (Appendix C), and the lemma plan (section 10).
• Added check_proof.py, which re-checks every claim; the checks of the earlier stages remain in scripts/.
• Corrected: 5.3 said that a jump needs every changing gap to stay at least 64 at both ends. The actual condition is at least 24 at every jumped episode; it is now verified independently of the stage-2 code (linear part and end-point shapes).
• Corrected: the 5.4 table omitted that Y grows 24 (r5) and 72 (r2) per visit in the first regime.
• Strengthened: Lemma C and C' are now checked on the exact defect model, not only on the compressed defect TM; the base case is compared with direct simulation of all three machine strings, cell by cell.
• Open for a referee: the composition step of Lemma C (residues decide, collisions are local), the residue argument behind Lemma R for gaps above the minimum, and the defect frame bookkeeping of 2.1 are argued in prose and checked on finite families, not derived symbolically.
• 2026-10-12, review pass 1. A referee read found the proof sound, with six minor gaps. All are fixed.
• Transfer lemma 2.4 added: inserting 4j cells into a stretch that never holds a defect keeps every event.
• Lemma R (4.3): the proof is now one base run per entry plus a free stretch of at least 11 edges in every long gap (check S6), in place of the shrink-bound prose. The shrink bound stays as a cross-check.
• Interval (5.3): Lemma J with the gap maps, the cycle composites f(h) = h + d (all 12 cycles composed symbolically, S7), the residue argument for the shapes inside a jump, and uniformity in u through u = 1 + 8t. Appendix F works out class r1 entry by entry.
• Record visit (6.3, 6.4): explicit formulas End -> V_(r+1) for every class, checked in S7, with r5 -> r0 worked by hand. The new record exit is derived by residues in both cases: inside block j's D0 -> D2 run when defects leave, and x_1, x_2, x_3 passed with d = 3, 2, 3 when they join.
• Episode 81 (4.2): Lemma L81 with input, output and all 31 events (Appendix E). The new defect at A - 1 comes from a wiggle at A - 3 and is passed with d = 3; the head ends on cell A at phase c_1 + 2, the entry of Lemma C'.
• Record exit (3.3): (H) now fixes the cell level (head on cell B - 1 in state B reading 1; edge B - 2 a defect only in the pre-sweep frame), gives B = (4K - 2)-th defect from A, plus 2, and an operational definition. S10 checks it at every snapshot and finds record exit 16 of all three strings by it on the direct simulation.
• Record numbering (3.1): only the 3-cell moves of λ are numbered; the start-up moves are listed; record 16 is at steps 398,088,768-770; line 588 has one extra start-up record.
• Lemma C (4.1): Lemma B (event lists, footprints, no halt) and Lemma B' (disjoint footprints, so a visit is a list of single-block runs); Appendix D lists the 18 event lists. The exhaustive tight-gap check is now a cross-check.
• 5.4: "X is down to 32 cells when the cycles end" corrected to 20 after the last jumped cycle (32 at its start), and w = 9^e = 81u defined.
• 2026-10-12, Class 2 close-out, invariant stage (dispatched after the kill).
• Every part the stage asked for was already here (table, rules, invariant, progress, halting, exact start, lemma plan, review log). Nothing in sections 1-9 or the appendices changed.
• Added: the status line under the header, and section 10.3. It records where the .v followed the plan of 10.1 and where it took another route (run-length simulator of tm, symbolic episodes, one interval invariant Inv with a free deep chain, base case at record exit 28). It also gives the sibling plan (this kill file with the table as tmP, new init28 / nus28, perm_halts, flip_halts), with the lemma names, phi maps and deep-gap differences taken from the three .v files.
• check_proof.py re-run after the edit: 68/68 claims PASS, 158 s (check_proof.out).
• Checkpoint B (Dennis): pending, non-blocking.