W7-5: the machine never halts (informal proof, both starts)

Table 1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---, started in A (740 line 274) and, mirrored and renamed, in F (740 line 514, 1RB---_0RC0LD_1RD1RC_1LB0LE_1LF0RA_0LD1LA).

Stage: informal proof, 2026-10-14. Every claim below is checked by check_proof.py in this directory (section letters in brackets; map in section 10). Status: CHECKPOINT_B. The review found the proof sound, with 5 minor gaps, all fixed (Review log, section 11).

0. What the machine does

The machine is a base-4 counter. Its digits are four fixed words in a sea of 100. The least significant digit is at the right end, next to the head's turning point.

One sweep adds 1. The head runs left from the right end to the first digit that is not 3, turns, and runs back. On the way left, every digit 3 is turned into a block (10)^4 that has eaten the first sea word to its right. On the way back, every such block becomes a digit 0.

When every digit is 3, the carry reaches the left end. With a wall 1100 there, the wall disappears (O1). Without a wall, a wall appears and a new digit 3 is born at the right end (O2). So the number of digits grows by one every two overflows, forever.

The only thing that could go wrong is a digit that needs a sea word and finds none to its right. Section 5 shows that one field, the one in front of the youngest digit, always has enough sea words for every older digit. That field is born large (about 3·4^k), and the older digits need only about 4^k/3 until the next birth.

1. The table and the two starts

• F1 is the only undefined transition. F is entered only by D1 (0LF) and E1 (1RF). [A]
• Line 514 is this table mirrored, with its states renamed by phi: A->F, B->B, C->C, D->A, E->D, F->E (514 state to this table's state). All 12 transitions agree, and this is the only map among the 720 renamings times 2 mirrorings. [A]
• So line 514 run from blank is, step by step, the mirror image of this table run from 0^inf F> 0^inf, with states mapped by phi. Line 514 halts if and only if this table halts from start F.

Lines 274 and 514 are therefore the starts A and F of one table. The proof below is about the table; section 7 gives the opening run for each start.

2. Notation

2.1 Words

w^n is n copies of w. Exponents are natural numbers; a lemma with an exponent holds for every value.

2.2 Head notation

u q> v means: the head is in state q on the first cell of v. u <q v means: the head is in state q on the last cell of u. When <q stands first, the head is on the (unread) cell left of everything written. 0^inf marks an end of the tape that is blank.

2.3 D-records and configurations

A D-record is a moment when the head, in state D, steps onto a cell it has never visited, at the right end. At every D-record of interest the tape is

C(W; p1..pk; f1..f(k-1); r)  =  0^inf [W] P(p1) s^f1 P(p2) s^f2 ... s^f(k-1) P(pk) s^r D> 0^inf

with k >= 1 digits, phases p_i in 0..3, fields f_i >= 0, and r >= 1 sea words between the last digit and the head. The wall, when present, touches the first digit (no field between them). The counter value is V = sum p_i 4^(k-i): digit 1 is the most significant, digit k the least.

3. Pass lemmas

Each lemma is an exact run of the machine on the cells shown, with the stated number of steps, for every value of the exponents. Cells outside the shown window are never read (they can be anything), except where the window ends in 0^inf. [B, C]

S0 visits exactly the four cells of 1010 (it ends in B on the last cell of the 100 before them, which it does not read). Every cell to the right of 1010 is still unvisited and blank. The cell after 1010 is first visited at the very end of the sweep, by the D> of RA2, RA3 or L5e, or among the new cells of RE2. In the lemmas ending in D> 0^inf, the final cell is the first cell never visited, and no earlier moment of the lemma is a D-record. [B]

3.1 How the lemmas with exponents are proved

The lemmas without exponents are finite runs. The others use six shift rules, each a finite run on one copy of X plus induction on n. In each rule a short group of cells (the "object") travels with the head and comes out unchanged. [C]

Usage: L2 is Ch1 then Ch2. L5 and L5e are Ch1, Ch2, then Ch3 on X^j and again on X^i. L7 is Ch1, Ch2, Ch4. RA1 and RA3 split j = 0 or j = j'+1 and use Ch5. RE1 splits the same way and uses Ch6.

The words (10011001)^n that the shift rules write are the digit words P0^n cut at another place. For example, L5 ends with the identity

P2 P0^n 1  =  1001100 (11001100)^n 1  =  (10011001)^(n+1)

The final comparison with each right-hand side is an identity of words like this one. [C]

The proofs are done by proof_scripts/symx.py, a symbolic executor in the style of busycoq's shift rules. It runs concrete transitions on concrete cells, crosses a block only with a shift rule it has just verified on one copy, peels a copy off a block whose exponent is at least 1, and otherwise splits a variable into 0 and n'+1. Section B of check_proof.py re-runs every lemma by plain simulation (exponents 0..5, random context cells) as an independent check of the executor.

4. One sweep

4.1 The left pass

Start from a D-record C(W; p; f; r). S0 and r uses of L1 bring the head to

0^inf [W] P(p1) s^f1 ... P(pk) <B  T,      T = s^r 1010 0^inf

T is the processed tail: a word over the letters X and s, followed by the end 1010 0^inf.

The pass goes left digit by digit, starting at digit k. While the digit at the head is P3:

1. Wrap (L2). T has the form X^j s T' (j >= 0 leading blocks, then the first s). L2 replaces P3 and that first s by one more block: T becomes X^(j+1) T'.
2. Cross the field (L1). The field s^f to the left of the digit moves into T unchanged: T becomes s^f T.

In words, a wrapping digit eats the first sea word to its right. If its own field is empty, that sea word comes from further right. This is the "push" of the observe stage.

The pass stops at the first digit with phase 0, 1 or 2 (the stop digit), or at the left end when every digit is 3.

4.2 The turn (case split)

So a stop at phase 1 also eats the first sea word to its right.

4.3 The right pass

A-pass. The head carries the object 10 A>. T splits into maximal pieces X^a s (a >= 0) and the end. RA1 turns each X^a s into P0^a s. At the end, RA2 (or RA3 after a block) turns the end into s s and the head is at the next D-record.

E-pass (O2 only). The head carries the object 1 E>, which always has an s written just before it. RE1 turns s X^a s into P0^a s s. Compared with RA1, the digits of the block end up 2 cells further left, and one s moves from the field on their left to the field on their right. At the end, RE2 turns the last two written sea words into P3 s s s. That P3 is the newborn digit.

Fields in the E-pass. In an O2 sweep every digit wraps. T after the wraps starts with a block, because there is no field before digit 1. Group T into maximal block groups:

T = X^(a_1) s^(g_1) X^(a_2) s^(g_2) ... X^(a_m) s^(g_m) 1010 0^inf,      every a_i >= 1

The gaps g_1, ..., g_(m-1) are the nonzero fields left of the last digit after the wraps, in order, and g_m is what is left of r. The zero fields lie inside the groups. So g_i >= 1 for i < m by maximality, while g_m may be 0.

The E-pass changes the gaps as follows.

1. L7 writes the wall, turns X^(a_1) s into P0^(a_1) s and keeps that s, written just before 1 E>. RE1 with j = 0 then crosses the other g_1 - 1 sea words of gap 1. Gap 1 now holds g_1 written sea words.
2. RE1 on a group i >= 2 uses the s written just before 1 E>, which is the last s of gap i-1, together with the first s of gap i, and writes P0^(a_i) s s. RE1 with j = 0 then crosses the other g_i - 1 sea words of gap i. So gap i-1 loses one s and gap i holds g_i + 1.
3. RE2 takes the last two written s of gap m.

Every gap except the first gains one s from its own RE1. Every gap except the last loses one to the next RE1. The last gap loses two to RE2. The gaps after the sweep are

m >= 2:   g_1 - 1,   g_2, ..., g_(m-1),   g_m - 1
m = 1:    g_1 - 2

followed by the newborn P3 s^3. After the wraps, the E-pass lemmas find their context exactly when g_m >= 1 (L7 for m = 1, the last RE1 for m >= 2) and, if m = 1, g_1 >= 2 (RE2 needs two written s; for m >= 2 the last RE1 always wrote two). [E]

4.4 The sweep in counter terms

Write the configuration after the sweep as C(W'; p'; f'; r'). [D, E]

• R1/R2 (stop digit i). Digits i+1..k (all 3) become 0, digit i goes up by one, and digits 1..i-1 are unchanged. So V' = V + 1. The wall is unchanged.
• O1. All digits go from 3 to 0, and the wall disappears. So V' = 0, which is 4^k in absolute terms.
• O2. All digits go from 3 to 0, the wall appears, and a digit 3 is born at the right end. So k' = k + 1, V' = 3 and r' = 3.

Consumption law [E]:

• The consuming digits are the stop digit if its phase is 1, plus every wrapped digit.
• Each takes one s from the first nonempty field at or to the right of it, in the order f_l, f_(l+1), ..., f_(k-1), r. The consumptions happen right to left.
• No other field changes, except as follows.
• In a sweep without O2, r' = (rest of r) + 2, where the rest of r is what the consumptions leave of r. If the rest is at least 1, the right pass crosses it and ends with RA2, which adds s s. If the rest is 0, the pass ends right after a block, with RA3 or L5e, and r' = 2.
• In O2, the first nonzero field after the wraps and the rest of r each lose one more s. If the rest of r is the only nonzero field after the wraps, it loses two. This is the gap rule of section 4.3: in the domain (g_m >= 1) the gaps are exactly the nonzero fields after the wraps, so g_1 is the first of them and g_m is the rest of r. Zero fields stay zero. What is left of r becomes the newborn's left field, and r' = 3.

The exact step count of a sweep is the sum of the steps of its lemmas. It equals the observe-stage step rule R3. [D, H]

4.5 The domain and the sweep theorem

The sweep of C is defined when every lemma it calls finds its context:

• (D1) every wrap (L2) and every phase-1 stop (L5/L5e) finds an s in T;
• (D2) in O2, the first block is followed by an s (L7), the last block is followed by an s (RE1 rather than a block next to the end), and RE2 finds two written s before the end. In the gap notation of section 4.3: g_m >= 1, and g_1 >= 2 when m = 1.

Sweep theorem. If the sweep of C is defined, the machine goes from C to sweep(C) in exactly steps(C) steps, with no D-record in between, and it does not halt on the way.

Proof. The left pass, the turn and the right pass are compositions of the lemmas of section 3. Each lemma is applied with the rest of the tape as untouched context, which is allowed because no lemma reads outside its window. The configuration after each lemma is again of the form used by the next one (sections 4.1 to 4.3). That is an induction on the digits for the left pass and on the pieces of T for the right pass. No lemma halts, so the sweep does not halt.

Checks [D]: 5,636 random in-domain sweeps and all 74,587 in-domain configurations with k <= 4, fields 0..2 and r 1..5 (both walls) give exactly the machine's next D-record, configuration and steps. The 813 small configurations outside the domain are not claimed.

5. Invariant and progress

5.1 Birth configurations

For k >= 2 and fields f, the birth configuration is

B(k; f1..f(k-1)) = 0^inf 1100 P0 s^f1 P0 ... P0 s^f(k-1) P3 s^3 D> 0^inf

This is exactly the form that O2 produces: the wall, digits 0, ..., 0, 3 (so V = 3), and r = 3. Set

m_k = (4^k - 4) / 3 = 4 + 16 + ... + 4^(k-1)

5.2 Epoch theorem

Epoch theorem. If f(k-1) >= m_k, then

B(k; f)  -->  B(k+1; f')    in N = 2·4^k - 3 sweeps, each defined,

with f'_k = 3·4^k - 5, or 3·4^k - 6 when every field left of the last digit is empty after the O2 wraps (possible only if f(k-1) = m_k). In both cases f'_k >= m_(k+1). [F]

Proof. Let C_t be the configuration after t sweeps, t = 0..N-1. Let Q_t be the number of consumptions by digits 1..k-1 in sweeps t..N-1. This number is fixed by the counter alone, through the consumption law. We prove the following by induction on t.

I(t):

• (a) the phases of C_t are the base-4 digits of V_t = (3 + t) mod 4^k, and the wall is present iff t <= 4^k - 4;
• (b) r_t = 3 + 2t - ceil(t/2);
• (c) f(k-1) in C_t is at least Q_t.

Base. V_0 = 3, r_0 = 3, and Q_0 = m_k <= f(k-1). The count Q_0 = m_k holds because the digit at position e >= 1 (weight 4^e) consumes 4^(k-e) times in an epoch. In one epoch the increments pass the values 4, 5, ..., 2·4^k (O1 passes 4^k, O2 passes 2·4^k). The digit goes 1 -> 2 at v = 2·4^e mod 4^(e+1) and 3 -> 0 at v = 0 mod 4^(e+1), each 2·4^(k-e-1) times. The sum over e = 1..k-1 is m_k.

The sweep is defined. In sweep t, every consumption by a digit l < k takes the first s at or to the right of f_l. Field f(k-1) is reached last and holds at least Q_t, which is at least the number of these consumptions. So it is never empty when reached, and no consumption by an older digit reaches r. The last digit consumes at most once, from r, and r_t >= 3. This gives (D1).

In O2 (t = N-1), what is left of r after the wraps is g_m = r_t - 1 = 3·4^k - 4 >= 2 sea words (gap notation of section 4.3). This gives (D2), in two cases.

• If m >= 2, the first block group is followed by g_1 >= 1 sea words by maximality, so L7 applies. RE1 applies to every group in between for the same reason, and to the last block group, which is followed by r_t - 1 >= 1 sea words, and RE2 finds the two s that this RE1 writes.
• If m = 1, every field left of the last digit is empty after the wraps (this is the -6 case). The only block group is both the first and the last. L7 handles it, not RE1, and RE2 finds 2 of the g_1 = r_t - 1 >= 2 written sea words after it: the one L7 keeps and those crossed by RE1 with j = 0.

Step. (a) is the counter law. For (b): the last digit's phase in sweep t is (3 + t) mod 4, so it consumes (phase 1 or 3) iff t is even. That consumption comes from r, and the right pass adds 2 (consumption law; here the rest of r is at least 2, so the pass ends with RA2). (c) holds because f(k-1) loses at most the number of consumptions by older digits in sweep t, and that number is exactly Q_t - Q_(t+1). (The step is needed only for t < N-1. By (a) these sweeps are not O2, so by the consumption law no field loses anything except through consumptions.)

End. Sweep N-1 is an O2: V = 4^k - 1, and the wall is absent because N - 1 > 4^k - 4. Its last digit eats one s of r_(N-1) = 3·4^k - 3, so the rest of r is 3·4^k - 4. By the O2 law the newborn's left field is that rest minus 1, or minus 2 when the only nonzero field left is the rest of r. All old digits are 0, the wall is back and r = 3, so the result is B(k+1; f').

Finally,

3·(3·4^k - 6) - (4^(k+1) - 4) = 5·4^k - 14 > 0      (k >= 1)

so f'_k >= m_(k+1), with strict inequality. So every epoch after the first starts strictly above the minimum. Then f(k-1) still holds an s after the O2 wraps, the first nonzero field is not the rest of r, and f'_k = 3·4^k - 5 exactly. [F]

Checks [F]: the closed forms and the identities, for k up to 199; the consumption counts by direct counting for k = 1..6. Full abstract epochs for k = 2..7, from birth configurations with f(k-1) at the minimum m_k and the other fields all 0, random 0..3, or random 0..50: every sweep is defined, I(t) holds at every t, and each run ends at B(k+1) with the stated f'_k. At the O2 sweep, m = 1 exactly in the runs that end with 3·4^k - 6, and the gap rule of section 4.3 gives the same result as the sweep.

5.3 Main theorem

Theorem. From any B(k; f) with k >= 2 and f(k-1) >= m_k, the table runs forever.

Proof. By the epoch theorem and induction, the run passes through B(k; .), B(k+1; .), B(k+2; .), ..., each after finitely many sweeps. Each sweep takes at least 9 steps (S0). By the sweep theorem no step halts.

Halting is unreachable. Halting needs F to read a 1. Between two D-records the run is a chain of lemma runs, each an exact run on defined transitions. Inside them F always reads 0. So F1 is never executed.

6. Progress at a glance

The fields left of the youngest digit can be anything, including 0. In the real run they shrink and die one by one, and the dead digits form the zero-field cluster at the wall. The proof never needs them.

7. Openings (start-parametric part)

7.1 Line 274: start A

Direct simulation from blank: [G]

• Step 108 is the first D-record in the language: C(no wall; P1; r = 3) = 0^inf 110000 s^3 D> 0^inf.
• Three sweeps later (R1, R1, O2), step 477 is the first birth, B(2; f1 = 3). Here 3 is one below m_2 = 4, so the epoch theorem does not apply yet. The opening runs on.
• Step 7,910 is a D-record with tape B(3; 0, 41) = 0^inf 1100 P0 P0 s^41 P3 s^3 D> 0^inf, and 41 >= m_3 = 20. Steps 108 to 7,910 are 32 sweeps of section 4, and every D-record in between matches.

By the main theorem with k = 3, line 274 never halts.

7.2 Line 514: start F, mirrored

Line 514 from blank is the mirror image of this table from 0^inf F> 0^inf (section 1). [A, G]

• Run as itself, line 514 at step 792 has its head in state E on a new leftmost cell. E is phi^-1(D), so this is a D-record of the table. Read mirrored, the tape is B(2; f1 = 7) = 0^inf 1100 P0 s^7 P3 s^3 D> 0^inf.
• The table run from F gives the same: a D-record at step 792 with tape B(2; 7).
• 7 >= m_2 = 4.

By the main theorem with k = 2, this table never halts from F, so line 514 never halts.

7.3 The two runs side by side

After their openings both lines follow the same rules. Their counters are equal, and their fields differ only in one field (+4 on 514), which moves right whenever the cluster absorbs a digit (observe stage). The proof does not need this.

8. Cross-checks (not needed by the proof)

• The abstract orbit (section 4 sweeps from the openings) equals every real D-record from step 108 (274) and step 792 (514) up to 1e9, configuration and step: 18,410 and 18,406 sweeps. It also hits the C core's first D-record after 1e11 on both starts: steps 100,001,300,895 and 100,000,054,594. [G]
• The sweep of section 4 equals the observe-stage model (scripts/model.py, rules R1/R2/PUSH/O1/O2 and step rule R3) on 2,812 random in-domain sweeps. [H]
• In the observe-stage notes, the O2 rule says "every digit moves 2 more cells left, then pushes". Section 4.3 states the same thing exactly through L7, RE1 and RE2.

9. Lemma plan for the formal proof

9.1 Against verify/Sk1Machines.v (mxdys): it applies only in part

Sk1Counter/Sk1CounterMixed prove a digit counter from a wall hypothesis and a one hypothesis. A head visit passes a segment word p ++ W^^(take p + n), and a batch rule chains digits. Our machine has the same shape:

• a periodic sea (W = 100);
• fixed digit words;
• a take of 1 on phases 1 and 3;
• a carry on phase 3.

Three things do not fit:

• A wrap moves a digit by 2 cells (P3 s becomes X, then P0), not by whole W words. The digit words would need a re-cut before one reads as take/give.
• Consumption reaches through empty fields. The batch rule requires "all consumed W initially available" in the digit's own field.
• The O2 pass (E object, RE1/RE2) and the birth are a second kind of visit.

So we follow our own route: the closed-language and epoch-invariant structure of kills #30/#7/W4-1, with segment lemmas in the Individual62 style.

9.2 Coq lemma list

1. Shift rules Ch1..Ch6, and the sea rules L1, RA1 (j = 0) and RE1 (j = 0), each by induction n plus a finite execute.
2. Pass lemmas S0, L1..L7, RA1..RA3, RE1, RE2 as -->+ lemmas: finite runs plus the shift rules, with word re-cuts by lpow and app rewriting.
3. An abstract configuration type: wall bool, a list of (phase, field), and r : N. The tail T as a list of X and s^n. A function sweep with an option result for the domain.
4. The sweep theorem: induction on the digit list (left pass) and on T (right pass), composing the pass lemmas.
5. The counter and consumption laws as list lemmas about sweep, including the E-pass gap rule of section 4.3 (induction on the block groups: one s moves from gap i-1 to gap i at each RE1).
6. The epoch invariant I(t) and the epoch theorem: induction on t, with arithmetic on N (lia/nia, using 4^k closed forms).
7. Openings: - 274: solve_init for 7,910 steps to B(3; 0, 41); - 514: busycoq's flip_halts/perm_halts with phi (as in the #7 and W4-1 files), then 792 steps from F to B(2; 7).
8. nonhalt from the infinite chain of birth configurations, via progress_nonhalt on the family B.

Nearest solved example: #30's .v (Individual62, epoch invariant on counter positions). It is heavier than what this machine needs: there is no recursive digestion here, and the invariant is one field bound.

10. check_proof.py map

Files:

• proof_scripts/symx.py: the symbolic executor.
• proof_scripts/sweep.py: the abstract sweep of section 4.
• proof_scripts/tm.py: plain simulator and decoders.

11. Review log

Checkpoint B review, 2026-10-14: sound, 5 minor gaps, no fatal or major one. All five are fixed.