/machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/work/proof_draft_hunt_2026-10-11.md · raw

1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (W4-2): never halts (informal proof, draft)

Machine: 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (740 list line 224), viewer https://bbchallenge.org/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF
Written for: the string itself (no mirror, no renaming). 349 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- is Eqv_v3 TM518, i.e. this table started in F; §7.3.
Status: draft from the funded stage hunt (2026-10-11). Rules validated by simulation; the invariant I (§4) is closed under the clean-to-clean step and keeps every overflow off the halting points. The case analysis below is by hand; every case is also checked by script (§8). Checkpoint B pending, non-blocking.
AI assistance: written by Claude (Anthropic) under Dennis's direction.

     0    1
A   1RB  1LF
B   0RC  0RB
C   0LD  1LA
D   1LC  0LE
E   0LA  ---        halting transition: E reads 1
F   1LA  1LF

0. Where each piece stands

piece	status	evidence (§8)
configuration family `K(w,n,m)`, bounce R1, overflow R2/R3/R4	rules, checked on random instances by direct simulation	V1
`phi` closed form, `phi^j` acceleration	checked against direct simulation / iterated `phi`	V1
counters std/pk, big steps from clean counters	checked by direct simulation	V1
landing lemma (dirty orbits, gen 1 and gen 2), closed-form step `B`	derived (§3); `B` = phi iteration on 60,000 random states; `B` = direct TM on 1,587 random/constructed states covering every case	V2, V3
invariant I, safety lemma S, closure lemma C	proved by case analysis (§5, §6); checked exhaustively for m <= 1300 (856,374 states) and on 5.2M random states up to m ~ 2^60	V4, V5
init: blank tape reaches `K('1',0,1)` = std(1), m = 1, which satisfies I	exact (32 steps)	V1
on the real run	I holds at all 17,000,000 clean overflow states checked (m ~ 4.3e7)	V6

1. Configurations

K(w, n, m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf. A reads the last cell of the left word w (string, highest cell first, leading 0s dropped). Offsets in w count from its right end (offset 0 = the cell A reads). E-cells = even offsets, O-cells = odd offsets.

Counters: std(N) has the binary digits of N on the E-cells (digit d at offset 2d, all O-cells 0). pk(N) (N >= 2): one O-cell 1 at offset 2P+1 worth 2^(P+1), plus N - 2^(P+1) < 2^(P+1) on the E-cells 0..2P. A clean overflow state (typ, N, m) means K(typ(N), 0, m).

2. Rules (validated, previous stage)

phi (left bounce of the word): last cell 0 -> 1; otherwise take the lowest adjacent pair 00 (cells e, e+1, 0^inf counts), set cell e+1 to 1 and cells 0..e to 0. F1 = 1LF lets the carry pass 11.
R1 (n >= 1): K(w,n,m) -> K(phi(w), n-1, m+1); so K(w,n,m) ->* K(phi^n(w), 0, m+n).
Overflow (n = 0): f = phi(w) = x 1 0^q.
R2, q even: K(w,0,m) -> K(x, m+1+q/2, 0).
R3, q odd, x = x' 00 (or empty): K(w,0,m) -> K(x', 0, m+(q+3)/2) (reset).
R4, q odd, x ends in 01 or 11: halts. R5, q odd, x ends in 10: nested (no closed form; treated as fatal).
So halting is possible only at an overflow whose phi puts the lowest 1 of f on an O-cell ("odd landing").
Init: blank -> K('',0,0) (step 5) -> K('',1,0) (14) -> K('1',0,1) (32) = clean state (std, 1, 1).

3. The clean-to-clean step B

Let (typ, N, m) be clean, i = number of trailing 1 bits of N, k = N >> (i+1) (so N = (2k+1)2^i - 1), b = 1+i+m, L = bitlen(k). The overflow strips the low digits: phi(typ(N)) = x 1 0^(2i) with x = std(k)0 (std) or pk(k)0 (pk, k >= 2), so R2 gives K(x, b, 0) and then K(phi^b(x), 0, b). The next overflow applies phi once more, i.e. it looks at phi^(b+1)(x).

3.1 Landing lemma (gen 1)

std, H0 = std(k)0: k's bits sit on O-cells. phi^j(H0) = O-bits k_j (k with its lowest runs of 1s swept up) plus a binary counter on the E-cells below the lowest O-bit, and 2 k_j + (counter) = 2k + j (the T-count). Odd landings happen exactly at T_g = 2((k >> g << g) + 2^g) for each 0-bit g of k above its lowest 1 bit (g < L), and at T = 2^(L+1) (k_j = 2^L: the word is pk(2k+j) from then on). Above a landing at g the two cells are (bit g+1 of k, 0): 10 = N (nested) if bit g+1 = 1, 00 = R (reset) otherwise. The landing at 2^(L+1) leaves x empty (R3, harmless).
pk, H0 = pk(k)0, k = 2^(L-1) + r, 0 < r < 2^(L-1): E-cell 1 at offset 2L-2, r on O-cells, T-count 2r + j. Odd landings at T_g = 2((r >> g << g) + 2^g) for 0-bits g of r above its lowest 1, g <= L-2. Above the landing: 01 = H (halts) when g = L-2, else N/R as for std. At T = 2^L the carry passes the 11 pair and lands on the E-cell 2L: phi^j(H0) = std(2r + j) from then on.
Consequence: the overflow is safe unless its T-count T = 2k+b+1 (std) / 2r+b+1 (pk) equals an N/H landing. All N/H/R landings of std lie at T <= 3*2^(L-1) (the top one is the gap at bit L-2), all of pk at T <= 2^(L-1) (the H point).

3.2 Cases of B (all checked: closed form = phi iteration = direct TM, §8)

case	condition	next clean state
std k=0	N = 2^i - 1	std(b), m'=b
std k=2^p, std clean	k power of 2, or `2k+b >= 2^(L+1)`	pk(2k+b), b
std top reset	`2k+b+1 = 2^(L+1)`	std(b+L+3), b+L+3 (R3 with x empty, then R2)
pk k=0	N = 2^(i+1) - 1 (all ones)	std(b+1), b+1 (R3 with x empty)
pk k=2^p	k power of 2 (k = 1 gives x = '1' = std(1))	std(k+b), b
pk clean	`2r+b >= 2^L`	std(2r+b), b
pk merge-at-overflow	`2r+b+1 = 2^L`	std(b+L+1), b+L+1 (even landing, then R2 with x empty)
std/pk dirty	T below the clean point, not a landing	gen 2 (§3.3)
N/H landing	T = an N/H landing	halt or nested: excluded by I (§5)
R landing	T = an R landing	a reset into another counter: excluded by I (§5)

3.3 Gen 2 (dirty overflow, T not a landing)

Let k_s (r_s) be the barrier at T (k swept by every landing below T), v = T - 2k_s >= 1 the E-counter after the overflow's phi, u = tz(v). Then q = 2u is even and R2 gives x with E-bits K = k_s >> u, O-bits g = v >> (u+1) < 2^tz(K) (pk: plus the O-bit 1 worth 2^(L-1-u)), and n = b+1+u bounces. - g = 0: x is clean: std(K + n), n / pk(2^(L-1-u) + K + n), n. - g > 0: the O-bits g sweep up like a gen-1 orbit (T-count 2g + counter). All their landings have T_x < 2^(lowK+1), lowK = tz(K) (the H point of this orbit is T_x = 2^lowK). At T_x = 2^(lowK+1) the carry merges into K and the word is clean: std(K - 2^lowK + 2g + j) / pk(2^(L-1-u) + K - 2^lowK + 2g + j). If n + 1 > 2^(lowK+1) - 2g the overflow comes after the merge: next clean state std/pk(... + n), n.

4. The invariant I

For a clean state (typ, N, m): - I0: 1 <= m <= N (pk: N >= 2). - Parity class P (N = m mod 2): - std, N even: 2N <= 3m + 6 - std, N odd: N <= 2m + 3 - pk, N even: N <= 2m + 3 - pk, N odd: 2N <= 5m + 6 - Broken parity X (N != m mod 2): N <= m + 3 (std or pk).

In P, N even <=> m even <=> i = 0. The asymptotic shape is m/N >= 2/3, 1/2, 1/2, 2/5; the real run stays inside with room (min m/N: 0.78, 0.58, 0.50, 0.44 over 1M cycles), and in X it only ever has N = m+1 (after pk with k = 1).

5. Lemma S (safety): if I holds, the step B never halts

Danger needs a small m. An N/H landing at the overflow needs b + 1 <= 2^(L-1) (std: 2k + b + 1 <= 3*2^(L-1) with 2k > 2^L; pk: 2r + b + 1 <= 2^(L-1)). With N + 1 = (2k+1)2^i this means m + 2 <= 2^(a-1) <= N/2 for i = 0 (a = bitlen(N) - 1), i.e. N >= 2m + 4, and N >= 4m + 7 for i >= 1. I excludes both in every class (largest allowed: N <= 2m+3 for i = 0, N <= 2.5m+3 for i >= 1). R landings lie below the same thresholds, so they are excluded too.
Which states are dirty under I. Dirty std needs b < 2^(L+1) - 2k < 2^L < 2k, which gives N > 2m + 5 when i >= 1 and N > m + 5 for X: so only std in P with i = 0. Dirty pk needs b < 2^L <= 2k: i >= 2 needs N > 4m + 15, X needs N > m + 5 (i = 0) or is impossible (i = 1): so only pk in P with i in {0, 1}.
Each dirty state sits in its final gap. (a = bitlen(N) - 1) - std, i = 0: T = N + m + 2 >= 5N/3 > 32^(a-1) (from 2N <= 3m+6) and T < 2^(a+1) (dirty), so N < 1.22^a, bit a-2 of k is 0, and T lies after the last landing T_{a-2} = 3*2^(a-1): barrier k_s = 3*2^(a-2). - pk, i = 0: T = N - 2^a + m + 2 >= 1.5N - 2^a + 1 > 2^(a-1) = T_H (from N <= 2m+2) and T < 2^a, so r < 2^(a-2) and T lies after the H point: r_s = 2^(a-2). - pk, i = 1: T = (N-1)/2 - 2^(a-1) + m + 3 >= 0.9N - 2^(a-1) + 1.3 > 2^(a-2) = T_H (from 2N <= 5m+6) and T < 2^(a-1), so r < 2^(a-3): r_s = 2^(a-3). - In all three, T is even (parity class), so v = T - 2k_s is even and u >= 1.
Gen 2 merges before its overflow. lowK = tz(K) <= L - 3, so 2^(lowK+1) <= 2^(L-2), while n = b+1+u > m + 2 > 2^(a-1) (i = 0, both types) or > 0.4*2^a (pk i = 1). So n + 1 > 2^(lowK+1): the overflow comes after the merge and sees a clean counter (std overflow: q even; pk overflow: q odd only at the all-ones point, a harmless reset).

So under I the run from one clean state to the next passes only R1, R2 and resets with x empty.

6. Lemma C (closure): I(s) implies I(B(s))

Every next state has N' = m' + D with D >= 0, so I0 holds; the class bound is a bound on D. - std k=0, pk k=0, top reset, pk merge-at-overflow: D = 0. - std k=2^p / std clean, next pk(2k+b), b, D = 2k + b - b = 2k, P class: - i = 0, P (m even): N' = N + m + 1 odd, need 2N' <= 5b + 6, i.e. 2N <= 3m + 9. True. - i = 0, X (m odd): N' even, need N <= m + 4. True. - i >= 1: 2k = (N+1)/2^i - 1 <= (N-1)/2; N' has the parity of b = m+1+i. Both bounds (2k <= b+3 when even, 4k <= 3b+6 when odd) follow from N <= 2m+3. - pk k=2^p, next std(k+b), b: k = 1 gives X with D = 1. Otherwise P, N' has the parity of b. i = 0, P: k = N/2 <= m + 1.5 and N' is odd (k, m even). i = 0, X: 2k = N <= m + 3 <= b + 6. i >= 1: k <= (N+1)/4; in P, N' is even only when i is even (>= 2), and then 2k <= (N+1)/4 <= b + 6. In X, 2k <= m/2 + 2. - pk clean, next std(2r+b), b, D = 2r < k <= (N+1)/2^(i+1), P class; N' has the parity of b. Bounds: 4r <= b+6 (N' even), 2r <= b+3 (N' odd). - i = 0, P: b odd, 2r < k <= m + 1.5. i = 0, X: 4r < 2k = N <= m + 3. - i >= 1, P (m odd): N' is even only for i even (>= 2), and then 4r < 2k <= (N+1)/4. For i odd, 2r < k <= (N+1)/4. Both hold with N <= 2.5m+3. - i >= 1, X: 4r < 2k <= (N+1)/2 <= m/2 + 2. - dirty std / pk (only the three kinds of §5.3), K = 2^lowK * (3 for std, 1 for pk), lowK = L-2-u: - g = 0: D = 3*2^lowK. lowK = 0 gives D = 3, X class: N' <= n + 3. lowK >= 1: D even, P. - merged: D = 2^(lowK+1) + 2g < 2^(lowK+2) <= 2^(L-u), even, P. - Parity of N' = parity of n = parity of u (m even for i = 0; m odd and n = m+3+u for pk i = 1). Bounds: D <= n + 3 always (D < 2^(L-1) <= 2^(a-1) < n). The strict ones (std N' even: 2D <= n + 6) need u even >= 2, and then D < 2^(L-2) < n/2.

7. Conclusion

7.1 Non-halting

Init gives (std, 1, 1), which satisfies I. By S and C, every step B is a finite run of R1/R2 (and resets with x empty) that ends in a clean state with I, and m' >= m + 1. So the machine runs forever.

7.2 Why it is not a cryptid

Safety comes from inequalities on (N, m) and the octave of N, not from residues of long orbits. The only arithmetic facts used are parities (N = m mod 2 in class P, T even at dirty overflows). Under I the dirty orbits are always past every landing (§5.3).

7.3 Machine 349

349 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- is Eqv_v3 TM518 = this table started in F. From F the run reaches K('',0,1), i.e. (std, 0, 1), at step 14. Next comes (std, 2, 2) by std k=0, which satisfies I. The same proof applies from there.

8. Checks (scripts in `scripts/hunt/`, outputs in `work/`)

V1: scripts/validate_rules.py (observe stage): R1, R2, R3, R4, phi^j, big steps 200/200 each; R5 recorded. Blank-tape init exact.
V2: cf_vs_phi.py closed form B vs phi iteration (step.clean_step) on 60,000 random states (seed 2), all cases: 0 mismatches. 110,000 more cross-checks at m up to 2^60 inside closure_random.py.
V3: cf_vs_tm.py closed form B vs direct TM simulation (tools/sim.py) per case, random and constructed (overflow placed on a landing), seed 13: 1,587 instances, all equal (100 per case; the rare gen-2 cases 42 / 40 / 4 / 1). work/hunt_cf_vs_tm.json.
V4: closure_check3.py exhaustive: every state with I and m <= 1300 (83,499 + 772,875 states): next state satisfies I, no danger. lemma_check.py exh 1 1300: lemmas L1 (who is dirty), L2/L3 (final gap, u >= 1, merge before overflow), L4 (closure) on all 856,374 states.
V5: closure_random.py: 4,200,000 boundary-hugging random states (m up to 2^60 and up to 2^14); lemma_check.py rand: 1,000,000 states. 0 failures.
V6: traj_inv.py: I at every clean state of the blank run, 17,000,000 cycles (m = 43,683,205). traj_inv_start.py: from start F, I at all 999,999 states after (std, 0, 1).

9. Open before formalizing

§3.1 and §3.3 are stated from the phi closed form; the Rocq version needs them as lemmas on phi^j over O/E-interleaved words (the observe-stage phij validation is the informal evidence).
Template: BECv5 TM1/TM2 (LC0 std counter, R n m, RIncs, ROv). New pieces: the pk counter with its own overflow, the gen-1/gen-2 dirty orbits (needed only in their final gap), resets with empty x, and I as progress_nonhalt_cond.