BB(6) hunt
Machines / #28

1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_---0RA

#28Claimed elsewhereBell eats counterbbchallenge ↗Explorer

Upstream result

Claimed elsewhere

The blank-start machine never halts: BECv10.v.TM32 ↗. 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

tm10 sibling: 3-cell binary counter eats a unary run; 9 round rules predict 100% of rounds to 1e10

Upstream
The blank-start machine never halts: BECv10.v.TM32 ↗. Recorded commit time: 2026-10-13T13:42:06Z. First public push time is not established.
Status
Externally Solvedprove l9 (L9 open; flagged cryptid with #10) · updated 2026-10-12Parked · Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Park with #10 as one cryptid candidate. The 3 open questions are optional.
idle since Oct 12 08:59 · status.json 2026-10-12
Informal proof
proof.mdconditional; see Proof for what is still open
Class
Bell eats counterours: Bell eats counter (sheet) · ours adds: BECv1 tm10 with E1 = 1LB (3-cell binary counter with fillers + unary marker; eats shift the counter) · med confidence
On the list
not on BB6_holdouts_663.txt (line 596 of the previous list) · historical 740 line 596
#28eqv ×1sim 1e15
Your calls on file 8
priority call (answered)
Park #28 with #10 as one cryptid candidate, fund the shared Rocq rule reduction, or fund research on the shared Lemma X?
parked
Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Park with #10 as one cryptid candidate.
funded
option: prove_l9 · date: 2026-10-11
next
Cryptid protocol: AntiHydra-style Rocq rule reduction of the rule layer, shared with #10 and its twin, at low priority (decision.json).
2026-10-10 · close_chain
Fund one more stage to close the chain case and then write proof.md, write proof.md now with the chain case as a stated open lemma, or park? (auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.)
2026-10-10 · flush_proof
Fund one stage for the flush lemma and proof.md (hand route, BECv7-style carry relation), run a native CTL search first, or park? (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.)
2026-10-11 · prove_l9
Fund one more stage to prove L9 (PC < 2^(D+1) for words that start with 1) and then write proof.md, write proof.md now with L9 as an open lemma, or park? (Dennis: go with recommendations (2026-10-11))
decision.json · answered 2026-10-12: park_with_10
#28 is #10 mirrored and started in E, and the two orbits merge: park it with #10 as one cryptid candidate, fund the shared Rocq rule reduction now, or fund research on the shared Lemma X? Decisions →

Mechanism

How it works: 3 notes
  • Left: a binary counter in 3-cell blocks (1=100, 0=000, filler f=010 that carries skip). Right: tm10's 011 unary run with a 00 marker. Each round adds 1 and moves the marker one block left.
  • When the marker reaches the counter, one of 3 eats fires. EAT0f drops the low digit and fillers into the unary. EAT0z and EAT1 absorb the marker and shift the counter one cell right (phi).
  • The shifted blocks are debris (s=001). A carry that reaches an s re-encodes them (CARRY_S, recursive). On the blank run the debris is always gone before the next eat.

Figures for Checkpoint A

Fig 1 · bbchallenge default view, 10,000 stepsviewer ↗

The site's view: the counter sits at the left edge, the unary run to its right.

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: px row y blends steps 20y+9 and 20y+10, so about one sample every 20 steps
Fig 2 · One row per left entry into EQ1viewer ↗

Left edge pinned. Follow one dark diagonal down to the left band, then watch the band and the next diagonal.

One row per left entry into E
bbchallenge-defaultStart blankRows every entry into state E moving leftWindow cells 0..119, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Rows: 552 rows to step 40,000; every round start is one of them, and carries add a few more rows · Window: counted from each row's leftmost visited cell (frame = left), so only the 120 leftmost cells are shown
Fig 3 · Close-up: an EAT1 eatQ2

Compare the counter's 1-cells (columns left of the start head) in the top row and below the first left sweep.

Close-up: an EAT1 eat
bbchallenge-exploreStart constructed: 0∞ 100 000 010 1 <E 11 00 (011)6 0∞Rows every step: 141 rowsWindow cells -12..24, 1 px = 0.25 cellsColors 0 1 A B C D E F
Rows: step 0 to step 140 (the eat ends at step 37, then the next round runs) · Window: (each cell 4x4 px); cell 0 = the start head (the LSB cell b) · Colors: head cell coloured by state
More figures (2)Fig 4–5: Blaze, 100 million steps · Left records, left edge pinned, 1e9
Fig 4 · Blaze, 100 million stepsviewer ↗

Whole run at a glance: left edge grows like a bell, the right edge slowly.

Blaze, 100 million steps
bbchallenge-blazeStart blankRows Blaze time blocks of 131,072 stepsWindow cells -2076..283, 1 px = 2 cellsColors 0 1 1 only part of the time (or in part of the cells) of that pixel's block
Rows: (each averaged), 763 blocks to step 1e8 (Blaze image, not stretched) · Window: Blaze image, 1,180 columns · Colors: no head
Fig 5 · Left records, left edge pinned, 1e9viewer ↗

Left edge pinned. Each row is a new leftmost cell; the counter digits sit in the first columns.

Left records, left edge pinned, 1e9
bbchallenge-defaultStart blankRows left records onlyWindow cells 0..149, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Rows: the start, then one row per new leftmost cell (4,634 rows to step 1,000,000,000; not evenly spaced in time) · Window: counted from each row's leftmost visited cell (frame = left), so only the 150 leftmost cells are shown
Rules (10/10 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
R1 A-sweep (= BECv1 HR1)
l A> (011)n r
⟶ l (010)n A> r
—5n✓25/25
R2 marker step (= HR2)
l A> 011 00 011 r
⟶ l <B 00 011 011 r
——✓25/25
R3 B-sweep (= HR3)
l (010)n <B r
⟶ l <B (011)n r
—3n✓25/25
INC0
RS(W,0,n+1,m)
⟶ RS(W,1,n,m+1)
RS(W,b,n,m) = 0^inf W b <E 11 (011)^n 00 (011)^m 0^inf; W over blocks 1=100 0=000 f=010 s=0018n+16✓100/100
CARRY
RS(W,1,n+1,m)
⟶ RS(inc W,0,n,m+1)
inc = binary +1 from the right: f skip, 1->0, 0->1 stop, overflow prepends 18n+16+carry✓100/100
CARRY_S (carry meets debris)
RS(X s Y,1,n+1,m)
⟶ RS(inc(incC X) f Y0,0,n,m+1)
Y in {1,f}*, Y0 = Y with 1->0; incC = +1 with f=1, 0=0, s skipped (overflow prepends f); recursive when inc meets another s—✓200/200
BIRTH (marker reborn at the right end)
NM(W,0,n+1)
⟶ RS(W,1,n,1)
NM(W,b,n) = 0^inf W b <E 11 (011)^n 0^inf; BIRTHC: NM(W,1,n+1) -> RS(inc W,0,n,1) (validated, never fires from blank)8n+16✓200/200
EAT0f
RS(W' d f^k 1j,0,0,m)
⟶ RS(W',d,k-1,m+2+j)
k >= 1, d in {0,1}, j >= 0; marker stays at the counter—✓100/100
EAT0z
RS(W' 0 1j,0,0,m)
⟶ NM(phi W',0,m+2+j)
phi: 1->f, 0->0, f->s (each block shifted one cell right); W = 1^j uses W' empty—✓200/200
EAT1
RS(W,1,0,m)
⟶ NM(phi(inc W),0,m+1)
W in {1,0,f}*—✓100/100
Compressed historythe tape as 0∞ W 0 <E 11 (011)n 0∞ at 26 moments: where the rules are read off
0∞ W 0 <E 11 (011)n 0∞
stepn (unary blocks; the next epoch lasts about n rounds)|W| (blocks)#s (shifted debris blocks)W (1=100 0=000 f=010 s=001)
120510f
337631f f s
664931f s 0
1,1911052f s 0 s f
2,1181910f
6,3353000—
10,4753600—
22,9764151f 0 f s 0
52,9835483f f 0 f f s s s
100,9676883f 0 s 0 s f s 0
191,99879138f 0 f s s s s 0 0 s s s s
415,53411173f f s f 0 s s
880,3991381710f 0 0 0 f s 0 s f s s s s s s s s
1,884,030189104f f s 0 0 s f s f s
3,995,447248103f f f s f f s 0 s 0
8,577,8503132013f 0 0 f f f s s f s s s s s s s s s s s
18,895,844429158f f s 0 f 0 f s s s s f s s s
39,652,245560101f 0 0 0 f f 0 0 s 0
84,498,5757202012f 0 f f 0 s s f 0 s s s s 0 s s s s s s
178,862,95097350f f f f f
385,954,0481,225145f 0 0 f f s 0 0 s s s f f s
820,471,3301,5892921f f 0 0 f 0 0 s s s 0 s s s s s s s s s s s s s ...
1,738,588,7882,071188f 0 0 0 0 0 s f 0 0 0 s s s s s s s
3,720,429,4572,668188f 0 f 0 0 s f s s f f s f s s s 0 s
7,958,424,3393,5182010f f 0 s s s f f 0 f f s s s f s f s s s
9,996,109,6953,8042212f f f 0 f f 0 f f s s s f s s s s s s s s s
n (unary blocks; the next epoch lasts about n rounds)last 3,804
3,80451201e10log xstep 120: n (unary blocks; the next epoch lasts about n rounds) = 5step 337: n (unary blocks; the next epoch lasts about n rounds) = 6step 664: n (unary blocks; the next epoch lasts about n rounds) = 9step 1191: n (unary blocks; the next epoch lasts about n rounds) = 10step 2118: n (unary blocks; the next epoch lasts about n rounds) = 19step 6335: n (unary blocks; the next epoch lasts about n rounds) = 30step 10475: n (unary blocks; the next epoch lasts about n rounds) = 36step 22976: n (unary blocks; the next epoch lasts about n rounds) = 41step 52983: n (unary blocks; the next epoch lasts about n rounds) = 54step 100967: n (unary blocks; the next epoch lasts about n rounds) = 68step 191998: n (unary blocks; the next epoch lasts about n rounds) = 79step 415534: n (unary blocks; the next epoch lasts about n rounds) = 111step 880399: n (unary blocks; the next epoch lasts about n rounds) = 138step 1884030: n (unary blocks; the next epoch lasts about n rounds) = 189step 3995447: n (unary blocks; the next epoch lasts about n rounds) = 248step 8577850: n (unary blocks; the next epoch lasts about n rounds) = 313step 18895844: n (unary blocks; the next epoch lasts about n rounds) = 429step 39652245: n (unary blocks; the next epoch lasts about n rounds) = 560step 84498575: n (unary blocks; the next epoch lasts about n rounds) = 720step 178862950: n (unary blocks; the next epoch lasts about n rounds) = 973step 385954048: n (unary blocks; the next epoch lasts about n rounds) = 1225step 820471330: n (unary blocks; the next epoch lasts about n rounds) = 1589step 1738588788: n (unary blocks; the next epoch lasts about n rounds) = 2071step 3720429457: n (unary blocks; the next epoch lasts about n rounds) = 2668step 7958424339: n (unary blocks; the next epoch lasts about n rounds) = 3518step 9996109695: n (unary blocks; the next epoch lasts about n rounds) = 3804
|W| (blocks)last 22
2901201e10log xstep 120: |W| (blocks) = 1step 337: |W| (blocks) = 3step 664: |W| (blocks) = 3step 1191: |W| (blocks) = 5step 2118: |W| (blocks) = 1step 6335: |W| (blocks) = 0step 10475: |W| (blocks) = 0step 22976: |W| (blocks) = 5step 52983: |W| (blocks) = 8step 100967: |W| (blocks) = 8step 191998: |W| (blocks) = 13step 415534: |W| (blocks) = 7step 880399: |W| (blocks) = 17step 1884030: |W| (blocks) = 10step 3995447: |W| (blocks) = 10step 8577850: |W| (blocks) = 20step 18895844: |W| (blocks) = 15step 39652245: |W| (blocks) = 10step 84498575: |W| (blocks) = 20step 178862950: |W| (blocks) = 5step 385954048: |W| (blocks) = 14step 820471330: |W| (blocks) = 29step 1738588788: |W| (blocks) = 18step 3720429457: |W| (blocks) = 18step 7958424339: |W| (blocks) = 20step 9996109695: |W| (blocks) = 22
#s (shifted debris blocks)last 12
2101201e10log xstep 120: #s (shifted debris blocks) = 0step 337: #s (shifted debris blocks) = 1step 664: #s (shifted debris blocks) = 1step 1191: #s (shifted debris blocks) = 2step 2118: #s (shifted debris blocks) = 0step 6335: #s (shifted debris blocks) = 0step 10475: #s (shifted debris blocks) = 0step 22976: #s (shifted debris blocks) = 1step 52983: #s (shifted debris blocks) = 3step 100967: #s (shifted debris blocks) = 3step 191998: #s (shifted debris blocks) = 8step 415534: #s (shifted debris blocks) = 3step 880399: #s (shifted debris blocks) = 10step 1884030: #s (shifted debris blocks) = 4step 3995447: #s (shifted debris blocks) = 3step 8577850: #s (shifted debris blocks) = 13step 18895844: #s (shifted debris blocks) = 8step 39652245: #s (shifted debris blocks) = 1step 84498575: #s (shifted debris blocks) = 12step 178862950: #s (shifted debris blocks) = 0step 385954048: #s (shifted debris blocks) = 5step 820471330: #s (shifted debris blocks) = 21step 1738588788: #s (shifted debris blocks) = 8step 3720429457: #s (shifted debris blocks) = 8step 7958424339: #s (shifted debris blocks) = 10step 9996109695: #s (shifted debris blocks) = 12
W (1=100 0=000 f=010 s=001)last f f f 0 f f 0 f f s s s f s s s s s s s s s
not plottable
Template comparisonBECv1_6x2_solved.v tm10: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB0RA
B1LC0LD
C1LE1LD
D0LB0RE
E1RF1LBtpl 1LE
F---0RA

differs from the template

file
BECv1_6x2_solved.v:88 (+ BECv1.v Section; structure: BECv7.v)
module
tm10 / nonhalt10, cert Build_BEC_cert_v1 B A E A [0] [1] [1] [0] [1] ... 1 0 0
machine
1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LE_---0RA (1 transition apart)
diff
E1: 1LB (ours) vs 1LE (tm10); the other 11 transitions are equal (#7 has E1 = 0LA)
note
Our TM on tm10's cert: 10/11 hypotheses hold (HL1, HL3-5, HR1-3, HE0-3: 25/25 each); HL2, the 1-cell carry 1<E1 -> <E11, fails 0/25 (E1 = 1LB sends the carry through B and C, so digits are 3 cells apart). The unary half carries over; LeftBinaryCounter becomes a block-list counter with fillers and a phase-shifted debris region, closest to BECv7.v's inductive RIncs carry relation over 110/000/100 blocks.
Proof strategy & riskshow the formal proof will go · 3 risks to watch

Proof on round starts RS/NM, with W over {1,0,f,s}. Invariant: no 1 left of an s, and no s at an eat (the flush lemma). Unary lemmas from BECv1; inc/incC/CARRY_S as an inductive carry relation in BECv7 style. Then progress_nonhalt_cond. The open piece is the flush lemma: before the marker returns, the counter carries through every s block.

  • ▲The flush lemma is a size bound (2^(digits right of the leftmost s) < epoch length, about m+1); it holds with slack on the blank run (worst ratio 0.44, below 0.11 after 1e9) but is not proved.
  • ▲An eat with s still present leaves the block alphabet; random words that do this can halt (26 of 1,200 fuzz samples), so the invariant must carry the bound.
  • ▲CARRY_S is recursive (debris inside debris), so the Coq carry relation must be mutually inductive, like BECv7's RIncs.
Stats & provenance1010 steps simulated · 11,492 cells · the status in full · files
simulated
1010 steps
tape
11,492 cells · 5,201 nonzeros
growth
span ~t^0.34 (5,197 cells at 1e9, 11,492 at 1e10); epoch length n ~t^0.35 (1,589 at 8.2e8, 3,804 at 1e10)
status now
Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Park with #10 as one cryptid candidate. Funded stage prove_l9 (Dennis 2026-10-11, 'go with recommendations') ended at its stop rule: L9 did not close, and it cannot close by a local invariant. Proved: after the flush the normalized debris weight s = sigma/2^D never grows (W1); sigma after the flush = g(PC) + h (W2); s < 1 passes from S1 to S1 in every case except the hard case H (exact carry PC = 2^D + sparse Y with N < 2^(D+1)) (W3-W5); so L9 reduces to Lemma H. Checks: 100,000 random states, 0 violations. Found: #28 is #10 (CRYPTID_CANDIDATE) mirrored with A..F -> E,A,B,F,C,D, started in #10's E (12/12 entries, 3e6 steps lock-step), and the orbits merge at our epoch 350,328 = #10's t = 350,272. #10's counter-family sigma0(B), translated, satisfies INV (L9 included) and then breaks L9 and the flush (an eat sees an s block) for every B = 8..18; on #28's own TM at B = 8: 779/779 rounds match, unsafe eat at N = 194, then recovery. Safety therefore rests on exact coincidences along one orbit (ground rule 6), as for #10. proof.md is the conditional write-up with L9 open. decision.json: park with #10 (recommended) vs shared Rocq rule reduction vs research. (status.json, 2026-10-12)
observer's note
Mechanism found: 9 round rules (1,000/1,000 random-instance sims) predict all 1,008,130 rounds to 1e10, 0 mismatches. Not cryptid. Non-halting needs the unproved flush lemma, so confidence is med.
files
observe.json · notes.md · proof.md · status.json

Proof & checks

Files

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

namesizechanged
notes.md ↓30 KB2026-10-12 08:59
proof.md ↓17 KB2026-10-11 08:58
status.json ↓2.0 KB2026-10-12 08:59
observe.json ↓13 KB2026-10-10 13:25
deepen.json ↓8.3 KB2026-10-11 08:57
decision.json ↓3.1 KB2026-10-12 08:59
data/10 items2026-10-11 08:57
decisions/3 items2026-10-11 08:58
img/6 items2026-10-10 13:21
scripts/42 items2026-10-11 08:54
status.json in full
{
 "tm": "1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_---0RA",
 "status": "CRYPTID_CANDIDATE",
 "stage": "prove_l9 (L9 open; flagged cryptid with #10)",
 "confidence": "med",
 "updated": "2026-10-12",
 "cryptid_flag": true,
 "twin": "1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC",
 "reason": "Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Park with #10 as one cryptid candidate. Funded stage prove_l9 (Dennis 2026-10-11, 'go with recommendations') ended at its stop rule: L9 did not close, and it cannot close by a local invariant. Proved: after the flush the normalized debris weight s = sigma/2^D never grows (W1); sigma after the flush = g(PC) + h (W2); s < 1 passes from S1 to S1 in every case except the hard case H (exact carry PC = 2^D + sparse Y with N < 2^(D+1)) (W3-W5); so L9 reduces to Lemma H. Checks: 100,000 random states, 0 violations. Found: #28 is #10 (CRYPTID_CANDIDATE) mirrored with A..F -> E,A,B,F,C,D, started in #10's E (12/12 entries, 3e6 steps lock-step), and the orbits merge at our epoch 350,328 = #10's t = 350,272. #10's counter-family sigma0(B), translated, satisfies INV (L9 included) and then breaks L9 and the flush (an eat sees an s block) for every B = 8..18; on #28's own TM at B = 8: 779/779 rounds match, unsafe eat at N = 194, then recovery. Safety therefore rests on exact coincidences along one orbit (ground rule 6), as for #10. proof.md is the conditional write-up with L9 open. decision.json: park with #10 (recommended) vs shared Rocq rule reduction vs research.",
 "funded": {
  "option": "prove_l9",
  "date": "2026-10-11"
 },
 "next": "Cryptid protocol: AntiHydra-style Rocq rule reduction of the rule layer, shared with #10 and its twin, at low priority (decision.json).",
 "priority_call_answered": "Park #28 with #10 as one cryptid candidate, fund the shared Rocq rule reduction, or fund research on the shared Lemma X?",
 "parked": "Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Park with #10 as one cryptid candidate."
}