BB(6) hunt
Machines / R2

1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LD0RC

R2Claimed elsewhereBell eats counterbbchallenge ↗Explorer

Upstream result

Claimed elsewhere

The blank-start machine never halts: BECv10.v.TM27 ↗. Recorded commit time: 2026-10-13T13:42:06Z. First public push time is not established.

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

BECv1 tm108 twin (E1, F0 differ): 110/010 bell eats a binary counter; eat size varies, left language open

Upstream
The blank-start machine never halts: BECv10.v.TM27 ↗. Recorded commit time: 2026-10-13T13:42:06Z. First public push time is not established.
Status
Externally Solvedsize invariant · updated 2026-10-10Not blocking · Stuck at the size invariant stage. Answer Q1–Q3 whenever; a “no” redirects the work.
idle since Oct 10 15:08 · status.json 2026-10-10
Class
Bell eats counterours: Bell eats counter (sheet) · ours adds: tm108-like 110/010 bell eats a 3-cell-digit binary counter; eat size varies (not BECv1) · low confidence
On the list
not on BB6_holdouts_663.txt (line 659 of the previous list) · historical 740 line 659
R2eqv ×1sim 1e15
Your calls on file 6
priority call (answered)
Med confidence: spend a proof-prep stage deriving the size invariant (pending-t height < log2 N - 2) natively, or park R2 until #29's eat work gives a shared counter/shift lemma?
parked
Waiting (auto-applied wait_shared, 2026-10-10): R2 parks until the joint R3/R2 crossing-lemma stage and #29 report on the same size lemma.
funded
option: size_invariant · date: 2026-10-10 · auto: true
2026-10-10 · deepen
Spend a deepen stage on the left-word language and the eat size e', starting with an early cryptid test, or park R2 behind its sibling #29? (Dennis: go with all recommendations (2026-10-10))
2026-10-10 · size_invariant
Spend one stage proving R2's size invariant (every pending t clears before the next eat) and then write proof.md, or park R2 until #29's eat work gives a shared lemma? (auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was at lunch). Override any time.)
decision.json · answered 2026-10-10: wait_shared
R2's size invariant is reduced to one inequality that needs a crossing lemma near powers of two: park R2 until #29/R3's size-invariant stages report, fund an R2 crossing-lemma stage now, or park it for good? Decisions →

Mechanism

How it works: 3 notes
  • Tape = L | bell 1 (110)^e (010)^f 1 0^inf, e+f = N per epoch; each round e+1, f-1 and L (binary counter, 3-cell digits) gains 1/2.
  • At f = 0 the bell eats the low 3e'-2 cells of L: f' = N, e' = 1 (odd last round) or 2..47 (even); L then mixes digit kinds.
  • Exact so far: sweeps R1-R4 and INC2 on pure counters; open: carry/eat on mixed words. tm108 cert: 9/12 hold (HL2, HR2, HE2 fail).

Figures for Checkpoint A

Fig 1 · Blaze, 100 million steps

Overall shape: the left edge (counter side) versus the right edge (bell side) over time.

Blaze, 100 million steps
bbchallenge-blazeStart blankRows Blaze time blocks of 131,072 stepsWindow cells -1929..263, 1 px = 2.74 cellsColors 0 1 1 only part of the time in that pixel's block
Rows: (each averaged), 763 blocks to step 1e8, stretched to 500 px · Window: Blaze image: 1,097 columns of 2 cells = the visited span at 1e8, stretched to 800 px · Colors: no head
Fig 2 · Rounds aligned at the bell boundaryQ1

Left of red: the word L, cell by cell. Right of red: one column per bell block. Compare rows.

Rounds aligned at the bell boundary
customStart blankRows one row per clean round startWindow cells -80..-1, 1 px = 0.33 cellsColors 1 0 (left word L) never visited boundary cell b (a 1) one 110 block one 010 block beyond the tape
Rows: (E0 -> A turn landing on the boundary cell b of 1 (110)^e (010)^f 1), i.e. every second round of an epoch: 198 rows, steps 250,017..469,936 · Window: (3x scale), counted from the boundary cell b; then b (red); then 112 columns in block units (1 column = one 3-cell block) · Colors: black right of
Fig 3 · Close-up around one resetQ2

Rows every 40 steps. Follow the white bell region's right border down to where the picture changes.

Close-up around one reset
bbchallenge-defaultStart mid-run: step 290,000Rows every 40 stepsWindow cells -266..51, 1 px = 0.5 cellsColors 1 0 or unvisited head (last move right/left)
Start: configuration from the blank-tape run · Rows: 601 rows, steps 290,000..314,000 · Window: (2x scale); absolute positions of the blank-tape run (head at -116 at step 290,000)
More figures (1)Fig 4: bbchallenge default view, 10,000 steps
Fig 4 · bbchallenge default view, 10,000 steps

The site's own first view, for comparison with the bbchallenge page.

bbchallenge default view, 10,000 steps
bbchallenge-defaultStart blankRows every step 0..9,999Window cells -200..199, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Rows: squeezed into 500 px by the site's bilinear filter (about one sample every 20 steps)
Rules (9/9 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
R1 A-sweep over 110 (as BECv1 HR1 shape)
l A> (110)n 1 r
⟶ l (001)n A> 1 r
any l, r7n✓200/200
R4 A-sweep over 101 (= tm108 HR1)
l A> (101)n r
⟶ l (010)n A> r
any l, r7n✓200/200
R2 B-sweep back over 010 (= tm108 HR3)
l (010)n <B r
⟶ l <B (101)n r
any l, r3n✓200/200
R3 B-sweep back over 001 (uses F0, ours only)
l (001)n <B r
⟶ l <B (100)n r
any l, r3n✓200/200
INC2 pure counter, suffix 001 (two rounds)
0∞ 1 W(v) 001 A> 1 (110)e (010)f+2 1 0∞
⟶ 0∞ 1 W(v+1) 001 A> 1 (110)e+2 (010)f 1 0∞
W(v) = v in k blocks 000/001, MSB first, 0<=k<=7; v = 2^k-1 overflows to 1 (000)^(k+1) 001; e>=1, f>=0—✓200/200
INC2 pure counter, suffix 000 100 101
0∞ 1 W(v) 000100101 A> 1 (110)e (010)f+2 1 0∞
⟶ 0∞ 1 W(v+1) 000100101 A> 1 (110)e+2 (010)f 1 0∞
as above (overflow 1 (000)^(k+1) 000100101)—✓200/200
ROUND (blank run): bell e+1, f-1
0∞ L A> 1 (110)e (010)f+1 1 0∞
⟶ 0∞ L' A> 1 (110)e+1 (010)f 1 0∞ (next round)
every round from blank to step 100,000,000,000; L' = L with the counter's half-step (carry depth = turn offset)—✓3935408/3935408
RESET-odd: epoch ends on a deep-turn round
0∞ L A> 1 (110)N 1 0∞ (f = 0, last round odd)
⟶ 0∞ L* A> 1 (110)1 (010)N 1 0∞; boundary 1 cell left
all 480 odd resets from blank to step 100,000,000,000—✓480/480
RESET-even: bell eats 3e'-2 cells of L
0∞ L A> 1 (110)N 1 0∞ (f = 0, last round clean)
⟶ 0∞ L* A> 1 (110)e' (010)N 1 0∞; boundary 3e'-2 cells left
e' in 2..47, not yet predicted from L; all 602 even resets from blank to step 100,000,000,000 (boundary shift 2-3e' checked on all 1081/1081 resets)—✓602/602
Compressed historythe tape as 0∞ L A> 1 (110)e (010)f 1 0∞ at 35 moments: where the rules are read off
0∞ L A> 1 (110)e (010)f 1 0∞
stepN (bell blocks e+f before the reset)e' (blocks gained = new e)last round of the epoch (odd = deep turn)|L| (cells left of the bell)
2912even1
9431odd4
24141odd10
53956even13
1,094111odd10
1,953121odd13
3,057132even22
4,636151odd25
6,547161odd31
9,9311715even40
14,269323even13
21,099354even22
3,099,0522104even37
32,682,32147319even91
129,079,1197881odd49
341,116,1211,0781odd76
706,429,6431,38910even67
1,276,772,6251,7185even64
2,136,234,5222,0791odd49
3,289,358,7812,3421odd100
4,788,879,5622,6751odd79
6,719,405,5983,0431odd73
9,150,305,2873,3821odd76
12,157,709,7973,73738even130
15,835,521,8784,1311odd61
20,140,233,9544,41327even112
25,100,220,7274,74715even82
30,839,942,0575,1212even79
37,434,155,6615,4681odd79
44,996,934,5015,8701odd58
53,613,204,2066,2111odd91
63,227,141,6186,58111even64
74,058,152,1856,9781odd91
86,245,624,5637,3801odd115
99,837,414,7767,80418even91
N (bell blocks e+f before the reset)last 7,804
7,8041291e11log xstep 29: N (bell blocks e+f before the reset) = 1step 94: N (bell blocks e+f before the reset) = 3step 241: N (bell blocks e+f before the reset) = 4step 539: N (bell blocks e+f before the reset) = 5step 1094: N (bell blocks e+f before the reset) = 11step 1953: N (bell blocks e+f before the reset) = 12step 3057: N (bell blocks e+f before the reset) = 13step 4636: N (bell blocks e+f before the reset) = 15step 6547: N (bell blocks e+f before the reset) = 16step 9931: N (bell blocks e+f before the reset) = 17step 14269: N (bell blocks e+f before the reset) = 32step 21099: N (bell blocks e+f before the reset) = 35step 3099052: N (bell blocks e+f before the reset) = 210step 32682321: N (bell blocks e+f before the reset) = 473step 129079119: N (bell blocks e+f before the reset) = 788step 341116121: N (bell blocks e+f before the reset) = 1078step 706429643: N (bell blocks e+f before the reset) = 1389step 1276772625: N (bell blocks e+f before the reset) = 1718step 2136234522: N (bell blocks e+f before the reset) = 2079step 3289358781: N (bell blocks e+f before the reset) = 2342step 4788879562: N (bell blocks e+f before the reset) = 2675step 6719405598: N (bell blocks e+f before the reset) = 3043step 9150305287: N (bell blocks e+f before the reset) = 3382step 12157709797: N (bell blocks e+f before the reset) = 3737step 15835521878: N (bell blocks e+f before the reset) = 4131step 20140233954: N (bell blocks e+f before the reset) = 4413step 25100220727: N (bell blocks e+f before the reset) = 4747step 30839942057: N (bell blocks e+f before the reset) = 5121step 37434155661: N (bell blocks e+f before the reset) = 5468step 44996934501: N (bell blocks e+f before the reset) = 5870step 53613204206: N (bell blocks e+f before the reset) = 6211step 63227141618: N (bell blocks e+f before the reset) = 6581step 74058152185: N (bell blocks e+f before the reset) = 6978step 86245624563: N (bell blocks e+f before the reset) = 7380step 99837414776: N (bell blocks e+f before the reset) = 7804
e' (blocks gained = new e)last 18
381291e11log xstep 29: e' (blocks gained = new e) = 2step 94: e' (blocks gained = new e) = 1step 241: e' (blocks gained = new e) = 1step 539: e' (blocks gained = new e) = 6step 1094: e' (blocks gained = new e) = 1step 1953: e' (blocks gained = new e) = 1step 3057: e' (blocks gained = new e) = 2step 4636: e' (blocks gained = new e) = 1step 6547: e' (blocks gained = new e) = 1step 9931: e' (blocks gained = new e) = 15step 14269: e' (blocks gained = new e) = 3step 21099: e' (blocks gained = new e) = 4step 3099052: e' (blocks gained = new e) = 4step 32682321: e' (blocks gained = new e) = 19step 129079119: e' (blocks gained = new e) = 1step 341116121: e' (blocks gained = new e) = 1step 706429643: e' (blocks gained = new e) = 10step 1276772625: e' (blocks gained = new e) = 5step 2136234522: e' (blocks gained = new e) = 1step 3289358781: e' (blocks gained = new e) = 1step 4788879562: e' (blocks gained = new e) = 1step 6719405598: e' (blocks gained = new e) = 1step 9150305287: e' (blocks gained = new e) = 1step 12157709797: e' (blocks gained = new e) = 38step 15835521878: e' (blocks gained = new e) = 1step 20140233954: e' (blocks gained = new e) = 27step 25100220727: e' (blocks gained = new e) = 15step 30839942057: e' (blocks gained = new e) = 2step 37434155661: e' (blocks gained = new e) = 1step 44996934501: e' (blocks gained = new e) = 1step 53613204206: e' (blocks gained = new e) = 1step 63227141618: e' (blocks gained = new e) = 11step 74058152185: e' (blocks gained = new e) = 1step 86245624563: e' (blocks gained = new e) = 1step 99837414776: e' (blocks gained = new e) = 18
last round of the epoch (odd = deep turn)last even
not plottable
|L| (cells left of the bell)last 91
1301291e11log xstep 29: |L| (cells left of the bell) = 1step 94: |L| (cells left of the bell) = 4step 241: |L| (cells left of the bell) = 10step 539: |L| (cells left of the bell) = 13step 1094: |L| (cells left of the bell) = 10step 1953: |L| (cells left of the bell) = 13step 3057: |L| (cells left of the bell) = 22step 4636: |L| (cells left of the bell) = 25step 6547: |L| (cells left of the bell) = 31step 9931: |L| (cells left of the bell) = 40step 14269: |L| (cells left of the bell) = 13step 21099: |L| (cells left of the bell) = 22step 3099052: |L| (cells left of the bell) = 37step 32682321: |L| (cells left of the bell) = 91step 129079119: |L| (cells left of the bell) = 49step 341116121: |L| (cells left of the bell) = 76step 706429643: |L| (cells left of the bell) = 67step 1276772625: |L| (cells left of the bell) = 64step 2136234522: |L| (cells left of the bell) = 49step 3289358781: |L| (cells left of the bell) = 100step 4788879562: |L| (cells left of the bell) = 79step 6719405598: |L| (cells left of the bell) = 73step 9150305287: |L| (cells left of the bell) = 76step 12157709797: |L| (cells left of the bell) = 130step 15835521878: |L| (cells left of the bell) = 61step 20140233954: |L| (cells left of the bell) = 112step 25100220727: |L| (cells left of the bell) = 82step 30839942057: |L| (cells left of the bell) = 79step 37434155661: |L| (cells left of the bell) = 79step 44996934501: |L| (cells left of the bell) = 58step 53613204206: |L| (cells left of the bell) = 91step 63227141618: |L| (cells left of the bell) = 64step 74058152185: |L| (cells left of the bell) = 91step 86245624563: |L| (cells left of the bell) = 115step 99837414776: |L| (cells left of the bell) = 91
Template comparisonBECv1_6x2_solved.v BECv1: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB0RA
B1LC0LF
C1LE0LD
D1LB---
E1RA1LBtpl 1LE
F0LDtpl 0LB0RC

differs from the template

file
BECv1_6x2_solved.v:872
module
BECv1 (Section in verify/BECv1.v); tm108 / nonhalt108, cert Build_BEC_cert_v1 B A E A ... 1 0 0
machine
1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LE_0LB0RC (2 transitions apart)
diff
E1: 1LB (ours) vs 1LE (tm108); F0: 0LD (ours) vs 0LB (tm108)
note
scripts/template_check.py runs tm108's 12 cert hypotheses on both machines: tm108 12/12 (sanity), ours 9/12 (25/25 each). Fail 0/25: HL2 (binary carry 1 <E -> <E 1, needs E1=1LE), HR2 (00 marker step, uses F0) and HE2 (marker birth). So the sweeps and the eat pieces HE0/HE1/HE3 carry over; the counter (3-cell digits), the marker (a 110|010 border, not 00) and the eat size (3e'-2 cells, e' = 1..47, not a = 1) do not.
Proof strategy & riskshow the formal proof will go · 3 risks to watch

Deepen before any proof: (1) derive the carry automaton on mixed digit words and the eat automaton (predict e' from L); (2) find a language for L closed under INC2/ROUND and RESET, with a size bound N >= c|L|, and closure-fuzz it; (3) then a BECv1-style file with an Inductive digit list, or a CTL/RWL certificate if the language is regular.

  • ▲The eat size e' depends on the counter's digits at the reset (arithmetic feedback); if the reachable L words are not regular, a hand proof is hard.
  • ▲Real left words with a too-small bell (N < |L|) do halt (2/300 replay starts), so the invariant needs a quantitative N vs |L| bound.
  • ▲Sibling #29 (F0 = 0LB) looks similar but its trajectory differs (1e8: span -1917..265 vs ours -1929..263); a shared proof is not guaranteed.
Stats & provenance1011 steps simulated · 23,535 cells · the status in full · files
simulated
1011 steps
tape
23,535 cells
growth
span ~ t^(1/3): 453 cells at 1e6, 2,193 at 1e8, 10,590 at 1e10 (4,082 nonzeros), 23,535 at 1e11; bell N = 7822 after 1082 epochs
status now
Waiting (auto-applied wait_shared, 2026-10-10): R2 parks until the joint R3/R2 crossing-lemma stage and #29 report on the same size lemma. Funded size_invariant stage (2026-10-10) ended STUCK; confidence stays med. No inductive size invariant was found. The reduction is now sharp: ball gaps never grow (20,596,783 trajectory ball-eats to N = 1e7 and 743,436 random, 0 violations), so safety reduces to each ball's first t-epoch. Every birth outside one special case has 2^h1 <= V*/2 (by hand; 7,454,109 trajectory and 188,785 random births). So non-halting follows from one inequality, R1: T_k + 1 <= I_k (total value at epoch start below the epoch's INC count), plus Delta+1 < 2^m in the special case V* = 2^m with two odd eats. R1 holds at all 808,539 epochs to N = 1e7, with T/I <= 0.28 for N >= 2^13 and <= 0.13 for N >= 2^14 to 1e7. It is not provable from size summaries: near-power-of-two random states break the candidates (Ja 44, Jb 601, Jc 668 of 2000), because during a crossing V* = 2^m + delta the whole ball potential moves into T. Needed: a crossing lemma bounding sum over balls of 2^(Z_gap(2^m + delta_k)) along a passage of V* through 2^m. (status.json, 2026-10-10)
observer's note
Low confidence. ROUND/RESET structure holds on every round from blank to 100,000,000,000 steps (0 exceptions) and INC2 is exact on pure counters, but the left-word language and the eat size are not derived. Not a cryptid candidate yet: no halt depends on the eat sizes in the tests.
files
observe.json · notes.md · status.json

Proof & checks

No proof work yet.

Files

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

namesizechanged
notes.md ↓25 KB2026-10-10 15:08
status.json ↓1.7 KB2026-10-10 14:45
observe.json ↓13 KB2026-10-10 09:58
deepen.json ↓9.6 KB2026-10-10 14:22
decision.json ↓2.9 KB2026-10-10 14:45
decisions/2 items2026-10-10 14:20
img/4 items2026-10-10 09:53
scripts/14 items2026-10-10 14:02
epochs_1e11.txt ↓91 KB2026-10-10 09:58
qsim.jsonl ↓3.3 KB2026-10-10 09:54
rounds_3e7.txt ↓1.5 MB2026-10-10 09:58
template_check.json ↓1.0 KB2026-10-10 09:56
validation.json ↓346 B2026-10-10 09:51
status.json in full
{
 "tm": "1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LD0RC",
 "status": "STUCK",
 "stage": "size_invariant",
 "updated": "2026-10-10",
 "reason": "Waiting (auto-applied wait_shared, 2026-10-10): R2 parks until the joint R3/R2 crossing-lemma stage and #29 report on the same size lemma. Funded size_invariant stage (2026-10-10) ended STUCK; confidence stays med. No inductive size invariant was found. The reduction is now sharp: ball gaps never grow (20,596,783 trajectory ball-eats to N = 1e7 and 743,436 random, 0 violations), so safety reduces to each ball's first t-epoch. Every birth outside one special case has 2^h1 <= V*/2 (by hand; 7,454,109 trajectory and 188,785 random births). So non-halting follows from one inequality, R1: T_k + 1 <= I_k (total value at epoch start below the epoch's INC count), plus Delta+1 < 2^m in the special case V* = 2^m with two odd eats. R1 holds at all 808,539 epochs to N = 1e7, with T/I <= 0.28 for N >= 2^13 and <= 0.13 for N >= 2^14 to 1e7. It is not provable from size summaries: near-power-of-two random states break the candidates (Ja 44, Jb 601, Jc 668 of 2000), because during a crossing V* = 2^m + delta the whole ball potential moves into T. Needed: a crossing lemma bounding sum over balls of 2^(Z_gap(2^m + delta_k)) along a passage of V* through 2^m.",
 "funded": {
  "option": "size_invariant",
  "date": "2026-10-10",
  "auto": true
 },
 "priority_call_answered": "Med confidence: spend a proof-prep stage deriving the size invariant (pending-t height < log2 N - 2) natively, or park R2 until #29's eat work gives a shared counter/shift lemma?",
 "confidence": "med",
 "parked": "Waiting (auto-applied wait_shared, 2026-10-10): R2 parks until the joint R3/R2 crossing-lemma stage and #29 report on the same size lemma."
}
observe.json contract (tools/README-card.md):
1 contract warning
  • rank: not an int