1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---: never halts

• Machine: 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---, viewer https://bbchallenge.org/1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---
• Sheet: Results row 921, "Sync bouncer counter", no notes. Archive: "does not halt in 2e13". It is on dyuan01's Oct 1 longitudinal list (ask before submitting) and on mxdys's UBRRBA_TODO.
• Written for the string itself. Its only undefined transition is F1.
• Status: informal proof, not yet formalized. Finite claims (the 21 shift rules, the initial segment, the polygon's vertex check) are executed exactly. Parametric claims (CTR, QC, R1–R5o, the cycle lemma) are derived by hand in §3–§4, and check_proof.py checks them over ranges and random samples (§7).
• Template: verify/SBCv7.v has six solved machines that differ from this one only in F0: TM1 (0LC), TM2 (0RD), TM3 (0LA), TM4 (0RA), TM18 (0LD) and TM37 (1RB). TM4 is used below for its hL/hR/d0/d1 names and its BigStep shape; TM1–TM3 share the same names and lemma list, so any of them would do equally well (§6).

0. Picture

The left end of the tape is a binary counter. To its right is a row of 5-cell blocks. The head bounces between the counter and the right edge, adding 1 to the counter on every visit to it.

• P phase. Each bounce adds one B block at the right edge.
• Overflow. When the counter overflows, it gains a digit and a 3-cell marker, the front 111, appears at its right.
• Q phase. The front walks right two blocks every three bounces.
• Conversion. When the front reaches the B blocks, it turns them all into A blocks.

Each full cycle doubles the counter range. The block counts after a cycle are an affine function of the counts before it, and the function has two branches, chosen by the parity of a count. The proof finds a hexagon in the scaled block counts that both branches map into itself.

1. Notation and families

Tapes are written in directed-head notation. L <S R means the head is in state S on the last cell of L. L S> R means the head is in state S on the first cell of R.

The families below are the right-edge visits in state C. Simulation found that 4,711 of 4,722 such visits up to step 1e9 have one of these two shapes; the other 11 are the start and mid-conversion visits.

P(k,n,X,z)   := 0^inf C_k(n) A^X B^z 00 C> 0^inf                 X,z >= 0
Q(k,n,x,y,z) := 0^inf C_k(n) A^x 111 A^y B^z 00 C> 0^inf         x >= 1; y,z >= 0

2. Rule table (busycoq comment-block style)

1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---

C_k(n): n in k bits MSB first, 1 -> 1010, 0 -> 0010;   A = 00111, B = 10111
P(k,n,X,z)   := 0^inf C_k(n) A^X B^z 00 C> 0^inf
Q(k,n,x,y,z) := 0^inf C_k(n) A^x 111 A^y B^z 00 C> 0^inf                    (x >= 1)

R1  P(k,n,X,z)      --> P(k,n+1,X,z+1)                     n+1 <= 2^k-1
R2  P(k,2^k-1,X,z)  --> Q(k+1,2^k+1,1,X-2,z+1)             X >= 2
R3  Q(k,n,x,y+2,z)  --> Q(k,n+3,x+2,y,z+1)                 n+3 <= 2^k-1
R4  Q(k,n,x,0,z)    --> P(k,n+z+2,x+z+1,0)                 n+z+2  <= 2^k-1
R5  Q(k,n,x,1,z)    --> P(k,n+2z+7,x+z+4,0)                n+2z+7 <= 2^k-1
R5o Q(k,n,x,1,z)    --> Q(k+1,2^k+1+3m,1+2m,x+z+2-2m,0)    m := n+2z+7-2^k >= 0,  x+z+2-2m >= 1,  3m <= 2^k-2

remark (true, never used): R4o Q(k,n,x,0,z) --> Q(k+1,2^k+1+3m,1+2m,x+z-1-2m,0),
                           m := n+z+2-2^k >= 0, x+z-1-2m >= 1, 3m <= 2^k-2

steps: R1 32X+32z+16t(n)+47,  R2 32X+32z+16k+61,  R3 96x+32y+32z+16(t(n)+t(n+1)+t(n+2))+197
       (t(n) = number of trailing 1 bits of n)

cycle (N = 2^k):  S(k,Y,Z) := Q(k+1, N+1+3m, 1+2m, Y-2m, Z+m),  m = max(0,-Z)
  (S(k,.) is the first right-edge visit after the counter grows to k+1 digits; its counter
   lies in [N,2N) and overflows at 2N)
  S(k,2j,Z)   -->+ S(k+1, 3j+Z,   N-3-4j-Z)      via R3^(j-m), R4, R1^(N-4-2Y-Z), R2
  S(k,2j+1,Z) -->+ S(k+1, 3j+3+Z, N-8-5j-2Z)     via R3^(j-m), then R5, R1^*, R2  or  R5o
invariant (N >= 64):  8Y >= N, 8Y <= 3N, 3Z <= N, 8Z >= -N, 4Y+2Z >= N, 20Y+16Z <= 9N
start: c0 -->(17215) S(6,16,0) = Q(7,65,1,16,0)

Every case is covered. For P: n < 2^k-1 uses R1, and n = 2^k-1 uses R2 (X ≥ 2 holds; see §4). For Q: y ≥ 2 uses R3. y = 0 uses R4: on the invariant the counter never overflows during an even conversion (§4), so R4o is never needed. y = 1 uses R5 if the counter does not overflow during the conversion, and R5o if it does. The domain conditions that the run must satisfy (no overflow inside a Q phase, R2's X ≥ 2, no overflow in an even conversion, and the R5o conditions) are exactly what the invariant in §4 guarantees. Outside those domains, the overflow chain of §3.3 fails to apply on every one of the 677 small instances tried (check_proof.py §3c). This shows the conditions matter, not that they are necessary. One out-of-domain instance even halts: Q(4,8,400,0,180) (from the card).

3. Proofs of the rules

3.1 Shift rules (level 0)

Each rule below is a fixed finite run. In the formal proof, each is one es (check_proof.py §1 executes each on its window exactly). Rules marked 0^inf need blank tape on that side. All others hold for every context.

3.2 Repeated rules (level 1, ind)

• AL^a: A^a <A 001 → <A 001 A'^a (25a steps). Likewise BL^z (9z), AR^a: 001 E> A'^a → A^a 001 E> (7a), BR^z (23z), D1L^t, and D0R^t.
• CTR. For n+1 ≤ 2^k-1: 0^inf C_k(n) <A 001 → 0^inf C_k(n+1) 001 E> in 16t(n)+18 steps. Write C_k(n) = W 0010 1010^t. Then:
• D1L^t gives W 0010 <A 001 0101^t;
• FLIP gives W 1010 001 E> 0101^t;
• D0R^t gives W 1010 0010^t 001 E> = C_k(n+1) 001 E>.
• OV. 0^inf C_k(2^k-1) <A 001 A' A' → 0^inf C_{k+1}(2^k+1) A 111 001 E> in 16k+46 steps:
• D1L^k gives 0^inf <A 001 0101^k A' A', which is the same tape as 0^inf <A 001 01 0101^(k-1) 01 00101 00101;
• OVL gives 0^inf 1010 001 E> 0101^(k-1) 01 00101 00101;
• D0R^(k-1) gives 0^inf 1010 0010^(k-1) 001 E> 01 00101 00101;
• OVR gives 0^inf C_{k+1}(2^k) <A 001 101 00101;
• FLIP (that is, CTR with t = 0) gives 0^inf C_{k+1}(2^k+1) 001 E> 101 00101;
• FR3 finishes.

The counter gains a digit: 2 of its 4 cells come from the blank left side and 2 from the right. The 13 cells 001 A' A' become the 11 cells A 111 001, which are the new front. - QC (one front step). For every right word G, with x ≥ 1, y ≥ 2, and n+3 ≤ 2^k-1:

C_k(n) A^x 111 A^y <A 001 G -AL^y-> C_k(n) A^x 111 <A 001 A'^y G -FL-> C_k(n) A^(x-1) <A 001 001 B' A'^y G front now "001 B'" -AL^(x-1),CTR,AR^(x-1),FR1-> C_k(n+1) A^x <A 001 001 A'^y G front "001" -AL^x,CTR,AR^x,FR2-> C_k(n+2) A^(x+1) <A 001 101 A'^(y-1) G front "101" -AL^(x+1),CTR,AR^(x+1),FR3-> C_k(n+3) A^(x+2) 111 001 E> A'^(y-2) G front back in left form -AR^(y-2)-> C_k(n+3) A^(x+2) 111 A^(y-2) 001 E> G

So the front is a 3-state gadget: it reflects the head twice, lets it through on the third visit, and ends up two blocks further right.

3.3 Macro rules

• R1 is ENDL, BL^z, AL^X, CTR, AR^X, BR^z, ENDR. The step count is 7+9z+25X+(16t+18)+7X+23z+22.
• R2 is ENDL, BL^z, AL^X, OV, AR^(X-2), BR^z, ENDR. It needs X ≥ 2, because OV uses two A' blocks.
• R3 is ENDL, BL^z, QC (with G = B'^z 0^inf), BR^z, ENDR.

Conversion (R4, R5, R5o; R4o as a remark). The derivation below treats both parities at once, because the argument is the same. The proof only needs the overflow case for y = 1 (R5o): §4 shows that on the invariant an even conversion never overflows. Start from Q(k,n,x,y,z) with y ∈ {0,1}. Applying ENDL, BL^z, AL^y, FL gives 0^inf C_k(n) A^(x-1) <A 001 G_1, where the old front plus the B blocks now form a gadget:

• even (y=0): G_1 = 001 B'^(z+1) 0^inf. Its hits are FR1 z+1 times, then FE0.
• odd (y=1): G_1 = 001 B' A' B'^z 0^inf. Its hits are FR1, FR2, (FR4, FR2)^z, FE1, FE2, FE3, FE4, FE0. The gadget word runs through 001 B' A' B'^z, 001 A' B'^z, 101 B'^z, 001 A' B'^(z-1), 101 B'^(z-1), …, 101, 001 001, 1, 0011, 001, and then the right edge.

So there are T = z+2 (even) or 2z+7 (odd) hits. Every hit except the last is a reflection 001 E> G_t → A^(δ_t) <A 001 G_(t+1). Here δ_t = 1 for FR1, FR2, FE2 and FE4, and δ_t = 0 for FR4, FE1 and FE3. The last hit, FE0, ends at the right edge and adds one more A; count it as δ_T = 1. In total, Σ_t δ_t = z+2 (even) or z+5 (odd).

• Round without overflow (n+1 ≤ 2^k-1): C_k(n) A^a <A 001 G_t goes by AL^a, CTR, AR^a, hit_t to C_k(n+1) A^(a+δ_t) <A 001 G_(t+1). Starting from a_1 = x-1:
• R4/R5. If all T rounds avoid overflow (n+T ≤ 2^k-1), the run ends at P(k, n+T, x-1+Σδ, 0), which is R4 or R5.
• R5o (and R4o). Otherwise the counter overflows in round r = 2^k-n ≤ T, and m := T-r rounds remain after that.
• Rounds 1..r-1 are no-overflow rounds as above: by the choice of r, each one starts with counter ≤ 2^k-2.
• Round r is AL^a, OV, AR^(a-2), hit_r with a = a_r = x-1+Σ_{t<r}δ_t. OV needs the two A' blocks right of the head, so a_r ≥ 2. If m ≥ 1, round r ends at C_{k+1}(2^k+1) A 111 A^(b) <A 001 G_(r+1) with b = b_(r+1) := a_r-2+δ_r A blocks between the two fronts. A new front has started next to the counter while the old gadget is still converting.
• Each later round s (r < s ≤ T) is QC, hit_s. QC needs b_s ≥ 2. The new front moves 2 blocks right, the counter gains 3, and the between-count becomes b_(s+1) = b_s-2+δ_s ≤ b_s-1.
• End. The last hit is FE0 (δ_T = 1), which gives Q(k+1, 2^k+1+3m, 1+2m, y_f, 0) with y_f = (x-1+Σ_{t<r}δ_t) - 2 + Σ_{t≥r}δ_t - 2m = x-3+Σδ-2m. This is x+z+2-2m (odd, R5o) or x+z-1-2m (even, R4o).
• Domain. Assume y_f ≥ 1 and 3m ≤ 2^k-2.
  • If m = 0, round r is the last round and its hit is FE0, so it ends at Q(k+1, 2^k+1, 1, a_r-1, 0). Then y_f = a_r-1, and y_f ≥ 1 gives a_r ≥ 2 directly. There are no QC rounds. (The initial segment's last step, which reaches S(6,16,0), is this case; see §5.)
  • If m ≥ 1, the last round T is a QC round and y_f = b_T-2+1, so b_T = y_f+1 ≥ 2. The between-counts strictly decrease, so b_s ≥ b_T ≥ 2 for every r < s ≤ T, which is what each QC needs. Also b_(r+1) ≥ b_T ≥ 2 gives a_r = b_(r+1)+2-δ_r ≥ 3.
  • The counter fits in k+1 bits: the last QC starts at 2^k+1+3(m-1) and needs that value plus 3 to be ≤ 2^(k+1)-1, that is, 3m ≤ 2^k-2.

4. Coverage, invariant, progress

Cycle states. Let N = 2^k and m = max(0,-Z). Define S(k,Y,Z) := Q(k+1, N+1+3m, 1+2m, Y-2m, Z+m). S(k,·) is the first right-edge visit after the counter grows to k+1 digits: its counter lies in [N,2N) and overflows at 2N. (So S's index k is one less than the Q/P level k+1; in the cycle lemma, the next overflow is at 2N and the next cycle state is S(k+1,·) at level k+2.)

• For Z ≥ 1 this is R2's output Q(k+1,N+1,1,Y,Z).
• For Z ≤ 0 it is R5o's output, written as if those m front steps had been R3 steps from x = 1.

Cycle lemma. Write F_N(Y,Z) = (Y',Z') for the two branches in §2. Suppose that:

• (a) Y+2Z ≥ 1;
• (b) 3⌊Y/2⌋ ≤ N-2;
• (c) Y' ≥ 0, Y'+2Z' ≥ 1 and 3⌊Y'/2⌋ ≤ 2N-2;
• (d) if Y is even, then Z' ≥ 1 (equivalently 2Y+Z ≤ N-4).

Then S(k,Y,Z) →+ S(k+1,Y',Z').

Proof. Let p = Y mod 2 and j = ⌊Y/2⌋. By (a), j ≥ m.

• Q phase. R3^(j-m) gives Q(k+1, n, x, p, z) with n = N+1+3j, x = 1+2j and z = Z+j ≥ 0. No overflow occurs, by (b).
• Conversion. Let T = z+2 (even) or 2z+7 (odd), and s = n+T. In both cases Z' = 2N-s (see the formula below).
• If s ≤ 2N-1: R4/R5 gives P(k+1, s, X, 0), then R1^(2N-1-s) gives P(k+1, 2N-1, X, 2N-1-s), and R2 gives S(k+1, X-2, 2N-s). R2's condition X ≥ 2 is Y' ≥ 0. For even Y this case always applies, since s = 2N-Z' ≤ 2N-1 by (d): the even branch is R4, R1^(N-4-2Y-Z), R2.
• If s ≥ 2N, then Y is odd by (d), and R5o with m' = s-2N gives S(k+1, X-2, 2N-s) directly. Its conditions are y_f = Y'+2Z' ≥ 1, and 3m' ≤ 3⌊Y'/2⌋ ≤ 2N-2, where m' ≤ ⌊Y'/2⌋ because Y' ≥ 2m'+1. Both come from (c).
• The formula. In both cases (Y',Z') = (X-2, 2N-s):
• even: X-2 = x+z-1 = 3j+Z, and 2N-s = N-3-4j-Z;
• odd: X-2 = x+z+2 = 3j+3+Z, and 2N-s = N-8-5j-2Z. ∎

Invariant. Let R_N be the integer points (Y,Z) with

8Y ≥ N, 8Y ≤ 3N, 3Z ≤ N, 8Z ≥ -N, 4Y+2Z ≥ N, 20Y+16Z ≤ 9N.

In u = Y/N and v = Z/N this is the hexagon R with vertices (1/8,1/4), (1/8,1/3), (11/60,1/3), (3/8,3/32), (3/8,-1/8) and (5/16,-1/8). For N ≥ 64:

• (i) R_N gives (a), (b) and (d). On R, u+2v ≥ 1/16, so Y+2Z ≥ N/16 ≥ 4. Also 3⌊Y/2⌋ ≤ (3/2)(3/8)N = 9N/16 ≤ N-2. For (d): 16(2Y+Z) = (20Y+16Z) + 12Y ≤ 9N + 12·3N/8, so 2Y+Z ≤ 27N/32 (on R, max 2u+v = 27/32, at vertex (3/8,3/32)). Then 2Y+Z ≤ N-4 for N ≥ 26. So on the invariant the even branch always takes R4, then R1^(N-4-2Y-Z), then R2, and Z' = N-3-2Y-Z ≥ 5N/32-3 > 0. The counter never overflows during an even conversion, and R4o is never used.
• (ii) F_N maps R_N into R_2N. With u' = Y'/2N and v' = Z'/2N, each branch is affine in (u,v):
• even: u' = 3u/4 + v/2 and v' = 1/2 - u - v/2 - 3/(2N);
• odd: u' = 3u/4 + v/2 + 3/(4N) and v' = 1/2 - 5u/4 - v - 11/(4N).

An affine map sends the hexagon into itself if it sends the 6 vertices in. The image coordinates are affine in 1/N ∈ (0,1/64], so checking 1/N = 0 and 1/N = 1/64 covers every N ≥ 64. All 6 vertices × 2 branches × 2 values × 6 facets hold, with slack at least 3/128 in the integer-coefficient form above (exact rational check in check_proof.py §5). The minimum is attained by the odd images of the edge u = 1/8 against the facet 4Y+2Z ≥ N, at 1/N = 1/64. For the odd branch that slack is 4u'+2v'-1 = u/2 - 5/(2N), which does not depend on v, so both vertices (1/8,1/4) and (1/8,1/3) tie at 1/16 - 5/128 = 3/128. - (i) and (ii) give (c). Applying (i) at level 2N to the image point gives (c), and Y' ≥ 2N/8 > 0.

The linear parts of the two branches contract: the even branch's eigenvalues have modulus 0.354, and the odd branch's are 0.25 and -0.5. Their fixed points are (2/7,1/7) and (2/9,1/9).

Parity, and why this is not a cryptid. The branch at each level is the parity of Y, a pseudo-random bit; in the real run the sequence is even, odd, even, even, odd, odd, even, …. But R is mapped into itself by both branches, so halting does not depend on the parities. Ground rule 6 does not apply.

Progress. Every macro rule contains ENDL (7 steps), so each cycle takes at least 1 step; in fact it takes Θ(4^k).

Conclusion. The run reaches S(6,16,0), which is in R_64 (the facet 4Y+2Z ≥ N is tight there: 64 = 64). By induction, for every k ≥ 6, the run reaches S(k+1,F(Y,Z)) from S(k,Y,Z), with the invariant holding at each level. So the machine runs forever.

Why F1 is never reached. Every step of the run lies inside one application of the 21 shift rules of §3.1, and each of those was executed exactly on its window. F is entered only by E1 = 1RF. That happens only inside FR3, FR4, FE1 and FE3, where E reads the 1 of a front word 101 or the lone 1 of FE3. Each time, the next cell is 0, so F0 = 1RC runs and F1 (halt) never does (check_proof.py §1 lists the transitions each rule uses).

5. Initial segment

c0 = 0^inf A> 0^inf reaches Q(5,17,1,2,2) = S(4,2,2) in 1,507 steps, by direct simulation (exact). From there the rules give:

• R3 to Q(5,20,3,0,3) (step 1,912);
• R4 to P(5,25,7,0) (step 2,826);
• R1^6 to P(5,31,7,6) (step 4,996);
• R2 to Q(6,33,1,5,7) = S(5,5,7) (step 5,553);
• R3^2 to Q(6,39,5,1,9) (step 7,003);
• R5o with m = 0 to Q(7,65,1,16,0) = S(6,16,0) (step 17,215). Here the overflow round is the last round (its hit is FE0), the case m = 0 of the R5o domain in §3.3.

Direct simulation also gives c0 -->(17215) Q(7,65,1,16,0). In Rocq, Lemma init: c0 -->* 0inf <* <[1;0;1;0] <* <[0;0;1;0]^^5 <* <[1;0;1;0] <* <[0;0;1;1;1] <* <[1;1;1] <* <[0;0;1;1;1]^^16 <* <[0;0] {{C}}> 0inf. Proof. esx. Qed. compiles in 2.1 s, closed under the global context (checked 2026-10-10, Coq 8.20.1). The induction starts at k = 6 (N = 64), because S(4,…) and S(5,…) are below the N ≥ 64 bound of the invariant.

Check against the real run: starting from step 1,507, applying only these rules reproduces all 36 observe.json history rows from that point on (configuration and exact step number), up to P(15,25768,7028,0) at step 2,318,632,923. The run's cycle states (k,Y,Z) are (6,16,0), (7,24,29), (8,65,48), (9,147,-8), (10,214,155), (11,476,438), (12,1152,655), (13,2383,1134) and (14,4710,-39), all inside R.

6. Mapping to busycoq, and what is new

Templates. SBCv7.v has six solved machines that differ from this one only in F0: TM1 (0LC), TM2 (0RD), TM3 (0LA), TM4 (0RA), TM18 (0LD) and TM37 (1RB). Other files have more (IndSBCv1 nonhalt42 with 1RA, CTLv1 nonhalt22216/nonhalt22724 with 0LB/1LA), but those are decider certificates, not readable templates. TM1–TM4 share the same notations (hR = (E,<[0;0;1]), hL = (A,[0;0;1]), d0, d1) and the same lemma list (LIncs … BigStep, nonhalt); TM18 adds a second particle pair (hR', hL') and TM37 uses different particles. TM4 is used below for those names and its BigStep shape; TM1–TM3 would serve equally well.

TM4 in brief. TM4 uses the Longitudinal library. Its segments are segRLs/sideRLs; its counter is handled by LIncs via BC.Mul2/BC.Incs on tm' (d0 = <[0;0;1;0], d1 = <[1;0;1;0], which are our 0010 and 1010); its right side is a unary counter UC1.Incs on w0/w1/w0'/w1'. TM4's proof has one BigStep per counter overflow, then progress_nonhalt_cond with the one-line invariant Rn ls <= (2^k-1)*2.

What carries over: - the particles: TM4's hR/hL are our 001 E>/<A 001; - the digits; - the counter behaviour: D1L, FLIP, D0R, OVL and OVR never enter F (checked), so CTR and OV up to its final FR3 hold verbatim for TM4's machine; - the overall shape: init, a big step per cycle, and progress_nonhalt_cond with a linear invariant.

What is new: - Blocks. Our F0 = 1RC changes every right-side word. The blocks are 00111/00101 and 10111/00001, not TM4's. - Front gadget. A 3-state front gadget (FL, FR1, FR2, FR3) walks right inside the block row. - Conversion gadget. It has a parity split: even uses FR1 only; odd uses FR1, FR2, (FR4, FR2)^z, then FE1–FE4. - Overflow during an odd conversion (R5o). The new front's QC rounds run interleaved with the old gadget's hits. This is the main new lemma. Only the odd case is needed: on the invariant an even conversion never overflows (§4), so there is no R4o lemma. - Invariant. A two-branch affine cycle map with a 6-facet polygon invariant, instead of TM4's one inequality.

Suggested formalization (IPS style; Longitudinal is not needed).

7. Evidence (check_proof.py, 6 s, ALL CHECKS PASSED)

What kind of check each item is: §1, §5 and the initial segment in §6 are exact computations, so they prove those finite claims. Everything else is a range or sample check of a parametric claim (CTR for all k and n, QC for every G, R1–R5o, the cycle lemma) whose proof is the hand derivation in §3–§4.

• §1 Shift rules (exact). All 21 shift rules were executed exactly on their windows. Each step count matches, F1 is never read, and the transitions used are all except F1. For finite rules this is a proof, not a sample.
• §2 Repeated rules (ranges).
• AL/BL/AR/BR were executed exactly for a = 0..24.
• CTR was executed exactly for all 1,013 (k,n) with k ≤ 10, with 16t(n)+18 steps.
• OV was executed exactly for k = 1..10, with 16k+46 steps.
• §3 Macro rules (ranges and samples). A derivation runner applies exactly the chains of §3 to the concrete tape, checking every rule's pattern at the head. Its result is compared with the formulas of §2 and, for most instances, with direct simulation run for exactly the summed step count.
• Exhaustive over small parameters (one third also simulated): R1 2,793, R2 210, R3 12,096, R4 1,740, R5 954, R5o 393 instances, and R4o 428 (the remark).
• Random large parameters (k up to 11, blocks up to 300 or 2^(k-1)): 60 per rule, all also simulated.
• The step formulas for R1–R3 match on every instance.
• §4 Cycle map (samples, plus an exhaustive integer check).
• At k = 6..11, 12 random invariant points per level were checked with the runner, and the k ≤ 8 points also by simulation. Those 72 cycles used R1 13,124, R2 57, R3 5,770, R4 34, R5 23 and R5o 15 times, and R4o never.
• Exhaustively, all 316,911 integer points of R_N for N = 64..2048 map into R_2N and satisfy the cycle-lemma hypotheses (a)–(d). Their conversions are R4 158,810, R5 118,780, R5o 39,321, and R4o 0.
• §5 Polygon (exact). An exact rational vertex check confirms invariance for all N ≥ 64. The minimum slack is 3/128, attained at both vertices of the edge u = 1/8 (odd branch, facet 4Y+2Z ≥ N, 1/N = 1/64). It also confirms the side conditions, including max(2u+v) = 27/32 at (3/8,3/32).
• §6 Initial segment and orbit.
• Direct simulation confirms c0 reaches Q(5,17,1,2,2) at step 1,507 and S(6,16,0) at step 17,215 (exact).
• From step 1,507 to step 2,318,632,923, the runner applied only §3's rules and hit all 36 history rows at the right configurations and exact step numbers. It used R1 2,459, R2 7, R3 4,548, R4 7, R5 1 and R5o 3 times, and R4o never.

Gaps. None in the argument as far as I can see. What remains is formalization, and the CTR value bookkeeping (bits to C_k(n)) is the fiddliest part of it. The domain of R5o is a sufficient condition chosen for the cycle lemma; it is not claimed to be necessary.

Review log (Checkpoint B skeptic, 2026-10-10)

The skeptic found the argument sound and raised seven minor gaps. All seven were accepted.