/machines/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF/proof.md · raw

1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (W5-8): never halts (informal proof)

Machine: 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (740 list, line 214).
Viewer: https://bbchallenge.org/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF
Sheet: "Bouncer + Chaotic Edge", class only, no claim. It is on mxdys's UBRRBA_TODO list, which is an acceleration to-do list, not a claim.
Upstream: not proved in busycoq BB6 HEAD 9cf9e88.
Written for: the string itself, from the blank tape. No mirror, no renaming. Its only undefined transition is D0.
Template: TranslatedBellv5.v Module TM1.
It proves block macro rules with ES_v3 es', repeats them with ind and chains them with follow.
It ends with progress_nonhalt_cond; this proof needs only progress_nonhalt_simple.
Second template: Bouncer_v2.v Module TM1, for a whole multi-trip run in one es' and for a 4.76M-step stepn opening.
Not reused: the nearest table by transitions, 1RB0LA_1LC1RD_0RB0LC_1LA1RE_1LF0RD_---1LE (distance 3, RWL_mod_v5.v), is a decider certificate.
Status: informal proof, complete.
Every rule is an exact claim for its whole domain, proved by symbolic execution (§3.2) with two shift rules (§3.1).
The top level is integer arithmetic (§4), and the opening is an exact finite run (§5).
check_proof.py checks every claim, exhaustively on small cases and on random large ones (§9).
Not formalized yet; §8 outlines the formalization.
AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).

0. Summary

The machine builds a tape of five long blocks of 1s, separated by four short "particles", with a fixed gadget G at the left end.

Every round trip starts at G. The head runs right over some of the blocks and is turned back by one of the particles. How far it gets depends on the trip's phase, which has period 12.

Over 12 trips the first block grows by 48 and the second shrinks by 8. So the particle after the second block drifts toward the particle before it. When the second block is down to 2, 4, 6 or 8 cells, a collision of 135 to 147 trips rebuilds the pattern with new block lengths.

Two of the collisions alternate forever. Together with the 12-trip steps between them they form a double cycle on a one-parameter family:

Even(n, x)  -->  Even(n + 12x + 808, x + 32)        (n odd, x = 4 mod 8, x >= 52)

The run from the blank tape reaches Even(12863, 212) at step 153,126,993, after an opening of 4,097,897 steps and 20 more macro steps. From there the double cycle repeats forever, and every piece of it is an exact run of the machine. So the machine never halts.

piece	status	checks (§9)
shift rules R1, R2b	exact finite runs + induction	SR
macro rules S, TE, TO, T6, T8	exact for the whole domain, by symbolic execution; S, TE and TO also trip by trip (§3.3, Appendices A and B)	MR, PH, COL, ENG, DIR, TEETH
double cycle	arithmetic on the rule domains	DC
opening: 4,097,897 steps, then 20 macro steps to Even(12863,212)	exact	OPEN, ORB
D0 never read	follows from the above	HALT

1. Rule table (busycoq comment-block style)

1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF        (only D0 undefined; D is entered only by A1 = 1LD)

G            = 0^2 1^2 0 1^4 0 1^2 0 1^6 0 1^2 0 1^5 0^2 1^2 0 1^5 0 1^2 0^2          (43 cells)
K(n,a,b,c,d) = 0^inf <F G 1^n 0 1^a 0110 1^b 0^6 1^c 0110 1111 0^6 1^d 0110 0110 111 0^inf
Even(n,x)    = K(n, x, (x+76)/2, 35, 18)

R1   C> 1 1         --> 1 0 C>             2 steps    C1 E1
R2b  0 1 0 B> 0 0 0 --> 0 B> 0 0 0 1 1     12 steps   B0 C0 A0 B1 C0 A1 D1 E0 F1 F1 F1 F0
     k-fold:  C> 1^(2k) --> (10)^k C>   (2k steps);   0 (10)^k B> 000 --> 0 B> 000 1^(2k)   (12k steps)

rule  from            to                            domain                                          steps                          trips
S     K(n,a,b,c,d) -> K(n+48,a-8,b+4,c,d+4)         n odd, a even >= 10, b even >= 6, c odd >= 7, d even >= 2   84n+84a+77b+70c+63d+13628   12
TE    K(n,4,b,35,d) -> K(n+556,b-86,82,d+51,18)     n odd, b even >= 88, d even >= 20                         966n+952b+812d+455332        138
TO    K(n,2,b,c,d) -> K(n+588,b+c-91,d+62,35,18)    n odd, b even >= 82, c odd >= 37, d even >= 18            1029n+1001b+987c+882d+458476 147
T6    K(n,6,b,c,d) -> K(n+592,b+c-91,d+62,35,18)    n odd, b even >= 82, c odd >= 35, d even >= 18            1029n+1008b+987c+882d+462814 147
T8    K(n,8,b,35,d) -> K(n+540,b-74,86,d+47,18)     n odd, b even >= 88, d even >= 20                         945n+938b+784d+446893        135

DC    Even(n,x) --S^((x-4)/8)--> K(.,4,x+36,35,(x+32)/2) --TE--> K(.,x-50,82,(x+134)/2,18)
                --S^((x-52)/8)--> K(.,2,(x+112)/2,(x+134)/2,(x-16)/2) --TO--> Even(n+12x+808, x+32)
      n odd, x = 4 mod 8, x >= 52; 3x+201 trips

start c0 -->(4,097,897) K(1959,34,68,45,18) --(S^4 TO S^4 T6 S^6 T8 S^5 T6 S^12 T8 S^9 TO S^17 T8 S^13 T6 S^22 TE S^16 T6)-->
      Even(12863,212) at step 153,126,993;  then DC forever (x = 212, 244, 276, ...)

2. Notation and families

Configurations. l <S r is state S reading the last cell of l; l S> r is state S reading the first cell of r. Words are written left to right. w^k is k copies of w, and 0^inf is the blank tail.

Rules. X --> Y between configurations means an exact run of the machine. A rule on partial configurations, such as R1, holds for every left side and every right side: the run never reads a cell outside the written part.

G is the 43-cell word of §1. It is the same at the start of every trip.

The family K. For n, a, b, c, d ≥ 0,

K(n,a,b,c,d) = 0^inf <F G 1^n 0 1^a 0 1^2 0 1^b 0^6 1^c 0 1^2 0 1^4 0^6 1^d 0 1^2 0^2 1^2 0 1^3 0^inf

The head is in state F on the 0 just left of G, and everything left of it is blank. The five 1-blocks have lengths n, a, b, c, d.

Particles. The short words between the blocks are, from left to right:

W = 0 (between n and a);
P1 = 0 1^2 0 (between a and b);
Q = 0^6 (between b and c);
Q' = 0 1^2 0 1^4 0^6 (between c and d);
E = 0 1^2 0^2 1^2 0 1^3 (after d, the right end).

Trip. A left record is a step at which the head visits a cell left of every cell visited before. Trips are counted by left records, two per trip, and K(...) is the configuration at the first left record of a trip. "j trips" means 2j left records.

Even(n, x) = K(n, x, (x+76)/2, 35, 18). It is used for n odd and x = 4 (mod 8), x ≥ 52.

3. Rules

3.1 The two shift rules

R1. For all left sides l and right sides r:

l C> 1 1 r  -->(2)  l 1 0 C> r          transitions C1 (1RE), E1 (0RC)

C reads 1, writes 1 and moves right in state E. E reads 1, writes 0 and moves right in state C. By induction on k, C> 1^(2k) --> (10)^k C> in 2k steps.

R2b. For all l and r:

l 0 1 0 B> 0 0 0 r  -->(12)  l 0 B> 0 0 0 1 1 r

Number the six written cells 0 to 5, so B starts on cell 3. The twelve transitions are:

step	transition	head after	cells 0..5 after
1	B0 = 0RC	4	010000
2	C0 = 1LA	3	010010
3	A0 = 1RB	4	010110
4	B1 = 1RC	5	010110
5	C0 = 1LA	4	010111
6	A1 = 1LD	3	010111
7	D1 = 1LE	2	010111
8	E0 = 1RF	3	011111
9	F1 = 0LF	2	011011
10	F1 = 0LF	1	010011
11	F1 = 0LF	0	000011
12	F0 = 0RB	1	000011

The head stays on cells 0..5, so the rule holds for every l and r.
Cell 0 must be 0. With a 1 there, step 12 is F1 = 0LF instead, and the run goes elsewhere (check SR.R2b_needs_the_0_on_the_left).
k-fold form. 0 (10)^k B> 000 --> 0 B> 000 1^(2k) in 12k steps, by induction on k. In 0 (10)^(k+1) B> 000 = 0 (10)^k 1 0 B> 000, the cell left of the last copy is the 0 of the copy before it (or the leading 0 when k = 0). So R2b applies to the last copy, giving 0 (10)^k B> 000 11, and the induction hypothesis finishes.

Not used: R2a. The observe stage also found 0 10 11 C> 0 --> 0 11 C> 0 11 (12 steps). It is true (check SR), but no proof below uses it: every macro rule closes with R1 and R2b alone (check MR.*_proved_with_R1_R2b_only).

3.2 How the macro rules are proved: symbolic execution

Each macro rule is a statement "for all values of the variables in the domain, start → end in exactly N steps". It is proved the way busycoq's ES_v3 es' proves block rules.

Symbolic tapes. A tape is a finite list of tokens between two blank tails: - a single 0 cell; - a run 1^L; - a block (10)^X.

L and X are linear forms in variables over ℕ with nonnegative coefficients, so each form is at least its constant term. Each domain variable is written by its parity and lower bound; for example a even ≥ 10 is a = 2a' + 10 with a' ≥ 0.

Moves. Each move is either an identity of tapes or an exact run of the machine.

move	what it does	why it is sound
peel	take one concrete cell off a run whose constant term is ≥ 1	`1^L = 1 1^(L-1)`, `(10)^X = 1 0 (10)^(X-1)` (read from the side the head is on)
merge	join adjacent 1-runs; `(10)^X 1 0 = (10)^(X+1)`	identity
step	one transition of the table on a concrete head cell	the table; a `---` stops the proof
R1	`C> 1^(2h+c) --> (10)^h C> 1^c` on the symbolic part of a run	§3.1, 2h steps
R2b	`0 (10)^X B> 000 --> 0 B> 000 1^(2X)` on the symbolic part of a block	§3.1, 12X steps; the 0 is the last cell of the block's constant copies, or the cell below the block must be a 0 cell or the blank tail
split	v = 0, or v = v' + 1	covers every v in ℕ

A split happens only when the head must read a cell of a run or block whose constant term is 0.

Leaves. Each branch runs until the stated number of left records. Then it must match the claimed end configuration exactly, as a word (after merging runs), with the head on the leftmost cell and in state F. The step count of a branch is a linear form, and it must equal the claimed formula. The rule holds because the branches cover the domain and each branch is a chain of exact runs and tape identities.

Testing the executor. We run the executor against direct simulation of the machine on random symbolic tapes, half of them set up so that a shift rule fires. The test compares tape, head, state and step count, for random branches and random values of the variables (check ENG).

The same test catches a variant of the executor that drops R2b's 0-on-the-left condition (ENG.teeth_unsound_variant_is_caught).

3.3 Rule S, trip by trip

S is the composition of twelve one-trip rules P1, ..., P12 between the phase families below. Every phase family has the form K_j = 0^inf <F G w_j 0^inf (G as in §1), and K_0 = K(n,a,b,c,d). All phases use the domain of S: n odd, a even ≥ 10, b even ≥ 6, c odd ≥ 7, d even ≥ 2.

j	w_j (the word after G)	steps of P(j+1): K_j → K_(j+1)
0	`1^n 0 1^a 0 1^2 0 1^b 0^6 1^c 0 1^2 0 1^4 0^6 1^d 0 1^2 0^2 1^2 0 1^3`	7n+7a+7b+14c+14d+1135
1	`1^(n+3) 0^3 1^(a-2) 0^6 1^(b-2) 0^2 1^2 0^2 1^(c+3) 0^3 1^2 0^2 1^2 0^2 1^(d+2) 0 1^2 0 1^6 0 1^2`	7n+14a+28b+14c+21d+1459
2	`1^(n+7) 0 1^2 0^2 1^(a-4) 0^2 1^4 0^6 1^(b-1) 0 1^2 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)`	7n+841
3	`1^(n+12) 0^2 1^(a-4) 0^2 1^4 0^6 1^(b-1) 0 1^2 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)`	7n+14a+7b+933
4	`1^(n+15) 0^2 1^(a-2) 0^12 1^(b-1) 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)`	7n+7a+897
5	`1^(n+19) 0 1^2 0 1^(a-4) 0 1^2 0^7 1^(b-1) 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)`	7n+925
6	`1^(n+24) 0 1^(a-4) 0 1^2 0^7 1^(b-1) 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)`	7n+7a+971
7	`1^(n+27) 0^3 1^(a-6) 0^2 1^4 0 1^(b+1) 0 1^(c-1) 0^6 1^6 0^6 1^(d+5)`	7n+14a+21b+28c+28d+2247
8	`1^(n+31) 0 1^2 0^2 1^(a-8) 0^2 1^(b+8) 0^2 1^(c-1) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3`	7n+1009
9	`1^(n+36) 0^2 1^(a-8) 0^2 1^(b+8) 0^2 1^(c-1) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3`	7n+14a+14b+14c+1081
10	`1^(n+39) 0^2 1^(a-6) 0^6 1^(b+4) 0^6 1^c 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3`	7n+7a+1037
11	`1^(n+43) 0 1^2 0 1^(a-8) 0 1^2 0 1^(b+4) 0^6 1^c 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3`	7n+1093
12	`1^(n+48) 0 1^(a-8) 0 1^2 0 1^(b+4) 0^6 1^c 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3`	(= K(n+48, a-8, b+4, c, d+4))

How to read the table: - A block crossed once in each direction costs 7 steps per cell: 1 per cell by R1 going right, 6 per cell by R2b going left. So the coefficients show how far each trip goes. Trips 3, 6, 9 and 12 cost 7n + const: the head crosses only the first block and turns back at the particle right after it. - The steps add up to S's formula: 84n+84a+77b+70c+63d+13628 (check PH.sum_of_phase_steps_is_S_formula).

Case split. Our executor splits once, on d: d = 2 or d ≥ 4. The split happens in trip 1, where the head reads the (10)^X block made from the d block cell by cell, and X may be 0. Both branches reach the same K_1, with the same step formula, so the table holds for all d ≥ 2. P2 to P12 need no split.

The split is a feature of our executor, not of the rule. A block can be rotated before the head reads it:

y (v y)^X  =  (y v)^X y

This moves a concrete cell from one side of the block to the other. An executor that rotates the (10)^X block this way, instead of splitting, proves P1 and S in one branch.

Domain. Each lower bound of S is sharp. One below it (a = 8, b = 4, c = 5 or d = 0, same parity), the result is not K(n+48,a-8,b+4,c,d+4) in any sampled case (check TEETH). a = 8 is where T8 takes over.

3.4 The collision rules TE, TO, T6, T8

When the second block is down to a ∈ {2, 4, 6, 8}, P1 has reached W, and S does not apply. One of four collision rules follows; their statements are in §1.

rule	when	trips	steps	executor splits	concrete steps	R1 / R2b uses
TE	a = 4, c = 35	138	966n+952b+812d+455332	none	556,314	390 / 390
TO	a = 2	147	1029n+1001b+987c+882d+458476	none	593,982	420 / 420
T6	a = 6	147	1029n+1008b+987c+882d+462814	none	596,920	421 / 421
T8	a = 8, c = 35	135	945n+938b+784d+446893	none	546,062	381 / 381

Each rule is proved by the executor of §3.2 over its whole domain, in one branch. TE and TO carry the double cycle (§4); T6 and T8 are used only in the opening (§5).

Trip by trip. Appendices A and B list the configuration after every trip of TE and of TO, with the steps of each trip. Each row is a one-trip rule, like P1, ..., P12 in §3.3: from the configuration of the row above, the machine reaches the configuration of the row in exactly the steps shown, for every value in the rule's domain.

Each row can be checked by hand the way §3.3 is read: R1 across a variable block going right (it leaves a (10)^X block), R2b across that block going left, and single transitions everywhere else. The step column adds up to the rule's step formula. The executor also proves every row on its own (check COL).

What happens in a collision. The tables show the following.

The variables occur only in the exponents of a few long 1-blocks: the first block, and the blocks that come from b and d (and c, in TO). Every other exponent is a constant.
Every trip crosses the first block: every step count contains 7n.
In TO, the b and c blocks merge into one block at trip 10.
From trip 12 on, the left part grows and shrinks as in S. At rows 12, 24, 36, ... the first block is 48 longer than 12 rows before, and the block that came from b (in TO, from b and c) is 8 shorter. At the end that block is the new second block: b - 86 in TE, b + c - 91 in TO.
Right of the d block, the word is a constant in every row. The head reaches it only on the trips whose step count contains d. On those trips it rebuilds the right end through the constant words shown, and the last row ends in E again.

T6 and T8 are used only at the seven concrete arguments of §5. Each of those uses is a finite run of the machine, and §5 confirms each one by direct simulation. Their trip tables have the same form as those of TE and TO and are not printed here.

The bounds are sufficient, not minimal. Only the domains stated are claimed. For example TE also holds at d = 18 in the sampled cases, which nothing below uses.

In Rocq the es' lemmas of §8 are the certificate for these rules. The tables are for a human reader. They also give the intermediate statements if a collision has to be cut into pieces (§8, risk "Size of the collision runs").

4. The double cycle

Lemma DC. Let n be odd, x = 4 (mod 8) and x ≥ 52. Write m = (x-4)/8 and m' = (x-52)/8. Then

Even(n, x)  -->  Even(n + 12x + 808, x + 32)

by the chain S^m, TE, S^(m'), TO, in 12m + 138 + 12m' + 147 = 3x + 201 trips.

Proof. We check each rule's domain at each application.

Step 1: S, m times. Before the i-th application (0 ≤ i < m) the configuration is

K(n + 48i, x - 8i, (x+76)/2 + 4i, 35, 18 + 4i)

n + 48i is odd.
x - 8i is even and at least x - 8(m-1) = 12 ≥ 10.
x + 76 = 0 (mod 8), so (x+76)/2 + 4i is a multiple of 4, hence even, and it is ≥ 6.
35 is odd and ≥ 7; 18 + 4i is even and ≥ 2.

After m applications, with 4m = (x-4)/2:

K(n + 48m, 4, x + 36, 35, (x+32)/2)

Step 2: TE. a = 4 and c = 35 hold. - b = x + 36 is even, and b ≥ 88 exactly when x ≥ 52. - x + 32 = 4 (mod 8), so d = (x+32)/2 = 2 (mod 4) is even, and d ≥ 20 since x ≥ 8.

The result is

Odd = K(n + 48m + 556, x - 50, 82, (x+134)/2, 18)

Step 3: S, m' times. Before the i-th application the configuration is K(·, x - 50 - 8i, 82 + 4i, (x+134)/2, 18 + 4i). - x - 50 - 8i is even and at least x - 50 - 8(m'-1) = 10. - x + 134 = 2 (mod 8), so c = (x+134)/2 = 1 (mod 4) is odd, and c ≥ 7. - b and d are even and ≥ 6 and ≥ 2.

After m' applications, with 4m' = (x-52)/2:

K(n + 48(m+m') + 556, 2, (x+112)/2, (x+134)/2, (x-16)/2)

Step 4: TO. a = 2 holds. - x + 112 = 4 (mod 8), so b = (x+112)/2 is even; b ≥ 82 exactly when x ≥ 52. - c = (x+134)/2 is odd (step 3) and ≥ 37. - x - 16 = 4 (mod 8), so d = (x-16)/2 is even; d ≥ 18 exactly when x ≥ 52.

TO gives K(n'', b + c - 91, d + 62, 35, 18), where

b + c - 91 = (x+112)/2 + (x+134)/2 - 91 = x + 32
d + 62     = (x-16)/2 + 62 = (x+108)/2 = ((x+32) + 76)/2
n''        = n + 48(m+m') + 556 + 588 = n + 6(x-4) + 6(x-52) + 1144 = n + 12x + 808

So the result is Even(n + 12x + 808, x + 32). ∎

Closure. n + 12x + 808 is odd, x + 32 = 4 (mod 8) and x + 32 ≥ 52. So DC applies again, forever. The Even family with these conditions needs no further invariant: the conditions are the whole domain of DC, and DC preserves them.

The general two-parameter map behind DC, (x, y) ↦ (3x/4 + y/2 + 13, x/4 + y/2 + 35) for K(n, x, y, 35, 18), is an observation of the observe stage. It keeps the line x - 2y = -76, which is the Even family. Nothing below uses the general map.

5. Initial segment (exact)

Opening. From the blank tape 0^inf A> 0^inf, the machine reaches K(1959,34,68,45,18) after exactly 4,097,897 steps, by direct simulation. This is the first left record whose configuration is in the K family (check OPEN.first_K_shaped_left_record_is_4097897).

Macro steps. From there, 20 macro steps reach Even(12863,212). Each row applies its rule as many times as shown. Every application is inside its rule's domain, and the step numbers are the sums of the step formulas (check OPEN). Each row's configuration was also confirmed by direct simulation at exactly that step.

after	rule	step	configuration
opening	(direct run)	4,097,897	K(1959,34,68,45,18)
1	S^4	4,883,657	K(2151,2,84,45,34)
2	TO	7,713,999	K(2739,38,96,35,18)
3	S^4	8,769,007	K(2931,6,112,35,34)
4	T6	12,425,249	K(3523,56,96,35,18)
5	S^6	14,435,489	K(3811,8,120,35,42)
6	T8	18,629,265	K(4351,46,86,89,18)
7	S^5	20,653,275	K(4591,6,106,89,38)
8	T6	26,068,435	K(5183,104,100,35,18)
9	S^12	31,955,395	K(5759,8,148,35,66)
10	T8	38,035,111	K(6299,74,86,113,18)
11	S^9	43,257,865	K(6731,2,122,113,54)
12	TO	50,923,821	K(7319,144,116,35,18)
13	S^17	62,558,553	K(8135,8,184,35,86)
14	T8	70,933,037	K(8675,110,86,133,18)
15	S^13	81,231,039	K(9299,6,138,133,70)
16	T6	91,594,639	K(9891,180,132,35,18)
17	S^22	111,713,639	K(10947,4,220,35,106)
18	TE	123,039,285	K(11503,134,82,157,18)
19	S^16	139,662,869	K(12271,6,146,157,82)
20	T6	153,126,993	K(12863,212,144,35,18)

The last row is Even(12863, 212): (212 + 76)/2 = 144, 12863 is odd, and 212 = 4 (mod 8) with 212 ≥ 52.

Before row 20 the run is not in the Even family. For example row 16, K(9891,180,132,35,18), has b = 132 where Even would need (180+76)/2 = 128. The early runs end with all four collision types, which is why the opening needs T6 and T8.

6. Coverage and progress

Coverage. There is no case analysis at the top level. The orbit from step 153,126,993 stays in the Even family (§4, closure), and every Even member satisfies the hypotheses of DC. Inside DC, each application's domain is checked in §4. The opening is a fixed finite list (§5).
Progress. Every macro rule takes at least 13,628 steps (S at its smallest), so each DC round takes at least one step. Progress is never a 0-step round.

7. Conclusion

7.1 Non-halting

c0 = 0^inf A> 0^inf reaches Even(12863, 212) at step 153,126,993 (§5).
Each Even member reaches the next by an exact run of at least one step (§4), and the next one is again an Even member.
So the run is infinite.

Why D0 is never read. D0 is the only undefined transition. D is entered only by A1 = 1LD, so the machine halts exactly when A reads a 1 that has a 0 on its left. Every step of the run is inside one of the exact runs above: the opening (a direct run that does not halt), the shift rules (their transitions are listed in §3.1, and D0 is not among them), and the executor's concrete steps (it stops with a failure on a ---, and no leaf ever recorded D0; check HALT).

7.2 Why it is not a cryptid

The top-level map is affine: (n, x) ↦ (n + 12x + 808, x + 32). All parities are fixed (n odd, x = 4 mod 8). No branch depends on the digits of a growing number. So ground rule 6 does not apply.

7.3 Siblings (remark, not checked here)

The observe stage found that 740 line 418 (this table started in C, mirrored) and line 636 (started in E) reach Even(12857, 212) at step 153,013,640 and Even(13299, 220) at step 163,638,058. Both x values are 4 (mod 8) and ≥ 52, so §4 would finish them too after their own openings. This file proves only line 214.

8. Formalization outline (Rocq)

The templates are TranslatedBellv5.v TM1 and Bouncer_v2.v TM1. All lemmas below are stated on half-length parameters, so that every block is [1;1]^^k. Write

Kr n a b c d  :=  K(2n+1, 2a, 2b, 2c+1, 2d)
  = 0inf <{{F}} G *> [1] *> [1;1]^^n *> [0] *> [1;1]^^a *> [0;1;1;0] *> [1;1]^^b *> [0;0;0;0;0;0]
         *> [1] *> [1;1]^^c *> [0;1;1;0;1;1;1;1;0;0;0;0;0;0] *> [1;1]^^d *> [0;1;1;0;0;1;1;0;1;1;1] *> 0inf
Ev N X  :=  Even(2N+1, 8X+52)  =  Kr N (4X+26) (2X+32) 17 9

Header. Definition tm := Eval compute in (TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF"). and the two notations, as in TranslatedBellv5.v.
Macro rules, each by es' (possibly after destruct), with the domain built into the arguments:

lemma	statement
`S_step n a b c d`	`Kr n (5+a) (3+b) (3+c) (1+d) -->+ Kr (24+n) (1+a) (5+b) (3+c) (3+d)`
`TE n b d`	`Kr n 2 (44+b) 17 (10+d) -->+ Kr (278+n) (1+b) 41 (35+d) 9`
`TO n b c d`	`Kr n 1 (41+b) (18+c) (9+d) -->+ Kr (294+n) (14+b+c) (40+d) 17 9`
`T6 n b c d`	`Kr n 3 (41+b) (17+c) (9+d) -->+ Kr (296+n) (13+b+c) (40+d) 17 9`
`T8 n b d`	`Kr n 4 (44+b) 17 (10+d) -->+ Kr (270+n) (7+b) 43 (33+d) 9`

S may not need a destruct: the split of §3.3 is a feature of our executor, and rotating the block avoids it. 3. Iterated S by ind k S_step:

S_iter k n a b c d : Kr n (4*k+1+a) (3+b) (3+c) (1+d) -->* Kr (24*k+n) (1+a) (2*k+3+b) (3+c) (2*k+1+d) 4. DC. Ev N X -->+ Ev (48*X+716+N) (4+X). X grows by 4 because x grows by 32. The proof is follow through four lemmas, with finish / lia on the arguments:

lemma	arguments
S_iter	k = X+6, a = 1, b = 2X+29, c = 14, d = 8
TE	b = 4X, d = 2X+11
S_iter	k = X, a = 0, b = 38, c = 2X+43, d = 8
TO	b = 2X, c = 2X+28, d = 2X

Opening. First init: c0 -->* Kr 979 17 34 22 9, by stepn 4097897%N. (Bouncer_v2.v TM1 runs stepn 4760139%N.)

Then follow the 20 rows of §5 with S_iter, TO, T6, T8 and TE at concrete arguments, ending at Ev 6431 20.

nonhalt. eapply multistep_nonhalt with the opening. Then apply progress_nonhalt_simple with

A := (nat * nat), C := fun '(N, X) => Ev N X, witness (48*X+716+N, 4+X)

No invariant is needed, because every pair (N, X) is in DC's domain (§6).

Risks.

R2b and ES_v3's shift-rule search. R2b reads the 0 left of each copy it crosses. ES_v3's try_sr looks for a rule in which the head, with a context behind it, crosses one copy without reading past it.

Grouped as (01)^k 0, R2b is a 4-cell composite 0 B> 000 crossing 01 copies, which is inside try_sr's search space. Whether es' finds it depends on how rw_lpow_rotate spells the block that R1 creates. This is untested.

Fallback: prove R1 and R2b as ind lemmas and cut each trip at block boundaries.

Size of the collision runs. TE, TO, T6 and T8 each have 550,000 to 600,000 concrete steps and about 800 shift-rule uses. es_v3_TL (10^6) bounds one concrete stretch, so the bound is fine; the vm_compute time is unknown.

Fallback: split each collision into 12-trip pieces, or single trips. For TE and TO, the rows of Appendices A and B are exactly the intermediate statements. The executor gives the same kind of table for T6 and T8.

S's case split. Possibly none is needed (§3.3). If es' gets stuck on S, destruct d gives the two branches of our executor.
Opening length. 4,097,897 steps is below Bouncer_v2.v's 4,760,139, so stepn should be fine.

Appendix A. TE trip by trip

The rule, for n odd, b even ≥ 88 and d even ≥ 20:

TE:  K(n,4,b,35,d)  -->  K(n+556, b-86, 82, d+51, 18)      in 966n+952b+812d+455332 steps, 138 trips

Row j gives the configuration after j trips, 0^inf <F G w 0^inf, by its word w after G. Row 0 is K(n,4,b,35,d), and row 138 is K(n+556, b-86, 82, d+51, 18).

The steps of trip j take row j-1 to row j. They add up to the step formula of TE. On the whole domain every exponent is at least 1, so each row is a word of the shape shown.

trip  steps of the trip      w (the word after G)
   0  -                      1^n 0 1^4 0 1^2 0 1^b 0^6 1^35 0 1^2 0 1^4 0^6 1^d 0 1^2 0^2 1^2 0 1^3
   1  7n+7b+14d+1653         1^(n+3) 0^3 1^2 0^6 1^(b-2) 0^2 1^2 0^2 1^38 0^3 1^2 0^2 1^2 0^2 1^(d+2) 0 1^2 0 1^6 0 1^2
   2  7n+21b+21d+1963        1^(n+7) 0 1^2 0 1^6 0 1^2 0 1^(b-1) 0 1^2 0 1^2 0 1^34 0^6 1^6 0^6 1^(d+5)
   3  7n+841                 1^(n+12) 0 1^6 0 1^2 0 1^(b-1) 0 1^2 0 1^2 0 1^34 0^6 1^6 0^6 1^(d+5)
   4  7n+7b+907              1^(n+15) 0^3 1^4 0^6 1^(b-1) 0 1^2 0 1^34 0^6 1^6 0^6 1^(d+5)
   5  7n+28b+28d+3227        1^(n+19) 0 1^2 0^2 1^2 0^2 1^4 0^6 1^(b-2) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3
   6  7n+925                 1^(n+24) 0^2 1^2 0^2 1^4 0^6 1^(b-2) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3
   7  7n+7b+1637             1^(n+27) 0^2 1^4 0^12 1^(b-4) 0^2 1^41 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3
   8  7n+1023                1^(n+31) 0 1^2 0 1^2 0 1^2 0^7 1^(b-4) 0^2 1^41 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3
   9  7n+1009                1^(n+36) 0 1^2 0 1^2 0^7 1^(b-4) 0^2 1^41 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3
  10  7n+1097                1^(n+39) 0^5 1^4 0 1^(b-2) 0^2 1^41 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3
  11  7n+1075                1^(n+43) 0 1^6 0 1^(b-2) 0^2 1^41 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3
  12  7n+1093                1^(n+52) 0 1^(b-2) 0^2 1^41 0 1^2 0 1^4 0^6 1^(d+4) 0 1^2 0^2 1^2 0 1^3
  13  7n+7b+28d+2321         1^(n+55) 0^3 1^(b-4) 0^2 1^42 0^2 1^2 0^6 1^4 0^6 1^(d+9) 0 1^2
  14  7n+14b+28d+3357        1^(n+59) 0 1^2 0^2 1^(b-6) 0^2 1^46 0^6 1^4 0^2 1^4 0^6 1^(d+8) 0^2 1^8
  15  7n+1205                1^(n+64) 0^2 1^(b-6) 0^2 1^46 0^6 1^4 0^2 1^4 0^6 1^(d+8) 0^2 1^8
  16  7n+14b+7d+2303         1^(n+67) 0^2 1^(b-4) 0^6 1^42 0^6 1^2 0^2 1^6 0^6 1^(d+6) 0^2 1^10 0^2 1^4 0 1^2
  17  7n+7b+1247             1^(n+71) 0 1^2 0 1^(b-6) 0 1^2 0 1^42 0^6 1^2 0^2 1^6 0^6 1^(d+6) 0^2 1^10 0^2 1^4 0 1^2
  18  7n+1289                1^(n+76) 0 1^(b-6) 0 1^2 0 1^42 0^6 1^2 0^2 1^6 0^6 1^(d+6) 0^2 1^10 0^2 1^4 0 1^2
  19  7n+7b+7d+2121          1^(n+79) 0^3 1^(b-8) 0^6 1^40 0^2 1^2 0^6 1^8 0^6 1^(d+4) 0^2 1^12 0^6 1^2 0 1^2
  20  7n+14b+14d+3351        1^(n+83) 0 1^2 0^2 1^(b-10) 0^2 1^4 0^6 1^41 0 1^2 0 1^6 0^2 1^2 0^2 1^(d+6) 0 1^2 0 1^12 0 1^2 0^3 1^4 0 1^2
  21  7n+1373                1^(n+88) 0^2 1^(b-10) 0^2 1^4 0^6 1^41 0 1^2 0 1^6 0^2 1^2 0^2 1^(d+6) 0 1^2 0 1^12 0 1^2 0^3 1^4 0 1^2
  22  7n+14b+1675            1^(n+91) 0^2 1^(b-8) 0^12 1^41 0 1^6 0^2 1^2 0^2 1^(d+6) 0 1^2 0 1^12 0 1^2 0^3 1^4 0 1^2
  23  7n+7b+1387             1^(n+95) 0 1^2 0 1^(b-10) 0 1^2 0^7 1^41 0 1^6 0^2 1^2 0^2 1^(d+6) 0 1^2 0 1^12 0 1^2 0^3 1^4 0 1^2
  24  7n+1457                1^(n+100) 0 1^(b-10) 0 1^2 0^7 1^41 0 1^6 0^2 1^2 0^2 1^(d+6) 0 1^2 0 1^12 0 1^2 0^3 1^4 0 1^2
  25  7n+7b+1461             1^(n+103) 0^3 1^(b-12) 0^2 1^4 0 1^43 0 1^6 0^2 1^2 0^2 1^(d+6) 0 1^2 0 1^12 0 1^2 0^3 1^4 0 1^2
  26  7n+14b+28d+3675        1^(n+107) 0 1^2 0^2 1^(b-14) 0^2 1^50 0^2 1^6 0 1^2 0 1^6 0 1^2 0 1^(d+14) 0 1^2 0^2 1^2 0^2 1^8 0 1^2
  27  7n+1541                1^(n+112) 0^2 1^(b-14) 0^2 1^50 0^2 1^6 0 1^2 0 1^6 0 1^2 0 1^(d+14) 0 1^2 0^2 1^2 0^2 1^8 0 1^2
  28  7n+14b+2215            1^(n+115) 0^2 1^(b-12) 0^6 1^46 0^6 1^9 0 1^2 0 1^(d+14) 0 1^2 0^2 1^2 0^2 1^8 0 1^2
  29  7n+7b+1527             1^(n+119) 0 1^2 0 1^(b-14) 0 1^2 0 1^46 0^6 1^9 0 1^2 0 1^(d+14) 0 1^2 0^2 1^2 0^2 1^8 0 1^2
  30  7n+1625                1^(n+124) 0 1^(b-14) 0 1^2 0 1^46 0^6 1^9 0 1^2 0 1^(d+14) 0 1^2 0^2 1^2 0^2 1^8 0 1^2
  31  7n+7b+7d+2317          1^(n+127) 0^3 1^(b-16) 0^6 1^44 0^2 1^2 0^2 1^12 0^3 1^(d+12) 0^2 1^6 0 1^2 0 1^7
  32  7n+14b+21d+4167        1^(n+131) 0 1^2 0^2 1^(b-18) 0^2 1^4 0^6 1^45 0 1^2 0 1^8 0^2 1^(d+14) 0 1^2 0 1^16 0 1^2 0 1^3
  33  7n+1709                1^(n+136) 0^2 1^(b-18) 0^2 1^4 0^6 1^45 0 1^2 0 1^8 0^2 1^(d+14) 0 1^2 0 1^16 0 1^2 0 1^3
  34  7n+14b+1927            1^(n+139) 0^2 1^(b-16) 0^12 1^45 0 1^8 0^2 1^(d+14) 0 1^2 0 1^16 0 1^2 0 1^3
  35  7n+7b+1667             1^(n+143) 0 1^2 0 1^(b-18) 0 1^2 0^7 1^45 0 1^8 0^2 1^(d+14) 0 1^2 0 1^16 0 1^2 0 1^3
  36  7n+1793                1^(n+148) 0 1^(b-18) 0 1^2 0^7 1^45 0 1^8 0^2 1^(d+14) 0 1^2 0 1^16 0 1^2 0 1^3
  37  7n+7b+1741             1^(n+151) 0^3 1^(b-20) 0^2 1^4 0 1^47 0 1^8 0^2 1^(d+14) 0 1^2 0 1^16 0 1^2 0 1^3
  38  7n+14b+49d+5007        1^(n+155) 0 1^2 0^2 1^(b-22) 0^2 1^54 0^2 1^8 0 1^2 0 1^(d+34) 0 1^2 0 1^8
  39  7n+1877                1^(n+160) 0^2 1^(b-22) 0^2 1^54 0^2 1^8 0 1^2 0 1^(d+34) 0 1^2 0 1^8
  40  7n+14b+2523            1^(n+163) 0^2 1^(b-20) 0^6 1^50 0^6 1^(d+39) 0 1^2 0 1^8
  41  7n+7b+1807             1^(n+167) 0 1^2 0 1^(b-22) 0 1^2 0 1^50 0^6 1^(d+39) 0 1^2 0 1^8
  42  7n+1961                1^(n+172) 0 1^(b-22) 0 1^2 0 1^50 0^6 1^(d+39) 0 1^2 0 1^8
  43  7n+7b+14d+3009         1^(n+175) 0^3 1^(b-24) 0^6 1^48 0^2 1^2 0^2 1^(d+42) 0^3 1^6 0^2 1^2 0^2 1^4 0 1^2
  44  7n+14b+14d+4541        1^(n+179) 0 1^2 0^2 1^(b-26) 0^2 1^4 0^6 1^49 0 1^2 0 1^(d+38) 0^2 1^8 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  45  7n+2045                1^(n+184) 0^2 1^(b-26) 0^2 1^4 0^6 1^49 0 1^2 0 1^(d+38) 0^2 1^8 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  46  7n+14b+2179            1^(n+187) 0^2 1^(b-24) 0^12 1^49 0 1^(d+38) 0^2 1^8 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  47  7n+7b+1947             1^(n+191) 0 1^2 0 1^(b-26) 0 1^2 0^7 1^49 0 1^(d+38) 0^2 1^8 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  48  7n+2129                1^(n+196) 0 1^(b-26) 0 1^2 0^7 1^49 0 1^(d+38) 0^2 1^8 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  49  7n+7b+2021             1^(n+199) 0^3 1^(b-28) 0^2 1^4 0 1^51 0 1^(d+38) 0^2 1^8 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  50  7n+14b+28d+5647        1^(n+203) 0 1^2 0^2 1^(b-30) 0^2 1^58 0^2 1^(d+38) 0 1^2 0 1^16 0 1^2 0 1^4 0^6 1^6 0 1^2
  51  7n+2213                1^(n+208) 0^2 1^(b-30) 0^2 1^58 0^2 1^(d+38) 0 1^2 0 1^16 0 1^2 0 1^4 0^6 1^6 0 1^2
  52  7n+14b+14d+3223        1^(n+211) 0^2 1^(b-28) 0^6 1^54 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^6 0 1^2
  53  7n+7b+2087             1^(n+215) 0 1^2 0 1^(b-30) 0 1^2 0 1^54 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^6 0 1^2
  54  7n+2297                1^(n+220) 0 1^(b-30) 0 1^2 0 1^54 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^6 0 1^2
  55  7n+7b+14d+3599         1^(n+223) 0^3 1^(b-32) 0^6 1^52 0^2 1^2 0^2 1^(d+54) 0^3 1^2 0^2 1^2 0^2 1^8 0 1^2 0 1^3
  56  7n+14b+14d+5025        1^(n+227) 0 1^2 0^2 1^(b-34) 0^2 1^4 0^6 1^53 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  57  7n+2381                1^(n+232) 0^2 1^(b-34) 0^2 1^4 0^6 1^53 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  58  7n+14b+2431            1^(n+235) 0^2 1^(b-32) 0^12 1^53 0 1^(d+50) 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  59  7n+7b+2227             1^(n+239) 0 1^2 0 1^(b-34) 0 1^2 0^7 1^53 0 1^(d+50) 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  60  7n+2465                1^(n+244) 0 1^(b-34) 0 1^2 0^7 1^53 0 1^(d+50) 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  61  7n+7b+2301             1^(n+247) 0^3 1^(b-36) 0^2 1^4 0 1^55 0 1^(d+50) 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  62  7n+14b+28d+6025        1^(n+251) 0 1^2 0^2 1^(b-38) 0^2 1^62 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^4 0^11 1^4 0 1^2
  63  7n+2549                1^(n+256) 0^2 1^(b-38) 0^2 1^62 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^4 0^11 1^4 0 1^2
  64  7n+14b+14d+3671        1^(n+259) 0^2 1^(b-36) 0^6 1^58 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^4 0^11 1^4 0 1^2
  65  7n+7b+2367             1^(n+263) 0 1^2 0 1^(b-38) 0 1^2 0 1^58 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^4 0^11 1^4 0 1^2
  66  7n+2633                1^(n+268) 0 1^(b-38) 0 1^2 0 1^58 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^4 0^11 1^4 0 1^2
  67  7n+7b+14d+3989         1^(n+271) 0^3 1^(b-40) 0^6 1^56 0^2 1^2 0^2 1^(d+54) 0^3 1^2 0^2 1^2 0^2 1^6 0 1^2 0^2 1^2 0 1^3 0 1^3
  68  7n+14b+14d+5249        1^(n+275) 0 1^2 0^2 1^(b-42) 0^2 1^4 0^6 1^57 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  69  7n+2717                1^(n+280) 0^2 1^(b-42) 0^2 1^4 0^6 1^57 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  70  7n+14b+2683            1^(n+283) 0^2 1^(b-40) 0^12 1^57 0 1^(d+50) 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  71  7n+7b+2507             1^(n+287) 0 1^2 0 1^(b-42) 0 1^2 0^7 1^57 0 1^(d+50) 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  72  7n+2801                1^(n+292) 0 1^(b-42) 0 1^2 0^7 1^57 0 1^(d+50) 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  73  7n+7b+2581             1^(n+295) 0^3 1^(b-44) 0^2 1^4 0 1^59 0 1^(d+50) 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  74  7n+14b+28d+6177        1^(n+299) 0 1^2 0^2 1^(b-46) 0^2 1^66 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^7 1^2 0 1^4 0^2 1^2 0^2 1^4 0 1^2
  75  7n+2885                1^(n+304) 0^2 1^(b-46) 0^2 1^66 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^7 1^2 0 1^4 0^2 1^2 0^2 1^4 0 1^2
  76  7n+14b+14d+3951        1^(n+307) 0^2 1^(b-44) 0^6 1^62 0^6 1^(d+51) 0 1^2 0 1^4 0^7 1^2 0 1^4 0^2 1^2 0^2 1^4 0 1^2
  77  7n+7b+2647             1^(n+311) 0 1^2 0 1^(b-46) 0 1^2 0 1^62 0^6 1^(d+51) 0 1^2 0 1^4 0^7 1^2 0 1^4 0^2 1^2 0^2 1^4 0 1^2
  78  7n+2969                1^(n+316) 0 1^(b-46) 0 1^2 0 1^62 0^6 1^(d+51) 0 1^2 0 1^4 0^7 1^2 0 1^4 0^2 1^2 0^2 1^4 0 1^2
  79  7n+7b+14d+4225         1^(n+319) 0^3 1^(b-48) 0^6 1^60 0^2 1^2 0^2 1^(d+54) 0^3 1^2 0^2 1^2 0^3 1^2 0^3 1^2 0^2 1^4 0^6 1^2 0 1^2
  80  7n+14b+14d+5761        1^(n+323) 0 1^2 0^2 1^(b-50) 0^2 1^4 0^6 1^61 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  81  7n+3053                1^(n+328) 0^2 1^(b-50) 0^2 1^4 0^6 1^61 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  82  7n+14b+2935            1^(n+331) 0^2 1^(b-48) 0^12 1^61 0 1^(d+50) 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  83  7n+7b+2787             1^(n+335) 0 1^2 0 1^(b-50) 0 1^2 0^7 1^61 0 1^(d+50) 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  84  7n+3137                1^(n+340) 0 1^(b-50) 0 1^2 0^7 1^61 0 1^(d+50) 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  85  7n+7b+2861             1^(n+343) 0^3 1^(b-52) 0^2 1^4 0 1^63 0 1^(d+50) 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  86  7n+14b+28d+6559        1^(n+347) 0 1^2 0^2 1^(b-54) 0^2 1^70 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^9 0 1^3
  87  7n+3221                1^(n+352) 0^2 1^(b-54) 0^2 1^70 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^9 0 1^3
  88  7n+14b+14d+4231        1^(n+355) 0^2 1^(b-52) 0^6 1^66 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^9 0 1^3
  89  7n+7b+2927             1^(n+359) 0 1^2 0 1^(b-54) 0 1^2 0 1^66 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^9 0 1^3
  90  7n+3305                1^(n+364) 0 1^(b-54) 0 1^2 0 1^66 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^9 0 1^3
  91  7n+7b+14d+4519         1^(n+367) 0^3 1^(b-56) 0^6 1^64 0^2 1^2 0^2 1^(d+54) 0^3 1^2 0^2 1^2 0^2 1^14 0 1^2
  92  7n+14b+14d+6085        1^(n+371) 0 1^2 0^2 1^(b-58) 0^2 1^4 0^6 1^65 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
  93  7n+3389                1^(n+376) 0^2 1^(b-58) 0^2 1^4 0^6 1^65 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
  94  7n+14b+3187            1^(n+379) 0^2 1^(b-56) 0^12 1^65 0 1^(d+50) 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
  95  7n+7b+3067             1^(n+383) 0 1^2 0 1^(b-58) 0 1^2 0^7 1^65 0 1^(d+50) 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
  96  7n+3473                1^(n+388) 0 1^(b-58) 0 1^2 0^7 1^65 0 1^(d+50) 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
  97  7n+7b+3141             1^(n+391) 0^3 1^(b-60) 0^2 1^4 0 1^67 0 1^(d+50) 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
  98  7n+14b+28d+7043        1^(n+395) 0 1^2 0^2 1^(b-62) 0^2 1^74 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^8 0^3 1^6 0 1^2
  99  7n+3557                1^(n+400) 0^2 1^(b-62) 0^2 1^74 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^8 0^3 1^6 0 1^2
 100  7n+14b+14d+4511        1^(n+403) 0^2 1^(b-60) 0^6 1^70 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^8 0^3 1^6 0 1^2
 101  7n+7b+3207             1^(n+407) 0 1^2 0 1^(b-62) 0 1^2 0 1^70 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^8 0^3 1^6 0 1^2
 102  7n+3641                1^(n+412) 0 1^(b-62) 0 1^2 0 1^70 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^8 0^3 1^6 0 1^2
 103  7n+7b+14d+5059         1^(n+415) 0^3 1^(b-64) 0^6 1^68 0^2 1^2 0^2 1^(d+54) 0^3 1^2 0^2 1^2 0^2 1^10 0 1^2 0 1^6 0^2 1^2 0^2 1^4 0 1^2
 104  7n+14b+14d+6367        1^(n+419) 0 1^2 0^2 1^(b-66) 0^2 1^4 0^6 1^69 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 105  7n+3725                1^(n+424) 0^2 1^(b-66) 0^2 1^4 0^6 1^69 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 106  7n+14b+3439            1^(n+427) 0^2 1^(b-64) 0^12 1^69 0 1^(d+50) 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 107  7n+7b+3347             1^(n+431) 0 1^2 0 1^(b-66) 0 1^2 0^7 1^69 0 1^(d+50) 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 108  7n+3809                1^(n+436) 0 1^(b-66) 0 1^2 0^7 1^69 0 1^(d+50) 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 109  7n+7b+3421             1^(n+439) 0^3 1^(b-68) 0^2 1^4 0 1^71 0 1^(d+50) 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 110  7n+14b+28d+7361        1^(n+443) 0 1^2 0^2 1^(b-70) 0^2 1^78 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^10 0^3 1^4 0^2 1^4 0 1^2
 111  7n+3893                1^(n+448) 0^2 1^(b-70) 0^2 1^78 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^10 0^3 1^4 0^2 1^4 0 1^2
 112  7n+14b+14d+4791        1^(n+451) 0^2 1^(b-68) 0^6 1^74 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^10 0^3 1^4 0^2 1^4 0 1^2
 113  7n+7b+3487             1^(n+455) 0 1^2 0 1^(b-70) 0 1^2 0 1^74 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^10 0^3 1^4 0^2 1^4 0 1^2
 114  7n+3977                1^(n+460) 0 1^(b-70) 0 1^2 0 1^74 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^10 0^3 1^4 0^2 1^4 0 1^2
 115  7n+7b+14d+5277         1^(n+463) 0^3 1^(b-72) 0^6 1^72 0^2 1^2 0^2 1^(d+54) 0^3 1^2 0^2 1^2 0^2 1^12 0 1^2 0 1^5 0 1^3
 116  7n+14b+14d+6713        1^(n+467) 0 1^2 0^2 1^(b-74) 0^2 1^4 0^6 1^73 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 117  7n+4061                1^(n+472) 0^2 1^(b-74) 0^2 1^4 0^6 1^73 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 118  7n+14b+3691            1^(n+475) 0^2 1^(b-72) 0^12 1^73 0 1^(d+50) 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 119  7n+7b+3627             1^(n+479) 0 1^2 0 1^(b-74) 0 1^2 0^7 1^73 0 1^(d+50) 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 120  7n+4145                1^(n+484) 0 1^(b-74) 0 1^2 0^7 1^73 0 1^(d+50) 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 121  7n+7b+3701             1^(n+487) 0^3 1^(b-76) 0^2 1^4 0 1^75 0 1^(d+50) 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 122  7n+14b+28d+7771        1^(n+491) 0 1^2 0^2 1^(b-78) 0^2 1^82 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^10 0^2 1^6 0 1^2 0 1^3
 123  7n+4229                1^(n+496) 0^2 1^(b-78) 0^2 1^82 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^10 0^2 1^6 0 1^2 0 1^3
 124  7n+14b+14d+5071        1^(n+499) 0^2 1^(b-76) 0^6 1^78 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^10 0^2 1^6 0 1^2 0 1^3
 125  7n+7b+3767             1^(n+503) 0 1^2 0 1^(b-78) 0 1^2 0 1^78 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^10 0^2 1^6 0 1^2 0 1^3
 126  7n+4313                1^(n+508) 0 1^(b-78) 0 1^2 0 1^78 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^10 0^2 1^6 0 1^2 0 1^3
 127  7n+7b+14d+5675         1^(n+511) 0^3 1^(b-80) 0^6 1^76 0^2 1^2 0^2 1^(d+54) 0^3 1^2 0^2 1^2 0^2 1^12 0 1^2 0 1^10 0 1^2
 128  7n+14b+14d+7059        1^(n+515) 0 1^2 0^2 1^(b-82) 0^2 1^4 0^6 1^77 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^19
 129  7n+4397                1^(n+520) 0^2 1^(b-82) 0^2 1^4 0^6 1^77 0 1^2 0 1^(d+50) 0^6 1^6 0^6 1^19
 130  7n+14b+3943            1^(n+523) 0^2 1^(b-80) 0^12 1^77 0 1^(d+50) 0^6 1^6 0^6 1^19
 131  7n+7b+3907             1^(n+527) 0 1^2 0 1^(b-82) 0 1^2 0^7 1^77 0 1^(d+50) 0^6 1^6 0^6 1^19
 132  7n+4481                1^(n+532) 0 1^(b-82) 0 1^2 0^7 1^77 0 1^(d+50) 0^6 1^6 0^6 1^19
 133  7n+7b+3981             1^(n+535) 0^3 1^(b-84) 0^2 1^4 0 1^79 0 1^(d+50) 0^6 1^6 0^6 1^19
 134  7n+14b+28d+8169        1^(n+539) 0 1^2 0^2 1^(b-86) 0^2 1^86 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^18 0 1^2 0^2 1^2 0 1^3
 135  7n+4565                1^(n+544) 0^2 1^(b-86) 0^2 1^86 0^2 1^(d+50) 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^18 0 1^2 0^2 1^2 0 1^3
 136  7n+14b+14d+5351        1^(n+547) 0^2 1^(b-84) 0^6 1^82 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^18 0 1^2 0^2 1^2 0 1^3
 137  7n+7b+4047             1^(n+551) 0 1^2 0 1^(b-86) 0 1^2 0 1^82 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^18 0 1^2 0^2 1^2 0 1^3
 138  7n+4649                1^(n+556) 0 1^(b-86) 0 1^2 0 1^82 0^6 1^(d+51) 0 1^2 0 1^4 0^6 1^18 0 1^2 0^2 1^2 0 1^3

Appendix B. TO trip by trip

The rule, for n odd, b even ≥ 82, c odd ≥ 37 and d even ≥ 18:

TO:  K(n,2,b,c,d)  -->  K(n+588, b+c-91, d+62, 35, 18)     in 1029n+1001b+987c+882d+458476 steps, 147 trips

The rows are read as in Appendix A. Row 0 is K(n,2,b,c,d), and row 147 is K(n+588, b+c-91, d+62, 35, 18).

trip  steps of the trip      w (the word after G)
   0  -                      1^n 0 1^2 0 1^2 0 1^b 0^6 1^c 0 1^2 0 1^4 0^6 1^d 0 1^2 0^2 1^2 0 1^3
   1  7n+7b+14c+14d+1149     1^(n+3) 0^9 1^(b-2) 0^2 1^2 0^2 1^(c+3) 0^3 1^2 0^2 1^2 0^2 1^(d+2) 0 1^2 0 1^6 0 1^2
   2  7n+823                 1^(n+7) 0 1^2 0^4 1^(b-2) 0^2 1^2 0^2 1^(c+3) 0^3 1^2 0^2 1^2 0^2 1^(d+2) 0 1^2 0 1^6 0 1^2
   3  7n+841                 1^(n+12) 0^4 1^(b-2) 0^2 1^2 0^2 1^(c+3) 0^3 1^2 0^2 1^2 0^2 1^(d+2) 0 1^2 0 1^6 0 1^2
   4  7n+14b+7c+14d+1226     1^(n+15) 0^2 1^2 0^6 1^(b-6) 0^2 1^(c+6) 0 1^2 0 1^8 0 1^2 0 1^(d+5) 0 1^2
   5  7n+925                 1^(n+19) 0 1^2 0^2 1^2 0 1^(b-6) 0^2 1^(c+6) 0 1^2 0 1^8 0 1^2 0 1^(d+5) 0 1^2
   6  7n+925                 1^(n+24) 0^2 1^2 0 1^(b-6) 0^2 1^(c+6) 0 1^2 0 1^8 0 1^2 0 1^(d+5) 0 1^2
   7  7n+7b+7c+7d+1140       1^(n+27) 0^2 1^(b-2) 0 1^2 0 1^(c+3) 0^6 1^6 0^6 1^(d+5)
   8  7n+7b+971              1^(n+31) 0 1^2 0 1^(b-3) 0 1^(c+3) 0^6 1^6 0^6 1^(d+5)
   9  7n+1009                1^(n+36) 0 1^(b-3) 0 1^(c+3) 0^6 1^6 0^6 1^(d+5)
  10  7n+7b+1017             1^(n+39) 0^3 1^(b+c-2) 0^6 1^6 0^6 1^(d+5)
  11  7n+14b+14c+14d+1307    1^(n+43) 0 1^2 0^2 1^(b+c-3) 0^6 1^4 0^2 1^2 0^2 1^(d+9)
  12  7n+1093                1^(n+48) 0^2 1^(b+c-3) 0^6 1^4 0^2 1^2 0^2 1^(d+9)
  13  7n+14b+14c+14d+1653    1^(n+51) 0^2 1^(b+c-1) 0^6 1^2 0^2 1^4 0^6 1^(d+4) 0^2 1^4 0^6 1^2 0 1^2
  14  7n+7b+7c+1156          1^(n+55) 0 1^2 0 1^(b+c-3) 0 1^2 0 1^2 0^2 1^4 0^6 1^(d+4) 0^2 1^4 0^6 1^2 0 1^2
  15  7n+1177                1^(n+60) 0 1^(b+c-3) 0 1^2 0 1^2 0^2 1^4 0^6 1^(d+4) 0^2 1^4 0^6 1^2 0 1^2
  16  7n+7b+7c+1266          1^(n+63) 0^3 1^(b+c-5) 0^5 1^8 0 1^2 0 1^(d+4) 0^2 1^4 0^6 1^2 0 1^2
  17  7n+14b+14c+28d+2447    1^(n+67) 0 1^2 0^2 1^(b+c-7) 0^2 1^4 0^6 1^8 0 1^2 0 1^(d+2) 0 1^6 0 1^2 0 1^4 0^2 1^4 0 1^2
  18  7n+1261                1^(n+72) 0^2 1^(b+c-7) 0^2 1^4 0^6 1^8 0 1^2 0 1^(d+2) 0 1^6 0 1^2 0 1^4 0^2 1^4 0 1^2
  19  7n+14b+14c+7d+1589     1^(n+75) 0^2 1^(b+c-5) 0^12 1^6 0^6 1^(d) 0^3 1^4 0^6 1^2 0^2 1^8 0 1^2
  20  7n+7b+7c+1296          1^(n+79) 0 1^2 0 1^(b+c-7) 0 1^2 0^7 1^6 0^6 1^(d) 0^3 1^4 0^6 1^2 0^2 1^8 0 1^2
  21  7n+1345                1^(n+84) 0 1^(b+c-7) 0 1^2 0^7 1^6 0^6 1^(d) 0^3 1^4 0^6 1^2 0^2 1^8 0 1^2
  22  7n+7b+7c+1370          1^(n+87) 0^3 1^(b+c-9) 0^2 1^4 0 1^8 0^6 1^(d) 0^3 1^4 0^6 1^2 0^2 1^8 0 1^2
  23  7n+14b+14c+1739        1^(n+91) 0 1^2 0^2 1^(b+c-11) 0^2 1^(d+17) 0^3 1^4 0^6 1^2 0^2 1^8 0 1^2
  24  7n+1429                1^(n+96) 0^2 1^(b+c-11) 0^2 1^(d+17) 0^3 1^4 0^6 1^2 0^2 1^8 0 1^2
  25  7n+14b+14c+14d+1835    1^(n+99) 0^2 1^(b+c-9) 0^6 1^(d+12) 0^2 1^11 0^2 1^8 0 1^2
  26  7n+7b+7c+1436          1^(n+103) 0 1^2 0 1^(b+c-11) 0 1^2 0 1^(d+12) 0^2 1^11 0^2 1^8 0 1^2
  27  7n+1513                1^(n+108) 0 1^(b+c-11) 0 1^2 0 1^(d+12) 0^2 1^11 0^2 1^8 0 1^2
  28  7n+7b+7c+7d+2192       1^(n+111) 0^3 1^(b+c-13) 0^6 1^(d+10) 0^2 1^12 0^2 1^16 0 1^2
  29  7n+14b+14c+28d+2477    1^(n+115) 0 1^2 0^2 1^(b+c-15) 0^2 1^4 0^6 1^(d+21) 0 1^2 0 1^14 0 1^2
  30  7n+1597                1^(n+120) 0^2 1^(b+c-15) 0^2 1^4 0^6 1^(d+21) 0 1^2 0 1^14 0 1^2
  31  7n+14b+14c+7d+1689     1^(n+123) 0^2 1^(b+c-13) 0^12 1^(d+21) 0 1^14 0 1^2
  32  7n+7b+7c+1576          1^(n+127) 0 1^2 0 1^(b+c-15) 0 1^2 0^7 1^(d+21) 0 1^14 0 1^2
  33  7n+1681                1^(n+132) 0 1^(b+c-15) 0 1^2 0^7 1^(d+21) 0 1^14 0 1^2
  34  7n+7b+7c+1650          1^(n+135) 0^3 1^(b+c-17) 0^2 1^4 0 1^(d+23) 0 1^14 0 1^2
  35  7n+14b+14c+21d+3093    1^(n+139) 0 1^2 0^2 1^(b+c-19) 0^2 1^(d+30) 0^2 1^14 0 1^2 0 1^11
  36  7n+1765                1^(n+144) 0^2 1^(b+c-19) 0^2 1^(d+30) 0^2 1^14 0 1^2 0 1^11
  37  7n+14b+14c+14d+2201    1^(n+147) 0^2 1^(b+c-17) 0^6 1^(d+26) 0^6 1^22
  38  7n+7b+7c+1716          1^(n+151) 0 1^2 0 1^(b+c-19) 0 1^2 0 1^(d+26) 0^6 1^22
  39  7n+1849                1^(n+156) 0 1^(b+c-19) 0 1^2 0 1^(d+26) 0^6 1^22
  40  7n+7b+7c+7d+2498       1^(n+159) 0^3 1^(b+c-21) 0^6 1^(d+24) 0^2 1^2 0^2 1^24 0 1^2 0^2 1^2 0 1^3
  41  7n+14b+14c+28d+3003    1^(n+163) 0 1^2 0^2 1^(b+c-23) 0^2 1^4 0^6 1^(d+25) 0 1^2 0 1^22 0 1^2 0 1^2
  42  7n+1933                1^(n+168) 0^2 1^(b+c-23) 0^2 1^4 0^6 1^(d+25) 0 1^2 0 1^22 0 1^2 0 1^2
  43  7n+14b+14c+7d+1941     1^(n+171) 0^2 1^(b+c-21) 0^12 1^(d+25) 0 1^22 0 1^2 0 1^2
  44  7n+7b+7c+1856          1^(n+175) 0 1^2 0 1^(b+c-23) 0 1^2 0^7 1^(d+25) 0 1^22 0 1^2 0 1^2
  45  7n+2017                1^(n+180) 0 1^(b+c-23) 0 1^2 0^7 1^(d+25) 0 1^22 0 1^2 0 1^2
  46  7n+7b+7c+1930          1^(n+183) 0^3 1^(b+c-25) 0^2 1^4 0 1^(d+27) 0 1^22 0 1^2 0 1^2
  47  7n+14b+14c+21d+3865    1^(n+187) 0 1^2 0^2 1^(b+c-27) 0^2 1^(d+34) 0^2 1^22 0 1^2 0 1^2 0 1^2 0 1^10
  48  7n+2101                1^(n+192) 0^2 1^(b+c-27) 0^2 1^(d+34) 0^2 1^22 0 1^2 0 1^2 0 1^2 0 1^10
  49  7n+14b+14c+14d+2593    1^(n+195) 0^2 1^(b+c-25) 0^6 1^(d+30) 0^6 1^21 0 1^2 0 1^10
  50  7n+7b+7c+1996          1^(n+199) 0 1^2 0 1^(b+c-27) 0 1^2 0 1^(d+30) 0^6 1^21 0 1^2 0 1^10
  51  7n+2185                1^(n+204) 0 1^(b+c-27) 0 1^2 0 1^(d+30) 0^6 1^21 0 1^2 0 1^10
  52  7n+7b+7c+7d+2820       1^(n+207) 0^3 1^(b+c-29) 0^6 1^(d+28) 0^2 1^2 0^2 1^24 0^3 1^8 0^2 1^2 0^2 1^4 0 1^2
  53  7n+14b+14c+28d+3925    1^(n+211) 0 1^2 0^2 1^(b+c-31) 0^2 1^4 0^6 1^(d+29) 0 1^2 0 1^20 0^2 1^10 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  54  7n+2269                1^(n+216) 0^2 1^(b+c-31) 0^2 1^4 0^6 1^(d+29) 0 1^2 0 1^20 0^2 1^10 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  55  7n+14b+14c+7d+2193     1^(n+219) 0^2 1^(b+c-29) 0^12 1^(d+29) 0 1^20 0^2 1^10 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  56  7n+7b+7c+2136          1^(n+223) 0 1^2 0 1^(b+c-31) 0 1^2 0^7 1^(d+29) 0 1^20 0^2 1^10 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  57  7n+2353                1^(n+228) 0 1^(b+c-31) 0 1^2 0^7 1^(d+29) 0 1^20 0^2 1^10 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  58  7n+7b+7c+2210          1^(n+231) 0^3 1^(b+c-33) 0^2 1^4 0 1^(d+31) 0 1^20 0^2 1^10 0 1^2 0 1^4 0 1^2 0^3 1^4 0 1^2
  59  7n+14b+14c+21d+4975    1^(n+235) 0 1^2 0^2 1^(b+c-35) 0^2 1^(d+38) 0^2 1^20 0 1^2 0 1^18 0 1^2 0 1^4 0^6 1^6 0 1^2
  60  7n+2437                1^(n+240) 0^2 1^(b+c-35) 0^2 1^(d+38) 0^2 1^20 0 1^2 0 1^18 0 1^2 0 1^4 0^6 1^6 0 1^2
  61  7n+14b+14c+14d+2845    1^(n+243) 0^2 1^(b+c-33) 0^6 1^(d+34) 0^6 1^35 0 1^2 0 1^4 0^6 1^6 0 1^2
  62  7n+7b+7c+2276          1^(n+247) 0 1^2 0 1^(b+c-35) 0 1^2 0 1^(d+34) 0^6 1^35 0 1^2 0 1^4 0^6 1^6 0 1^2
  63  7n+2521                1^(n+252) 0 1^(b+c-35) 0 1^2 0 1^(d+34) 0^6 1^35 0 1^2 0 1^4 0^6 1^6 0 1^2
  64  7n+7b+7c+7d+3424       1^(n+255) 0^3 1^(b+c-37) 0^6 1^(d+32) 0^2 1^2 0^2 1^38 0^3 1^2 0^2 1^2 0^2 1^8 0 1^2 0 1^3
  65  7n+14b+14c+28d+4395    1^(n+259) 0 1^2 0^2 1^(b+c-39) 0^2 1^4 0^6 1^(d+33) 0 1^2 0 1^34 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  66  7n+2605                1^(n+264) 0^2 1^(b+c-39) 0^2 1^4 0^6 1^(d+33) 0 1^2 0 1^34 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  67  7n+14b+14c+7d+2445     1^(n+267) 0^2 1^(b+c-37) 0^12 1^(d+33) 0 1^34 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  68  7n+7b+7c+2416          1^(n+271) 0 1^2 0 1^(b+c-39) 0 1^2 0^7 1^(d+33) 0 1^34 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  69  7n+2689                1^(n+276) 0 1^(b+c-39) 0 1^2 0^7 1^(d+33) 0 1^34 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  70  7n+7b+7c+2490          1^(n+279) 0^3 1^(b+c-41) 0^2 1^4 0 1^(d+35) 0 1^34 0^6 1^6 0^6 1^6 0^2 1^2 0^2 1^4 0 1^2
  71  7n+14b+14c+21d+5311    1^(n+283) 0 1^2 0^2 1^(b+c-43) 0^2 1^(d+42) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^4 0^11 1^4 0 1^2
  72  7n+2773                1^(n+288) 0^2 1^(b+c-43) 0^2 1^(d+42) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^4 0^11 1^4 0 1^2
  73  7n+14b+14c+14d+3321    1^(n+291) 0^2 1^(b+c-41) 0^6 1^(d+38) 0^6 1^35 0 1^2 0 1^4 0^6 1^4 0^11 1^4 0 1^2
  74  7n+7b+7c+2556          1^(n+295) 0 1^2 0 1^(b+c-43) 0 1^2 0 1^(d+38) 0^6 1^35 0 1^2 0 1^4 0^6 1^4 0^11 1^4 0 1^2
  75  7n+2857                1^(n+300) 0 1^(b+c-43) 0 1^2 0 1^(d+38) 0^6 1^35 0 1^2 0 1^4 0^6 1^4 0^11 1^4 0 1^2
  76  7n+7b+7c+7d+3814       1^(n+303) 0^3 1^(b+c-45) 0^6 1^(d+36) 0^2 1^2 0^2 1^38 0^3 1^2 0^2 1^2 0^2 1^6 0 1^2 0^2 1^2 0 1^3 0 1^3
  77  7n+14b+14c+28d+4619    1^(n+307) 0 1^2 0^2 1^(b+c-47) 0^2 1^4 0^6 1^(d+37) 0 1^2 0 1^34 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  78  7n+2941                1^(n+312) 0^2 1^(b+c-47) 0^2 1^4 0^6 1^(d+37) 0 1^2 0 1^34 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  79  7n+14b+14c+7d+2697     1^(n+315) 0^2 1^(b+c-45) 0^12 1^(d+37) 0 1^34 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  80  7n+7b+7c+2696          1^(n+319) 0 1^2 0 1^(b+c-47) 0 1^2 0^7 1^(d+37) 0 1^34 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  81  7n+3025                1^(n+324) 0 1^(b+c-47) 0 1^2 0^7 1^(d+37) 0 1^34 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  82  7n+7b+7c+2770          1^(n+327) 0^3 1^(b+c-49) 0^2 1^4 0 1^(d+39) 0 1^34 0^6 1^6 0^6 1^2 0^9 1^2 0 1^2
  83  7n+14b+14c+21d+5463    1^(n+331) 0 1^2 0^2 1^(b+c-51) 0^2 1^(d+46) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^7 1^2 0 1^4 0^2 1^2 0^2 1^4 0 1^2
  84  7n+3109                1^(n+336) 0^2 1^(b+c-51) 0^2 1^(d+46) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^7 1^2 0 1^4 0^2 1^2 0^2 1^4 0 1^2
  85  7n+14b+14c+14d+3601    1^(n+339) 0^2 1^(b+c-49) 0^6 1^(d+42) 0^6 1^35 0 1^2 0 1^4 0^7 1^2 0 1^4 0^2 1^2 0^2 1^4 0 1^2
  86  7n+7b+7c+2836          1^(n+343) 0 1^2 0 1^(b+c-51) 0 1^2 0 1^(d+42) 0^6 1^35 0 1^2 0 1^4 0^7 1^2 0 1^4 0^2 1^2 0^2 1^4 0 1^2
  87  7n+3193                1^(n+348) 0 1^(b+c-51) 0 1^2 0 1^(d+42) 0^6 1^35 0 1^2 0 1^4 0^7 1^2 0 1^4 0^2 1^2 0^2 1^4 0 1^2
  88  7n+7b+7c+7d+4050       1^(n+351) 0^3 1^(b+c-53) 0^6 1^(d+40) 0^2 1^2 0^2 1^38 0^3 1^2 0^2 1^2 0^3 1^2 0^3 1^2 0^2 1^4 0^6 1^2 0 1^2
  89  7n+14b+14c+28d+5131    1^(n+355) 0 1^2 0^2 1^(b+c-55) 0^2 1^4 0^6 1^(d+41) 0 1^2 0 1^34 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  90  7n+3277                1^(n+360) 0^2 1^(b+c-55) 0^2 1^4 0^6 1^(d+41) 0 1^2 0 1^34 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  91  7n+14b+14c+7d+2949     1^(n+363) 0^2 1^(b+c-53) 0^12 1^(d+41) 0 1^34 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  92  7n+7b+7c+2976          1^(n+367) 0 1^2 0 1^(b+c-55) 0 1^2 0^7 1^(d+41) 0 1^34 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  93  7n+3361                1^(n+372) 0 1^(b+c-55) 0 1^2 0^7 1^(d+41) 0 1^34 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  94  7n+7b+7c+3050          1^(n+375) 0^3 1^(b+c-57) 0^2 1^4 0 1^(d+43) 0 1^34 0^6 1^6 0^6 1^9 0 1^2 0 1^2
  95  7n+14b+14c+21d+5845    1^(n+379) 0 1^2 0^2 1^(b+c-59) 0^2 1^(d+50) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^9 0 1^3
  96  7n+3445                1^(n+384) 0^2 1^(b+c-59) 0^2 1^(d+50) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^9 0 1^3
  97  7n+14b+14c+14d+3881    1^(n+387) 0^2 1^(b+c-57) 0^6 1^(d+46) 0^6 1^35 0 1^2 0 1^4 0^6 1^9 0 1^3
  98  7n+7b+7c+3116          1^(n+391) 0 1^2 0 1^(b+c-59) 0 1^2 0 1^(d+46) 0^6 1^35 0 1^2 0 1^4 0^6 1^9 0 1^3
  99  7n+3529                1^(n+396) 0 1^(b+c-59) 0 1^2 0 1^(d+46) 0^6 1^35 0 1^2 0 1^4 0^6 1^9 0 1^3
 100  7n+7b+7c+7d+4344       1^(n+399) 0^3 1^(b+c-61) 0^6 1^(d+44) 0^2 1^2 0^2 1^38 0^3 1^2 0^2 1^2 0^2 1^14 0 1^2
 101  7n+14b+14c+28d+5455    1^(n+403) 0 1^2 0^2 1^(b+c-63) 0^2 1^4 0^6 1^(d+45) 0 1^2 0 1^34 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
 102  7n+3613                1^(n+408) 0^2 1^(b+c-63) 0^2 1^4 0^6 1^(d+45) 0 1^2 0 1^34 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
 103  7n+14b+14c+7d+3201     1^(n+411) 0^2 1^(b+c-61) 0^12 1^(d+45) 0 1^34 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
 104  7n+7b+7c+3256          1^(n+415) 0 1^2 0 1^(b+c-63) 0 1^2 0^7 1^(d+45) 0 1^34 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
 105  7n+3697                1^(n+420) 0 1^(b+c-63) 0 1^2 0^7 1^(d+45) 0 1^34 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
 106  7n+7b+7c+3330          1^(n+423) 0^3 1^(b+c-65) 0^2 1^4 0 1^(d+47) 0 1^34 0^6 1^6 0^6 1^10 0^2 1^4 0 1^2
 107  7n+14b+14c+21d+6329    1^(n+427) 0 1^2 0^2 1^(b+c-67) 0^2 1^(d+54) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^8 0^3 1^6 0 1^2
 108  7n+3781                1^(n+432) 0^2 1^(b+c-67) 0^2 1^(d+54) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^8 0^3 1^6 0 1^2
 109  7n+14b+14c+14d+4161    1^(n+435) 0^2 1^(b+c-65) 0^6 1^(d+50) 0^6 1^35 0 1^2 0 1^4 0^6 1^8 0^3 1^6 0 1^2
 110  7n+7b+7c+3396          1^(n+439) 0 1^2 0 1^(b+c-67) 0 1^2 0 1^(d+50) 0^6 1^35 0 1^2 0 1^4 0^6 1^8 0^3 1^6 0 1^2
 111  7n+3865                1^(n+444) 0 1^(b+c-67) 0 1^2 0 1^(d+50) 0^6 1^35 0 1^2 0 1^4 0^6 1^8 0^3 1^6 0 1^2
 112  7n+7b+7c+7d+4884       1^(n+447) 0^3 1^(b+c-69) 0^6 1^(d+48) 0^2 1^2 0^2 1^38 0^3 1^2 0^2 1^2 0^2 1^10 0 1^2 0 1^6 0^2 1^2 0^2 1^4 0 1^2
 113  7n+14b+14c+28d+5737    1^(n+451) 0 1^2 0^2 1^(b+c-71) 0^2 1^4 0^6 1^(d+49) 0 1^2 0 1^34 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 114  7n+3949                1^(n+456) 0^2 1^(b+c-71) 0^2 1^4 0^6 1^(d+49) 0 1^2 0 1^34 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 115  7n+14b+14c+7d+3453     1^(n+459) 0^2 1^(b+c-69) 0^12 1^(d+49) 0 1^34 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 116  7n+7b+7c+3536          1^(n+463) 0 1^2 0 1^(b+c-71) 0 1^2 0^7 1^(d+49) 0 1^34 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 117  7n+4033                1^(n+468) 0 1^(b+c-71) 0 1^2 0^7 1^(d+49) 0 1^34 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 118  7n+7b+7c+3610          1^(n+471) 0^3 1^(b+c-73) 0^2 1^4 0 1^(d+51) 0 1^34 0^6 1^6 0^6 1^12 0 1^2 0^2 1^2 0 1^3
 119  7n+14b+14c+21d+6647    1^(n+475) 0 1^2 0^2 1^(b+c-75) 0^2 1^(d+58) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^10 0^3 1^4 0^2 1^4 0 1^2
 120  7n+4117                1^(n+480) 0^2 1^(b+c-75) 0^2 1^(d+58) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^10 0^3 1^4 0^2 1^4 0 1^2
 121  7n+14b+14c+14d+4441    1^(n+483) 0^2 1^(b+c-73) 0^6 1^(d+54) 0^6 1^35 0 1^2 0 1^4 0^6 1^10 0^3 1^4 0^2 1^4 0 1^2
 122  7n+7b+7c+3676          1^(n+487) 0 1^2 0 1^(b+c-75) 0 1^2 0 1^(d+54) 0^6 1^35 0 1^2 0 1^4 0^6 1^10 0^3 1^4 0^2 1^4 0 1^2
 123  7n+4201                1^(n+492) 0 1^(b+c-75) 0 1^2 0 1^(d+54) 0^6 1^35 0 1^2 0 1^4 0^6 1^10 0^3 1^4 0^2 1^4 0 1^2
 124  7n+7b+7c+7d+5102       1^(n+495) 0^3 1^(b+c-77) 0^6 1^(d+52) 0^2 1^2 0^2 1^38 0^3 1^2 0^2 1^2 0^2 1^12 0 1^2 0 1^5 0 1^3
 125  7n+14b+14c+28d+6083    1^(n+499) 0 1^2 0^2 1^(b+c-79) 0^2 1^4 0^6 1^(d+53) 0 1^2 0 1^34 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 126  7n+4285                1^(n+504) 0^2 1^(b+c-79) 0^2 1^4 0^6 1^(d+53) 0 1^2 0 1^34 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 127  7n+14b+14c+7d+3705     1^(n+507) 0^2 1^(b+c-77) 0^12 1^(d+53) 0 1^34 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 128  7n+7b+7c+3816          1^(n+511) 0 1^2 0 1^(b+c-79) 0 1^2 0^7 1^(d+53) 0 1^34 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 129  7n+4369                1^(n+516) 0 1^(b+c-79) 0 1^2 0^7 1^(d+53) 0 1^34 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 130  7n+7b+7c+3890          1^(n+519) 0^3 1^(b+c-81) 0^2 1^4 0 1^(d+55) 0 1^34 0^6 1^6 0^6 1^12 0^3 1^2 0 1^2
 131  7n+14b+14c+21d+7057    1^(n+523) 0 1^2 0^2 1^(b+c-83) 0^2 1^(d+62) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^10 0^2 1^6 0 1^2 0 1^3
 132  7n+4453                1^(n+528) 0^2 1^(b+c-83) 0^2 1^(d+62) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^10 0^2 1^6 0 1^2 0 1^3
 133  7n+14b+14c+14d+4721    1^(n+531) 0^2 1^(b+c-81) 0^6 1^(d+58) 0^6 1^35 0 1^2 0 1^4 0^6 1^10 0^2 1^6 0 1^2 0 1^3
 134  7n+7b+7c+3956          1^(n+535) 0 1^2 0 1^(b+c-83) 0 1^2 0 1^(d+58) 0^6 1^35 0 1^2 0 1^4 0^6 1^10 0^2 1^6 0 1^2 0 1^3
 135  7n+4537                1^(n+540) 0 1^(b+c-83) 0 1^2 0 1^(d+58) 0^6 1^35 0 1^2 0 1^4 0^6 1^10 0^2 1^6 0 1^2 0 1^3
 136  7n+7b+7c+7d+5500       1^(n+543) 0^3 1^(b+c-85) 0^6 1^(d+56) 0^2 1^2 0^2 1^38 0^3 1^2 0^2 1^2 0^2 1^12 0 1^2 0 1^10 0 1^2
 137  7n+14b+14c+28d+6429    1^(n+547) 0 1^2 0^2 1^(b+c-87) 0^2 1^4 0^6 1^(d+57) 0 1^2 0 1^34 0^6 1^6 0^6 1^19
 138  7n+4621                1^(n+552) 0^2 1^(b+c-87) 0^2 1^4 0^6 1^(d+57) 0 1^2 0 1^34 0^6 1^6 0^6 1^19
 139  7n+14b+14c+7d+3957     1^(n+555) 0^2 1^(b+c-85) 0^12 1^(d+57) 0 1^34 0^6 1^6 0^6 1^19
 140  7n+7b+7c+4096          1^(n+559) 0 1^2 0 1^(b+c-87) 0 1^2 0^7 1^(d+57) 0 1^34 0^6 1^6 0^6 1^19
 141  7n+4705                1^(n+564) 0 1^(b+c-87) 0 1^2 0^7 1^(d+57) 0 1^34 0^6 1^6 0^6 1^19
 142  7n+7b+7c+4170          1^(n+567) 0^3 1^(b+c-89) 0^2 1^4 0 1^(d+59) 0 1^34 0^6 1^6 0^6 1^19
 143  7n+14b+14c+21d+7455    1^(n+571) 0 1^2 0^2 1^(b+c-91) 0^2 1^(d+66) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^18 0 1^2 0^2 1^2 0 1^3
 144  7n+4789                1^(n+576) 0^2 1^(b+c-91) 0^2 1^(d+66) 0^2 1^34 0 1^2 0 1^4 0 1^2 0 1^4 0^6 1^18 0 1^2 0^2 1^2 0 1^3
 145  7n+14b+14c+14d+5001    1^(n+579) 0^2 1^(b+c-89) 0^6 1^(d+62) 0^6 1^35 0 1^2 0 1^4 0^6 1^18 0 1^2 0^2 1^2 0 1^3
 146  7n+7b+7c+4236          1^(n+583) 0 1^2 0 1^(b+c-91) 0 1^2 0 1^(d+62) 0^6 1^35 0 1^2 0 1^4 0^6 1^18 0 1^2 0^2 1^2 0 1^3
 147  7n+4873                1^(n+588) 0 1^(b+c-91) 0 1^2 0 1^(d+62) 0^6 1^35 0 1^2 0 1^4 0^6 1^18 0 1^2 0^2 1^2 0 1^3

9. Evidence (`python3 -B check_proof.py [--seed S] [--quick|--full]`)

The script uses scripts/symexec.py (the executor of §3.2, about 450 lines) and scripts/krun.c (a batch C runner, compiled to work/krun on first use). Logs: work/check_proof_seed1.log, work/check_proof_seed2.log (default), work/check_proof_full_seed1.log (--full).

The tables of Appendices A and B were printed by scripts/phases.py from the executor's proof of TE and TO (it writes work/phases_<rule>.txt for S, TE, TO, T6 and T8). Check COL reads them back from this file and proves every row again on its own.

Public copy. Everything above §9 (sections 0 to 8 and the appendices) has no repository paths or internal files, and tools/writeup_lint.py reports 0 errors on it (check DOC.sections_0_to_8_and_appendices_lint_0_errors). A submission/proof.md starts from that part. It drops §9, §10, the review log and the references to named checks, and replaces §8 with an outline of the finished Rocq proof.

section	what is checked	size (default run)
T	the string; only D0 undefined; D entered only by A1; line 214 of the 740 list byte for byte; G (43 cells) and the K word of §2
SR	R1, R2b, R2a as exact window runs that never leave the window; R2b and R2a fail with a 1 on the left; k-fold forms by direct simulation	k ≤ 40, 5 random contexts each
ENG	the executor against direct simulation: random symbolic tapes (half set up for a shift rule), random branches, random values; tape, head, state, steps; an unsound variant (no 0-on-the-left check) is caught	2,000 + 2,000 cases
MR	S, TE, TO, T6, T8 by the executor: every leaf reaches the claimed K, with the head on the left end in state F; step formula exact; no D0; R2a unused; splits as stated; same result with R1 and R2b only	6 leaves
PH	P1–P12 by the executor; their step formulas; their sum = S's formula; K_12 = K(n+48,a-8,b+4,c,d+4)	12 rules
COL	Appendices A and B, read from this file: row 0 and the last row are the rule's start and end; every row by the executor from the row above (one branch, exact step formula, R1 and R2b only, no D0); the step column sums to the rule's formula; the structure listed in §3.4; every row by direct simulation	138 + 147 rows; 5,382 + 13,671 runs
DIR	every macro rule and phase rule by direct simulation: exhaustive boxes at the bottom of each domain + random values up to about 2,000; exact configuration and step count	S 3,185; TE, T8 1,788; TO, T6 1,356; each P_j 303
TEETH	each lower bound of S is sharp (one below it, the result fails)	4 bounds × 6
DC	every application inside its domain and the result Even(n+12x+808, x+32), for x = 52, 60, ..., 3,996; whole double cycles by direct simulation, with 3x+201 trips	494 + 26 (x ≤ 252)
OPEN	4,097,897 steps from blank to K(1959,34,68,45,18); no earlier K-shaped left record; the 20 rows of §5 (domains, step sums, direct simulation of every row)	153,126,993 steps
ORB	from step 153,126,993 on, the law predicts every even and odd run start of the observe stage's run to 10^10 steps (`work/run_starts_K.tsv`)	16 even + 15 odd
HALT	the executor stops on D0 (control); no leaf reads D0; no halt in the first 153,126,993 steps
PLAN	the §8 statements in Kr form equal the §1 rules (start and end words, for random arguments), and the §8 DC chain (its arguments) lands on Ev (48X+716+N) (4+X)	200 per lemma, 100 X
DOC	this file quotes the rule statements, step formulas, the phase table, the R2b trace and the opening rows exactly as checked; sections 0 to 8 and the appendices lint with 0 errors

10. Checkpoint B (Dennis)

Pending (non-blocking).

Review log

2026-10-13, informal_proof stage (first version).
New: the symbolic executor scripts/symexec.py (§3.2), which proves S, TE, TO, T6, T8 for their whole domains; the phase table of S (§3.3); the collision rules T6 and T8, which the observe stage had not stated; the double-cycle proof with every domain condition (§4); the opening as 4,097,897 direct steps plus 20 macro steps (§5), instead of 153,126,993 direct steps.
Corrections to the observe-stage notes: R2b needs a 0 on the left of the crossed copies; the notes' form 10 B> 000 -> B> 000 11 is false without it (the first version of the executor also lacked that condition, and the R2b window check in SR caught it). G has 43 cells, not 44 (44 counts the head cell). Not every trip reaches the right end: trips 3, 6, 9 and 12 of S turn at the first particle (§3.3). R2a is true but not needed.
The bounds of TE and TO in the notes are sufficient but not all sharp (TEETH found TE also works at d = 18 and TO below its b, c, d bounds in the sampled cases). Only S's bounds are claimed sharp.
A self-review pass before the final runs: the R2b trace table of §3.1 is now checked row by row against the machine (DOC.R2b_trace_row_quoted); the §8 statements in half-length form are checked against the rules (new section PLAN); §3.3 now says that P1 (not only S) needs the d split; §5 no longer quotes the observe stage's x - 2y values for the early runs (replaced by a checked example, row 16).
Results: 164/164 PASS with seed 1 and seed 2 (default, 48 s each) and with seed 1 --full (195 s).
Open: Checkpoint B; a skeptic pass by a second agent; formalization (§8).
2026-10-13, skeptic round 1: sound, 4 minor gaps, no fatal or major gap. All 4 fixed.
The skeptic re-proved S, TE, TO, T6, T8, the 567 per-trip statements and P1-P12 with an executor written from scratch, and confirmed the rules, double cycles, opening and orbit with a separate C simulator.
Gap 1, collisions not checkable by hand. New Appendices A and B give the configuration after every trip of TE (138 rows) and TO (147 rows) with the steps of each trip.
§3.4 now says how to read and check a row, and lists the structure the tables show. T6 and T8 are used only at concrete arguments (§5, each use confirmed directly), so their tables are not printed. §3.4 also says that in Rocq the es' lemmas are the certificate. The pointers to work/ files are gone from §0-§8.
New check section COL. It reads both tables back from proof.md, proves every row again with the executor (one branch, exact steps, R1 and R2b only), and checks the step sums, the first and last rows, the structure claims and every row by direct simulation. A mutation test (one wrong word per table, one wrong step count) made COL fail where expected.
Gap 2, the d split. §3.3 now says the split is a feature of our executor and that rotating the block, y (v y)^X = (y v)^X y, avoids it; §8 item 2 and the S risk are updated. Re-running the skeptic's executor on S gave one leaf.
Gap 3, stale comments. check_proof.py's docstring states R2b with its left 0, and its section map matches proof.md. symexec.py says G has 43 cells and points at §3.2. notes.md's two observe-stage lines carry the corrections.
Gap 4, a public copy. Header bullets split; §2 is short paragraphs; the executor's file description moved from §3.2 to §9; §8 renamed "Formalization outline", with its risks as short paragraphs. Everything before §9 lints with 0 errors and 0 warnings (new check DOC.sections_0_to_8_and_appendices_lint_0_errors); §9 says how submission/proof.md is made from it.
Results: 196/196 PASS with seed 1 and seed 2 (default, 55 s each) and with seed 1 --full (206 s). COL ran 5,382 + 13,671 direct row runs (default) and 17,112 + 46,452 (--full). After a last wording pass on §3.4 and §8 (prose only), DOC and COL were re-run: 69/69 PASS.
Open: Checkpoint B (non-blocking); formalization (§8).