BB(6) hunt
Machines / #23

1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---

#23Claimed elsewhereBell eats counterbbchallenge ↗Explorerparent: #2

Upstream result

Claimed elsewhere

The blank-start machine never halts: PR_BEC.v.TM3 ↗.

Absent from the current 663 holdout list. Earlier local observations remain below.

space-time diagram, first 10,000 steps from blank
The first 10,000 steps from a blank tape. Time runs down; white is 1.
About this picture

The standard picture (bbchallenge.org's Default view): each row is the whole tape at one step, time runs downward, and the head's path draws the pattern.

bbchallenge-defaultStart blankRows steps 0 → 10,000, top to bottomWindow cells −200..199, left to rightColors 1 0 or unvisited

Overview

In one sentence

neighbour of #2: one transition away (A1 0RA vs 0RF); its run differs and #2's proof does not carry over (status.json relation)

Upstream
The blank-start machine never halts: PR_BEC.v.TM3 ↗.
Status
Externally Solvedinformal proof · updated 2026-10-10Not blocking · Stuck at the informal proof stage.
idle since Oct 12 14:07 · status.json 2026-10-10
Informal proof
proof.mdconditional; see Proof for what is still open
Class
Bell eats counter
On the list
not on BB6_holdouts_663.txt (line 627 of the previous list) · historical 740 line 627
#23eqv ×1sim 1e15
Derived from
1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---#2 Kill claimed
Your calls on file 2
parked
Parked 2026-10-10 (auto-applied recommendation): Lemma T and shape condition K are new math; reopen if the queue runs dry.
decision.json · answered 2026-10-10: park
Fund one more stage (at most 2 h) to prove Lemma T and find the shape condition K that closes twin #2's domain, or park it as STUCK? Decisions →

Mechanism

No observation of its own: neighbour of #2: one transition away (A1 0RA vs 0RF); its run differs and #2's proof does not carry over. Below are #2's figures, rules and history. #2's Checkpoint A questions (3) are on its page.

Figures

Fig 1 · One eating pass: ours vs SOMDCv6 TM7✓ Q1

Same start for both. Blue boxes mark ours' extra +1 passes; compare everything outside them with TM7's run.

One eating pass: ours vs SOMDCv6 TM7
bbchallenge-defaultStart constructed: 0∞ 11 D> (110)4 100 110 100 0∞ = S(L⁴ 1L1)Rows every step: ours 0..118Window cells -4..24, 1 px = 1/12 cellColors 1 0 head after a move R/L box: ours' extra +1 pass ▶: TM7's A1 (turns back) dashes: eater stops
Start: the same for both machines · Rows: TM7 0..44 (until the eater reads the 1-digit); same scale · Window: cell 12 px wide, step 8 px tall
Fig 2 · One full sweep: ours vs TM7✓ Q2

One full sweep each. Find pass 5 (a drain pass), then compare the drain zigzags that follow it.

One full sweep: ours vs TM7
bbchallenge-defaultStart constructed: 0∞ 11 D> (110)4 100 110 100 0∞ = S(L⁴ 1L1)Rows every step: ours 0..421Window cells -4..34, 1 px = 1/10 cellColors 1 0 head after a move R/L box: ours' extra +1 pass ▶: TM7's A1 (turns back) dashes: eater stops bracket: drain passes
Start: the same for both machines · Rows: TM7 0..237 (to the next S config); same scale · Window: cell 10 px wide, step 4 px tall · Colors: white bracket: no A1: same rules in both
Fig 3 · bbchallenge default view, first 10,000 steps✓ Q3viewer ↗

The site's view from blank: watch the white bells and the right edge of the digit region.

bbchallenge default view, first 10,000 steps
bbchallenge-defaultStart blankRows 10,000 steps squeezed into 500 px rowsWindow cells -200..199, 1 px = 1 cellColors 1 0 or never visited head after a move R/L
Rows: 1 px row = 20 steps; the site blends steps 20y+9 and 20y+10 · Colors: red/green: blended into the squeezed rows, as on the site
More figures (2)Fig 4–5: Left/right records to 1 billion steps · Blaze, 10 million steps
Fig 4 · Left/right records to 1 billion steps

White bell waves over a steadily growing right edge; the left edge barely moves (209 vs 4,692 cells).

Left/right records to 1 billion steps
bbchallenge-defaultStart blankRows the start, then one row per new leftmost or rightmost cellWindow cells -209..4,692, 1 px = 1 cellColors 1 0 or never visited head after a move R/L
Rows: 4,902 rows (209 left, 4,692 right) up to step 1e9; rows are not evenly spaced in time · Colors: zoomed out, the L digits (110 stripes) look grey and the bell is solid white
Fig 5 · Blaze, 10 million steps

Stacked bells; the right edge grows roughly like t^(1/3).

Blaze, 10 million steps
bbchallenge-blazeStart blankRows Blaze time blocks of 16,384 stepsWindow cells -54..953, 1 px = 1.26 cellsColors 0 1 a cell that was 1 for only part of its 16,384-step block
Rows: (611 rows, each averaged), stretched to 500 px (1 px ~ 20,000 steps) · Window: 1,008 Blaze columns of 1 cell each, stretched to 800 px
Rules (6/6 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
Sweep
0∞ 11 D> r 0∞
⟶ 0∞ 11 D> eat(r) 0∞ (wall 1 cell left)
r over L=110,0=000,1=100. Eater, k=0: 0->L,k+1 | L->L,k+1,+1 rest* | 1->L, count mode. Count mode k>=1: L->L, eater again, +1 rest* | 1->L,k-1 | 0->0,(k-1)/2 if k odd; 0->1,(k-2)/2 if even. Right end: k=0->1; odd->0; even->1; repeat. *=new vs TM7—✓502/502
Eater enters L (new)
1 D> 110 X
⟶ 1 111 D> inc(X)
A1 fires here. inc = +1 on the 0/1 digits, little-endian, L skipped; overflow appends 100. TM7: 1 D> 110 X -> 1 111 D> X in 11 steps (no pass)6j+13 (j = digits before the first 000 in X)✓1393/1393
Drain pass enters L (new)
B> 1 110 X
⟶ 1 111 D> inc(X)
A1 fires here and the eater restarts after the L (115 of 208 sweeps to 1e9). TM7: B> 1 110 X -> 1 111 D> X in 10 steps (no pass)6j+12 (j as above)✓1393/1393
Eater over 0s
11 D> (000)a
⟶ 11 (111)a D>
—3a✓45/45
+1 pass: carry
B> (100)a 000
⟶ (000)a <C 100
at tape end: B> (100)^a 0^inf -> (000)^a <C 1 0^inf3a+1✓90/90
+1 pass: skip L, return
B> (110)a
⟶ (011)a B>
return: (011)^a <C -> <C (110)^a and (000)^a <C -> <C (000)^a, 3a each3a✓135/135
Compressed historythe tape as 0∞ 11 D> (110)n T 0∞ at 40 moments: where the rules are read off
0∞ 11 D> (110)n T 0∞
stepnT
501
1611
91311
31861
80980L11
1,93014111
3,971191,111
6,93221101L1
10,625231LL1L001
16,17632111
24,427381
34,85041111L11
47,929471L01101
64,518531L01101
84,5395710LL0011
436,857105111LL0101
1,355,2991591LL10L01001
2,835,01421000LL010011
5,658,65626910110L111
9,961,61232600L1111001
16,012,4323811LLL1L0011101
23,139,1834371LL11101011
33,896,5195031LLLL10101111
47,901,4395671L111L100001
65,193,5816280LL11L0011001
83,603,98668601L0L0L100101
108,594,88675001LLL0L1101101
138,455,6508160L0L01LL000011
173,399,6348840LL1LL10011011
208,657,71594111L1LLL1000111
254,952,9211,0160LLLLL101011111
308,436,9931,0800LLL0101L000001
368,117,8871,147111L10110001
426,162,8321,2011L0L01L1001001
499,947,9581,2720LLL11L00111001
582,161,1081,34110L1L10100101
673,443,4981,4091LLL0L1L10110101
761,279,3811,4720LL1LL0L10101101
871,368,5691,5561,001,000,011
992,340,7151,61910L11LL0100011
nlast 1,619
1,619059.9e8log xstep 5: n = 0step 16: n = 1step 91: n = 3step 318: n = 6step 809: n = 8step 1930: n = 14step 3971: n = 19step 6932: n = 21step 10625: n = 23step 16176: n = 32step 24427: n = 38step 34850: n = 41step 47929: n = 47step 64518: n = 53step 84539: n = 57step 436857: n = 105step 1355299: n = 159step 2835014: n = 210step 5658656: n = 269step 9961612: n = 326step 16012432: n = 381step 23139183: n = 437step 33896519: n = 503step 47901439: n = 567step 65193581: n = 628step 83603986: n = 686step 108594886: n = 750step 138455650: n = 816step 173399634: n = 884step 208657715: n = 941step 254952921: n = 1016step 308436993: n = 1080step 368117887: n = 1147step 426162832: n = 1201step 499947958: n = 1272step 582161108: n = 1341step 673443498: n = 1409step 761279381: n = 1472step 871368569: n = 1556step 992340715: n = 1619
Tlast 10L11LL0100011
1e9158.7e8log-logstep 5: T = 1step 16: T = 1step 91: T = 11step 318: T = 1step 1930: T = 111step 3971: T = 1111step 16176: T = 111step 24427: T = 1step 871368569: T = 1001000011
Template comparisonSOMDCv6.v TM7: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB0RFtpl 0RC
B1LC0RE
C0LC0LD
D1RD1LB
E0RF1RA
F0RB---

differs from the template

file
SOMDCv6.v:1626
module
TM7 (line 1626); TM8 (line 1874) has the identical proof
machine
1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- (1 transition apart)
diff
A1: 0RC (TM7) / 0LC (TM8) -> 0RF; other 11 transitions equal
note
Config S(r)=0^inf 11 D> r and digits 110/000/100 carry over (no other digit to 1e9). TM7's RIncs map fits 1/208 sweeps; with '+1 to the rest at every L entered' (eater and drain clause) it fits 208/208; eater clause alone: 95/208.

1Same machine as #2?

What to check here: whether this machine is its parent's table under a renaming, and whether its run follows the parent's (computed from the two machine strings).

status.json names #2 as the parent (1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---); relation: “neighbour of #2: one transition away (A1 0RA vs 0RF); its run differs and #2's proof does not carry over”. Everything below is computed from the two machine strings, not read from notes.

✗ Not the same table. No renaming of #2's states, with or without mirroring, gives this machine's table. Closest: A→A, B→B, C→C, D→D, E→E, F→F (#2's state → this machine's), no mirror, where 1 of 12 transitions differ:

  • #2's A1 = 0RF predicts this machine's A1 = 0RF; it is 0RA.

Under that map: This machine starts in #2's state A, the same start as #2.

#2#2's row (read 0, read 1)σpredicted row: renamed by σthis machine's actual row
A1RB 0RF→ A1RB 0RF1RB 0RA✗start of #2start of this machine
B1LC 0RE→ B1LC 0RE1LC 0RE✓
C0LC 0LD→ C0LC 0LD0LC 0LD✓
D1RD 1LB→ D1RD 1LB1RD 1LB✓
E0RF 1RA→ E0RF 1RA0RF 1RA✓
F0RB ---→ F0RB ---0RB ---✓

Rows aligned by σ: each of #2's states X sits next to this machine's state σ(X). ✓ = the actual row equals #2's row with every target state renamed by σ; --- (halt) must stay ---. Searched: all 720 renamings × with/without mirror.

Fig P1 · bbchallenge default view: #2 and this machine, first 10,000 steps

Same view, same settings on both sides. Look for the same band structure: the tables differ in 1 transition(s) (listed above).

#2 (parent), from blank in its A
not rendered yet
this machine (#23), from blank in its A
not rendered yet
bbchallenge-defaultStart blankRows steps 0 → 10,000, top to bottomWindow cells −200..199, left to rightColors 1 0 or unvisited
tools/diagram.py <tm> --as-site (the site's 400×500 canvas)
Fig P2 · Long run, Blaze (speed): #2 and this machine, 100 million steps

The macro behaviour, identical settings on both sides: each picture is its machine's own visited span stretched to 800 px, so compare the shape and order of the bands, not their absolute width. Speed mode samples one cell per column, so a one-cell shift can swap orange and white inside a band; compare band edges, not colours.

#2 (parent), from blank in its A
not rendered yet
this machine (#23), from blank in its A
not rendered yet
bbchallenge-blazeStart blankRows steps 0 → 1e8Window the visited spanColors 1 0 at the sampled cell
Rows: one snapshot per row (Blaze time blocks), stretched to 500 px · Window: every k-th cell sampled, stretched to 800 px
tools/diagram.py <tm> --mode blaze --speed --as-site --steps 1e8

Trajectory numbers not computed yet: run python3 -B tools/killreview.py 1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- (about 10 s; cached in img/vs-parent.json).

Proof & checks

What is still open (status.json):

  • stuck: proof.md 3.3.5: closing invariant J = J4 and K; Lemma T (conjecture) and condition K (not found)

Files

machines/<tm>/: 6 entries · raw notes, status, scripts, images

namesizechanged
notes.md ↓9.1 KB2026-10-10 13:58
proof.md ↓43 KB2026-10-10 13:15
status.json ↓1.7 KB2026-10-12 14:07
decision.json ↓2.6 KB2026-10-10 13:58
scripts/2 items2026-10-10 06:23
check_proof.py ↓38 KB2026-10-10 13:15
status.json in full
{
 "tm": "1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---",
 "status": "STUCK",
 "stage": "informal_proof",
 "updated": "2026-10-10",
 "reason": "Parked 2026-10-10 (auto-applied recommendation): Lemma T and shape condition K are new math; reopen if the queue runs dry. Twin #2 of pilot #2 (A1 0RA vs parent 0RF). Pass 3 after skeptic review (1 fatal, 5 minor): all 5 minor gaps fixed (RIncs_eq re-parse inside Lemma C, compiled with Example sweep_LS01; Lemma D 1-or-L; canonical/#S<=1 in G and P; Lemma U replaces determinism; orbit claims scoped, 1.25 bound attained at sweep 2). FATAL gap remains: no inductive invariant J closes the domain theta(x) <= N (proof.md 3.3.5). Refuted: G, J0, J2, J3, J3 with any N >= N0 ((2^(m+1)-4, 00001), m = 4..20), J4. New: V* (L after p digits counts 2^p) makes the sweep exactly affine, V*(x') = N + c(x) (proved); Lemma T 2theta <= V* - 1 is a conjecture (exhaustive to 11 tokens); J4 := ends1 and V* <= 2N+1 fails at (257, 10000000L1) but 400 random J4 starts x 25 sweeps never leave the domain. Missing: a proof of T and a shape condition K on L positions bounding c(x) <= N + 3 that is preserved. Not a cryptid.",
 "proof_md": "proof.md",
 "check_script": "check_proof.py",
 "unclaimed": "Results row 1048: class only (Bell eats counter); no Discord",
 "stuck": "proof.md 3.3.5: closing invariant J = J4 and K; Lemma T (conjecture) and condition K (not found)",
 "parked": "Parked 2026-10-10 (auto-applied recommendation): Lemma T and shape condition K are new math; reopen if the queue runs dry.",
 "relation": "neighbour of #2: one transition away (A1 0RA vs 0RF); its run differs and #2's proof does not carry over",
 "parent": "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---"
}