W7-2 · 1RB1LB_1RC0LA_1RD0RE_1LA0LB_1RF---_1RB1LD: informal proof (start-parametric)

• Table: 1RB1LB_1RC0LA_1RD0RE_1LA0LB_1RF---_1RB1LD, viewer https://bbchallenge.org/1RB1LB_1RC0LA_1RD0RE_1LA0LB_1RF---_1RB1LD
• Listed starts:
• line 175 = this string (start A);
• line 489 = 1RB0RC_1LC1RC_1LD0RB_1LA0LE_1LF---_1LC1RA = this table from start D, mirrored, states renamed A→B, B→C, C→D, D→A (check_proof.py §A).

Nonhalting is invariant under mirroring and renaming, so everything below runs the table above, from A or from D. - Stage: informal_proof (2026-10-14). Status: OPEN (Checkpoint B material; not formalized). - State of the argument. Both starts are covered by one invariant made of two exact cycles of the same table:

INV := { N(Y) : Y >= 22 } ∪ { Q(W) : W >= 14 } N(Y) -->+ N(2^18 Y + 32859022) (start A enters here) Q(W) -->+ Q(2^18 W + 34431880) (start D enters here)

Start A reaches N(508932094) after about 4.1e18 steps. Start D first reaches a regime with two far fields (9.4e17 and 1.0e19 words), crosses it with a three-parameter lemma applied 39,144,505,581,733,537 times, and enters Q when the first far field runs out. Every claim is checked by check_proof.py (§A-§G, ALL OK, 38 checks in about 3 minutes, most of it the 8.9M-move opening run of start D). - Correction to the observe notes. The notes said 489 is "not covered" and feared that its depth "grows like a tower". The build-up is finite: the far fields are refilled once more inside the opening run, and when the big Y1 runs out, Y2 is absorbed into the accumulator in one event and the run settles into the cycle Q. No residue of a huge number is ever needed: every side-condition log is empty (§6).

0. Machine and the halting transition

Only C1 enters E, and only B0 enters C. So the machine halts exactly when it reaches B> 0 1 1.

The proof never needs this fact. It only uses that every computation it cites is an exact run of the machine that does not halt.

1. Notation: 4-cell blocks

Cut the tape into fixed blocks of 4 cells. A configuration is written

0^inf  w_1^{e_1} ... w_k^{e_k}  <S  u_1^{f_1} ... u_l^{f_l}  0^inf      (head faces left)
0^inf  w_1^{e_1} ... w_k^{e_k}  S>  u_1^{f_1} ... u_l^{f_l}  0^inf      (head faces right)

Each w_i, u_j is a 4-cell word and w^e is e copies of it. The head always sits on a block boundary.

• <S means: state S, reading the last cell of the block to its left.
• S> means: state S, reading the first cell of the block to its right.

This is the repo's directed-head notation (tools/sim.py) with block words.

The three key shapes.

N(Y)          := 0^inf 0001 1011^Y <A 0001^28 0011 0000 1000 0^inf
Q(W)          := 0^inf 0011 1101 F> 1010 0010^W 0000 0010^28 0000 1000 0100 0^inf
D(X, Y2, Y1)  := 0^inf 1101^17 1111 0111^X 1101^Y2 1111 0111^Y1 C> 0^inf

N(Y) is a few moves before the record M(X) of the observe notes, with X = Y - 14:

M(X) = 0^inf 1 1011^X 10111110 1110^26 <A 01010100010000010001000100001 0^inf

check_proof.py §C/§E tie N to the independent qsim records 21, 42 and 63 (M(508932080), 2^18 X0 + 36529024, M(2^36 X0 + 9575900996480)).

2. The three kinds of moves

Every computation in this proof is a sequence of the following moves. Each one is an exact run of the machine.

(a) Block step. The head faces a block. Run the machine inside that block until the head leaves it.

This is a finite table: 6 states × 16 words × 2 directions = 192 cases, each a few dozen steps at most. §B1 checks the table against plain simulation. A case that halts aborts the run; none occurs anywhere in this proof.

(b) Chain step (shift rule). Suppose a block step on word w, from state S facing d, leaves w' and exits on the far side in the same state S facing d. Then for every n >= 0, by induction on n,

S> w^n  -->  w'^n S>          and the mirror form          w^n <S  -->  <S w'^n

This table has exactly 7 such entries:

So a right sweep turns 1-one words (rotations of 0001) into 3-ones words, and the left sweeps turn them back.

(c) Diff rule. A Diff rule is a configuration shape with some exponents fixed and the others written v_i + k_i:

C(v_1 + k_1, ..., v_r + k_r)  -->+  C(v_1 + k_1 + d_1, ..., v_r + k_r + d_r)       for all v_i >= 0

The deltas d_i are integers, at least one negative.

• Proof obligation. One symbolic run of moves (a)-(c) from the generalized configuration back to the same shape, with every exponent shifted by d_i. Every decision in it (is this block non-empty?) must follow from v_i >= 0 alone.
• Use. If the current exponents are e_i >= k_i, the rule applies n = min over d_i < 0 of floor((e_i - k_i) / |d_i|) + 1 times in a row, giving exponents e_i + n d_i. Each application starts with every slot still >= its k_i.
• Linear forms. When an e_i is a linear form in a parameter, the division must be exact in its coefficients; otherwise the step is refused.

Typical Diff rules are the left carries, e.g.

0001 1011^(v+2) 1111 <A 0001^(w+2) T  -->+  0001 1011^(v+1) 1111 <A 0001^(w+3) T

Here the head walks one 1011 word at a time from the left run into the right run (T is a fixed tail).

The other family is the doubling transfers of the observe notes, (0100)^a 11 (0001)^b -> a+2, b-1 per visit. A marker crosses the right run one word per left-end visit, and every word it crosses becomes two words on the other side. Applied b times this is Z -> 2Z + c. A pair of them, or a transfer that writes four words, is Z -> 4Z + c.

Side conditions. A symbolic run carries one designated parameter (m, x or z below). When a decision holds only for large values of it, the run records the side condition param >= B and continues. Every lemma below reports this log; in this proof all of them are empty.

3. The two cycle lemmas (start-independent)

3.1 Cycle N

Lemma N. For every Y >= 22,

N(Y)  -->+  N(2^18 (Y - 14) + 36529038)  =  N(2^18 Y + 32859022).

On X = Y - 14 this is X -> 2^18 X + 36529024. Two of these give

X -> 2^36 X + 36529024 (2^18 + 1) = 2^36 X + 9575900996480,

which is exactly the period map M(X) -->+ M(2^36 X + 9575900996480) fitted in observe (42 qsim records). The 42-record period is two of these half-cycles. In 4-cell blocks they have the same shape, so the proof needs one lemma and no residue condition on Y.

Proof. A symbolic run from N(m + 22), m a free natural number: 187,865 moves (49,938 chain steps, 130,998 block steps, 6,929 Diff-rule applications, each rule proved by its own symbolic run as in §2(c)). Its side-condition log is empty (check_proof.py §D).

The big field is never divided: every m-dependent transfer multiplies it by 2 or 4. Its m-coefficient changes at these points (scripts/segments.py, work/segments.txt; every row starts and ends with 0^inf):

Between the boundaries the run does bookkeeping on small fields only. The far-end words (0001^28, 0010^21, 1000^81, ...) are consumed and rewritten one sweep at a time, and the small constants 82, 80, 28, ... are the same in every cycle. ∎

3.2 Cycle Q

Lemma Q. For every W >= 14,

Q(W)  -->+  Q(2^18 (W - 14) + 38101896)  =  Q(2^18 W + 34431880).

Proof. A symbolic run from Q(m + 14): 184,086 moves (6,814 Diff-rule applications), side-condition log empty (check_proof.py §G1). It has the same rhythm as cycle N, with the far end in the other phase (scripts/segments.py Q, work/segments_Q.txt):

(The ×2 steps between the listed rows are as in cycle N; the full list is in work/segments_Q.txt.) ∎

3.3 Checks of the two lemmas

• §D and §G1: the symbolic runs themselves, with their side-condition logs (both empty).
• §E and §G2: the same lemmas re-run on concrete values (N(22), N(23), N(29), N(64), N(1001); Q(14), Q(15), Q(40), Q(777)) by the concrete engine, which detects its loops differently and gets the same results.
• §B3: every Diff rule of these runs (400 sampled per run) is re-checked on 3 instances by a rule-free run (block and chain steps only), and the small instances also by plain simulation, step for step.
• §B1-B2: the block table and 171 random rule-free runs agree with plain simulation.

4. Invariant, progress, halting unreachable

• Invariant. INV := { N(Y) : Y >= 22 } ∪ { Q(W) : W >= 14 }.
• Closure. By Lemma N, N(Y) with Y >= 22 reaches N(2^18 Y + 32859022), again with Y >= 22. By Lemma Q, Q(W) with W >= 14 reaches Q(2^18 W + 34431880), again with W >= 14.
• Progress. Each cycle is at least one machine step (each has over 100,000 block steps).
• Halting unreachable. Every move of every run is an exact machine computation, and none of them halts (a halting block step would abort the run; none occurs). So from any configuration in INV the machine runs forever: this is progress_nonhalt with INV.
• Entry. Start A enters N (§5), start D enters Q (§6).

5. Start A (line 175): the opening run

Claim. From the blank tape in state A, the machine reaches N(508932094).

Proof. A checked accelerated run with the same three moves on concrete numbers: 657,961 moves, 24,932 Diff-rule applications, each rule proved by its own symbolic run (400 re-checked on instances in §B3).

It passes the regime the observe notes describe: the far fields 0001^100, 0100^14, ..., 1000^15901602 are exhausted and refilled, and 15901602 is absorbed into the accumulator (63616434 = 4 · 15901602 + 26). After that the run enters N.

Independent cross-check. sligocki's accelerated simulator (qsim, work/trace175_r.txt) reaches M(508932080) at step 4,111,147,719,584,449,981 (record 21), and 508932080 = 508932094 - 14. Its records 42 and 63 are 1011^(2^18 X0 + 36529024) and M(2^36 X0 + 9575900996480), i.e. Lemma N twice (§E).

With §4: line 175 does not halt (informal level).

6. Start D (line 489): the opening run

The run from D has three parts.

6.1 Opening, blank tape to the D regime. A checked accelerated run from the blank tape in state D reaches

D(X0, Y2_0, Y1_0)    with  X0 a 29-digit number,  Y2_0 = 10456559309013950571,  Y1_0 = 939468133961604901

after 8,855,536 moves (check_proof.py §F1, about 2.5 minutes). The far fields Y1 and Y2 are the two huge fields of the observe notes (there at qsim record 183).

The D shape already occurs once before, at move 313,457, with small far fields (X a 6-digit number, Y2 = 330, Y1 = 54). Two applications of Lemma D and the exhaustion of that instance build the big far fields. This is the "far-end refill" of the observe notes. It happens inside the concrete opening run, so the proof does not need a lemma for it; it simply enters at the first D shape with Y1 > 10^17.

6.2 Lemma D (three parameters). For all X >= 100, Y2 >= 130, Y1 >= 30,

D(X, Y2, Y1)  -->+  D(2^20 X + 349479900, Y2 - 120, Y1 - 24).

Proof: a symbolic run from D(x + 100, b + 130, a + 30) with x, a, b free natural numbers, ending at D(2^20 (x + 100) + 349479900, b + 10, a + 6). The side-condition log is empty (§F2). About 518,000 moves, 19,916 Diff-rule applications.

Cross-check: two applications give X -> 2^40 X + 349479900 (2^20 + 1), Y1 - 48, Y2 - 240. This is qsim's fitted 40-record period X_q -> 2^40 X_q + 377451701380050 exactly, with X_q = X - 10 (§F2).

6.3 Iteration. Apply Lemma D while Y1 >= 30. Y2 and X only grow or stay huge, so the count is fixed by Y1:

n = floor((Y1_0 - 30) / 24) + 1 = 39144505581733537
Y1_n = Y1_0 - 24 n = 13,      Y2_n = Y2_0 - 120 n = 5759218639205926131,      X_n = 2^20 X_(n-1) + 349479900.

Before each application Y1 >= 30 and Y2 >= Y2_n + 120 >= 130, so every application is valid.

6.4 The exhaustion event. Write z := X_(n-1). It is a huge number, but the next run needs nothing about it except z >= 0 (it is >= X0 >= 100). A symbolic run with z free:

D(2^20 z + 349479900, 5759218639205926131, 13)  -->+  Q(2^33 z + 23036877419765819664)

339,452 moves (12,895 Diff-rule applications), side-condition log empty (§F4). In this run the remaining Y1 words are used up, Y2 is absorbed into the accumulator in one transfer (as 15901602 was for start A), and the far end settles into the tail of Q.

6.5 Conclusion for line 489. Q(2^33 z + 23036877419765819664) is in INV (W >= 14 for every z), so by §4 the run from D never halts: line 489 does not halt (informal level).

What the observe notes got wrong. They expected a tower: Y1 running out would push the accumulator into the far end as a new far field. Instead Y2 is absorbed and the run enters a cycle with a fixed far end. The cryptid concern (residues of tower-size numbers) does not arise: §6.4 needs no residue of z, and n is an explicit number.

7. Lemma plan for the Rocq file

Nearest solved example: our kill #3, machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/ (Skelet 1-like Class 2, Individual62: one macro lemma per segment, then progress_nonhalt). What carries over and what changes:

• Invariant. Simpler here, and the same for both starts: fun c => (exists m, c = N(m + 22)) \/ (exists m, c = Q(m + 14)). No residue, no case split.
• Cycles. Two lemmas, N(m + 22) -->+ N(2^18 m + 38626190) and Q(m + 14) -->+ Q(2^18 m + 38101896). Each is a chain of segment lemmas along the tables in §3 (15 boundaries each). Each segment composes:
• the 7 shift rules of §2(b) (one shift_rule-style lemma per row);
• the left-carry and doubling-transfer Diff rules (forall n, C(n + k) -->* C'(...), by induction on n with execute and the shift lemmas);
• finite execute runs for the far-end bookkeeping (fixed small exponents only).
• Size. Each half-cycle applies about 6,900 Diff rules, about 600 of them with a parameter-dependent count. Most share a handful of shapes (left carries on 1011/0001, 1110/0100, 0111/0010, 1101/1000, with different far-end tails), so the tail should be a parameter of the lemma. A tactic-driven symbolic executor, or a reflective checker that replays the engine's trace, is the realistic route; 600 hand-written lemmas are not.
• Start D, extra pieces. Lemma D with three parameters; its iteration, by induction on n, stated as D(X, Y2 + 120 n, Y1 + 24 n) -->* D(f^n X, Y2, Y1) with f X = 2^20 X + 349479900; then exists z >= 100, X_n = 2^20 z + 349479900 for the exhaustion run.
• Opening runs. Start A: 657,961 moves (about 4.1e18 steps). Start D: 8,855,536 moves plus the 339,452-move exhaustion run. Options: replay the engine trace with the same lemmas on concrete numbers, or upstream Sk1Machines.v's Sk1Auto checked accelerated run (its counter shapes do not fit the cycles, but a checked run only needs the step lemmas).
• Upstream Sk1CounterMixed does not fit the cycles: there are no periodic digit words, and the far ends are fixed words.

8. Reproduce

cd "[local working file]"
python3 -B check_proof.py            # §A-§G, 38 checks, about 3 min; prints ALL OK
python3 -B check_proof.py A C D E G  # everything except start D (§F) and the re-checks (§B), about 40 s
python3 -B scripts/segments.py       # the segment table of Lemma N (argument Q: Lemma Q)
python3 -B scripts/bigrules.py       # the m-dependent Diff-rule applications of one N half-cycle

The engine is scripts/engine.py (stdlib only). Last full run: work/check_proof_all.txt.

9. Risks and open points

• The engine is the proof. The symbolic runs are too long to read; their soundness rests on scripts/engine.py (about 500 lines) and the checks in §B. The three move kinds are elementary, but a bug in the linear-form comparisons or in the Diff-rule application count would be a gap. A second, independent implementation (or the Rocq replay) is the real check.
• Anchors. A Diff-rule application can jump over a configuration, so each cycle anchor was chosen where no loop passes (N(Y) right after the far-end 0001 run is used up; Q(W) right after the last transfer of the cycle). The lemmas are what the runs prove; the anchor choice only affects whether a run is found.
• Rule thresholds. The bounds Y >= 22, W >= 14, X >= 100, Y2 >= 130, Y1 >= 30 are what the runs use, not optimal values. They are all far below the values that occur.