1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---: never halts

This machine never halts. Between two blank ends, its tape is an alternating pattern ...0101... with a few exceptions, and the head sweeps back and forth across it. The exceptions are defects, places where two neighbouring cells are equal.

A sweep complements every cell it crosses, which keeps every defect where it is. So the defect pattern changes only when the head meets a defect.

The defects form a counter in base 3. A small word at the left end counts to 81. A chain of digit blocks in the middle counts the head's visits. Two growing blocks at the right end keep pace with the chain.

Every 81 x 3^K visits the left word overflows, the chain is regrouped, and the right end starts the next of six phases. After six phases the picture repeats with two more digits.

The long blocks have lengths affine in a scale u, and six phases take u to 9u. So a long block grows by a factor close to 9, but not exactly 9: for example 74844u - 36 becomes 673596u - 36.

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

Machine and status

• Machine: 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---, viewer https://bbchallenge.org/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---
• Holdout: on the current BB(6) holdout list, class "Skelet 1-like Class 2".
• Written for: the string itself, with no mirror or state renaming. The same table started in two other states gives two more holdouts (section 9). This .v does not cover them; each has its own file and write-up.
• Status: fully formalized. The accompanying verify/Skelet1LikeC2_1RB0RF_1RC0RB.v (2,584 lines) proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9).
• It compiles in about a minute with -native-compiler yes.
• Print Assumptions nonhalt is closed (no axioms).
• coqchk does not finish within a 600 s cap. The base case is 38 native_compute steps, so the result rests on coqc's kernel check at Qed, with the VM and the native compiler in the trusted base.

Template

The outer shape follows verify/SBCv6.v, Module TM21:

• a configuration built from a list of digit blocks;
• one invariant on macro states and a closure lemma inv_step : Inv s -> exists s', cfgI s -->+ cfgI s' /\ Inv s';
• the end by multistep_nonhalt and progress_nonhalt_cond.

The finite runs follow the idea of verify/Sk1like_TC_v1.v: a step function that is computed, proved correct once, and then run by evaluation.

What is different here:

• A verified symbolic simulator. Every finite run (block runs, left episodes, right-region episodes, record-exit episodes and the base case) is computed by one run-length simulator of the table, with a soundness theorem. Run lengths are linear forms c + v_1 x_1 + ... + v_n x_n over N, so one computation covers every value of the gaps.
• A chain of eight-state blocks. The digit list is a chain of blocks with an exit phase, and Lemma T counts the visits of a whole record interval.
• A right region with jumps. The right end is run by a verified executor for interval programs, with 4-cycle jumps by induction on the cycle count.
• A long macro step. One macro step is a whole record interval (81 x 3^K visits). The invariant has six classes, and after six steps u becomes 9u.

Where each section lives in the .v

Section 10 describes the .v in more detail, including the places where it takes a different route from the text.

Overview

Summary

Between the two blank ends the tape alternates, except at defects, two equal neighbouring cells. A sweep complements every cell it crosses but keeps the defects in place. So the defect pattern changes only when the head meets a defect.

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.

The long gaps are affine in a scale u (section 3.4), and u becomes 9u over the six phases. So every long gap grows by a factor close to 9 (not exactly 9: the constant terms stay).

The proof idea

The proof is an induction over these six-phase periods.

• A configuration at a record exit (the moment just after an overflow) is described by an invariant C_r(e): a class r (one of six), an epoch e, and a window of exact gap lengths, all affine in u = 9^(e-2).
• Lemma S maps C_r(e) to C_(r+1)(e), and C_r4(e) to C_r5(e+1).
• Each step of Lemma S is assembled from three region lemmas (C for the chain, L for the left word, R for the right region), a counting lemma T, and a symbolic run of the right region that is exact for every u.

The two growing blocks stay in step with the counter by an exact cancellation (section 5.4). The halting transition needs two defects at distance 1 in a particular phase, and every run in the proof avoids it.

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.

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. This does happen, inside some right-region episodes (4.3 works out an example). The rules above already cover it, since a toggle is a symmetric difference.

So the proof does not assume that defects never cancel. Only the halting case has to be ruled out.

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 }

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 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.

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 four parts, 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. 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.

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). Suppose all blocks are full and the head enters from the left at phase c_1 + 2. Then 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.

The proof uses 17 of these 18 runs. Block 1 is entered from the left only by a carry back, at phase c_1 + 2 (Lemma L). So the m = 1 run "D0 entered from the left at c" never occurs; the table lists it for completeness.

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. The 18 runs were computed for 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. 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.

In the .v each of the 11 runs with m = 3 is a single symbolic computation with every gap a variable, so it holds for all gap values at once. Block 1 always has digit gap 1 by (C), so its 6 runs that the proof uses are computed with concrete lengths (section 10).

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. 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.

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.

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.

The two regions stay apart in the other direction too. 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. It 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.

• (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.
• (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.

In simulation terms, the event sequences of the two runs in (3) are identical, by induction on the events. Two defects on opposite sides of a long gap always stay at least 12 cells apart, so no rule ever sees across the gap.

Cancellations inside an episode. An episode may cancel two defects on the way. The entry's result already accounts for this, and the transfer lemma 2.4 needs no assumption about it: its proof matches the toggles one for one.

Entry r5.23 is an example. Take the chain end B = 2, so c_K = 0, and the exit phase c_K, with

x_1 .. x_5  =  27, 54, 62, 63, 88        hi = 91        (shape L1 L3 8 1 L1 3)

Moving right, the head meets:

Both 62 and 63 were defects, so they cancel. The episode goes on without a halt and returns at phase 0 with the defects 27, 55, 87, 92 and hi = 94. This is the entry's result: x1, x2+1, x5-1, hi+1, and hi grows by 3.

The .v does not use the table: it runs every episode of an interval symbolically, with the long gaps as linear forms (section 10). The table is the readable form of those runs.

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. 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.
• (3) The shapes hold throughout. Suppose 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.
• (4) 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, their counts c, and the vectors at the first and the last jumped cycle. The two composites are

f(h1, 7, h3, h4, 3)  =  (h1, 7, h3, h4 + 36, 3)
f(h1, 8, h3, h4, 3)  =  (h1, 8, h3 - 4, h4 + 32, 3)

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

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'. There are 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

The whole step is computed 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). Write 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      E_2, ..., E_5 unchanged

The other five lines are evaluated 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.

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. Appendix C gives this configuration exactly.

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), at step 2,629,088,227,408. Section 6.4 closes Lemma S symbolically for every u, in all six classes.

Theorem. The machine never 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 (section 7). Some right-region episodes cancel two defects on the way (4.3); the results of Lemma R already include this.

The .v takes a shorter route to the start of the induction. It simulates the run from the blank tape directly up to record exit 28, so it needs neither the configuration at record exit 16 nor the twelve concrete steps (section 10).

9. Other starts of the same table

Two more holdouts run this transition table from another start state:

The first has the same record numbering. The second has one more 3-cell move of λ in its start-up, so its record n is its (n + 1)-th 3-cell move.

The first reaches record exit 16 in C_r5(0), after 398,095,384 steps from its start. From there on its gaps are this machine's, except one deep chain gap that is 4 cells longer. The deep chain enters only through residues and lower bounds.

The second reaches record exit 16 after 397,796,108 steps, and its record exits 16-27 satisfy (L), (C) and (H). Its windows at record exits 16-25 are not those of Appendix C, however. One start-up gap is 36 cells shorter (936 against 972 at record exit 16), and up to record exit 25 it still lies in the window or in the right region. From record exit 26 on, only deep chain gaps differ.

Both runs are in C_r5(2) at record exit 28, with the window V_r5(1). That is the base case of their proofs.

So the argument of sections 3-8 applies to both from record exit 28 on. The .v proves only the string of this write-up.

The other two are proved in verify/Skelet1LikeC2_1RB0RA_1LC0RE.v and verify/Skelet1LikeC2_1RB1RZ_1LC0LA.v. Each keeps the library part of this .v word for word, stated for this table as tmP: the simulator and its soundness, the chain and region lemmas, Lemma S, Inv and inv_step.

Each has its own base case and its own final theorems. A renaming lemma (for the second, with a mirror) turns a halt of that machine into a halt of this table. Their write-ups are attached alongside.

10. The formalization

10.1 The simulator

The .v does not formalize the defect model of section 2. It runs the transition table itself, on a run-length encoding of the tape.

• A run is a first symbol and a length; the cells of a run alternate. Where two runs meet with equal symbols there is a defect of 2.1. The boundaries between regions are cuts placed inside alternating stretches.
• A length is a linear form LF c [v1; ...; vn], standing for c + v_1 x_1 + ... + v_n x_n over N.
• A side is a list of runs, nearest the head first, followed by the blank stream or an abstract side.

One simulator step sstep crosses a whole run at once when the head state and the run's first symbol are in a sweep cycle of 2.1 and every coefficient v_i is divisible by 4. Otherwise it makes one machine step with tm.

The soundness theorem sstep_spec holds for every value of the x_i and every content of the abstract sides. reach iterates the simulator to a target configuration, and reach_spec turns a successful computation into a -->+ run of tm.

A simulator step returns nothing when tm has no transition, so every run proved this way is free of halts. If a computation would read an abstract side, it fails. So a successful reach is also a locality proof: the run holds for every content of the abstract sides.

This replaces the transfer lemma 2.4. A gap of residue c is a run of length c + 4x, and one computation covers every x.

10.2 The pieces

• Blocks. The eight m = 3 states are the labels lab, with run lengths lens. The gap variables are t = 4 + 4x_0 and s = 4 + 4x_1 (separator gaps), a = 1 + 4x_2 (digit gap) and lp = 2 + 4x_3 (the inter gap on the block's left, minus 3). The tight gaps are the instance x = 0, so they need no separate case.
• Single-block runs. The 17 runs of 4.1 that the proof uses are blk_turn, blk_pass, blk_reset (11 runs, m = 3, every gap a variable) and blk1_turn, blk1_pass, blk1_back (6 runs of block 1, five states lab1, concrete lengths). Each case is one reach computation with both sides abstract.
• The unused run. The m = 1 run "D0 entered from the left at c" never occurs (4.1), and the .v does not state it.
• Lemma C, C'. The functions visit3, cb and vis compute a visit on the label list. visit3_spec, cb_spec and vis_spec prove by list induction that the machine follows them. runv_spec chains n visits with the episodes between them.
• Lemma T. interval computes the visits of a whole interval on labels for every number m >= 2 of m = 3 blocks: 81 x 3^(m+1) - 1 visits, the first T of them at phase c_K + 2, with 2T + 5 = 3^(m+2). This is a proof for every K, in the pieces CU, CW, S3, allD and cycs.
• Lemma L, L81. The left word lw i is the closed form of 4.2 (lw 81 is the word after the record). lw_all checks all 81 episodes in one computation, and lw_ep states them. The .v numbers the episodes 0..80, so its episode 80 is the left record.
• The right region. ep_run runs one episode with the chain side abstract. jump_run checks one 4-cycle on a template with a fresh variable per changing run, and jump_lemma repeats it by induction on the cycle count (Lemma J). exec runs a program of single episodes and jumps, with soundness exec_spec.
• The six interval programs. prog_r5 .. prog_r4 are the programs of Appendix B with u = 1 + 8t, and int_r5 .. int_r4 check them by vm_compute. Each check also confirms the phase counts of Lemma T. For class r5 these are 3278 + 26244t episodes at phase c_K + 2 and 173868 + 1390932t at phase c_K.

10.3 Lemma S and the invariant

• Record visit. record_visit is the carry-out at all D0, left episode 81 and the carry back to all D2 (6.1).
• Regrouping. regroup is the tape equality of 6.2, by list induction on the chain. It takes no machine steps.
• Exchange and window. step_r5 .. step_r4 do the exchange of 6.3 and the next record-exit episode as reach computations. The take-in classes first split one run of the right region (split4).
• Lemma S. S_r5 .. S_r4 compose the interval, the record visit, the regrouping and the exchange, for every e >= 2 and every deep chain.

The invariant Inv (r, e, t, nus) is taken one episode later than C_r(e): after the record-exit episode, with the head entering the chain at phase c_K and the right region at the start vector of Appendix B.

• Reading from the head leftward, the chain is the m = 3 blocks in U0 with gap variables nus, then block 1 in U0, then the left word W_1.
• win fixes the window part of nus (for example x_0 = 18701 + 149688t for the last block in class r5) and the length of the deep part. The deep part is arbitrary, so the residues and minimums of (C) are built into the encoding.
• The arithmetic side is 2 <= e and 1 + 8t = 9^(e-2). After r4, t becomes 1 + 9t.

inv_step is the closure lemma, one class at a time.

10.4 Base case and conclusion

• init28 runs the simulator from the blank tape to record exit 28: 18,571,896 simulator steps, about 2.63 x 10^12 machine steps. It is cut into 38 pieces ck_0 .. ck_37, each one native_compute check between two written-out configurations.
• base28 moves the head 3 cells to the chain cut and runs the record-exit episode, reaching the invariant at class r5, e = 2, t = 0 (inv28). The chain there has K = 7 blocks.
• nonhalt is multistep_nonhalt with init28 and base28, then progress_nonhalt_cond with Inv and inv_step.

11. Numerical checks

They are evidence only; the result rests on the .v file alone.

• Defect model. The rules of 2.2 agree with direct simulation of the table 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). They also agree on 10,000 random tapes of up to about 2,400 cells.
• Record exits. The operational definition of 3.3 finds record exit 16 on the direct simulation. (H) and the formula for B hold at every record exit 16-39 of the defect-model run.
• Base configuration. Appendix C agrees with direct simulation, cell by cell.
• Chain. Every word of Lemma C's shape for K <= 2, and the pair (2, 3) at K = 3 entered from block 1, was run 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 add 5,210 runs. All give the lemma's result, with no collision, and no defect is ever left of A.
• Lemma T. It holds 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).
• Left end. All 81 episodes, run in a row from W_1 on a tape that holds only the left region, give the words of 4.2 and the record, without halt. With the first three chain blocks present in their full states at the tightest gaps (4 contexts, 324 runs), the result is the same and the chain is untouched.
• Right table. It was built from records 16-27 (262,430 episodes) and predicts every one of the 2,125,759 episodes of records 28-33. Every combination of the long gaps in {min, min + 4} (5,376 runs) and every long gap increased by 4j with j up to 10^6 (810 runs) give the table's result, with no halt.
• Record steps. On exact numbers, with every episode run singly (no jumps), the step reproduces every next record exit from record exits 16-27, and 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).
• Deep chain. Replacing every deep chain gap by a random value with the same residue and at least its minimum gives the same next window and a deep chain in the invariant (120 trials at record exits 16-27, 15 at 28-32).
• The run. Record exits 28-39 have the windows V_r(1) and V_r(9). The defect model runs to 1.2 x 10^14 steps without a halt.
• Other starts. For both holdouts of section 9, record exits 16-33 satisfy (L), (C) and (H), the step on exact numbers maps each record exit 16-27 to the next one, and the windows at 28-33 equal V_r(1). For the first, record exits 16-27 also have the windows of Appendix C, so they are in C_r(e). For the second they are not (section 9).

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, 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 does not show 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. 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

From record exit 28 on, the windows are V_r(1), V_r(9), and so 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 the run gives 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).

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic); corrections from an independent audit by GPT-6 Astra (OpenAI).