BB(6) hunt
Machines / #37

1RB0LF_1RC1RB_0RD0RC_1LE1LF_1LD---_0LB1LA

#37ParkedSync bouncer counterbbchallenge ↗Explorer

Where it stands

Parked at the deeper analysis

Twin port refuted (different halting event). 500 follows TM2's macro run exactly: 220/220 recorded counter words equal to the follow-stage simulator, to phase 370, and TM2's b = n-1 per phase.

Read the full status

TM2 exits 16 macro steps after its 374th overflow (early in 500's phase 375) and halts at step 13,297 when B reads 1. On the same configuration, with a and b kept symbolic, 500 makes the A0 turn, runs 72,652 steps without halting and re-enters TM2's own cfgL' a b r'' (next rule LIncs). TM2's left lemmas (LInc, LRst_101, LRst_11) hold for 500 iff a is odd, and a = 3 mod 4 throughout the orbit, so 500 can only halt on the counter side. It was already followed to phase 1,857 with no halt. Machine stays parked.

Observe
Deepen
Informal proof
Rocq
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

Left binary counter +1 per visit; right 1-block loses 2 cells/visit, pad gains 4; reset doubles it. Digit grammar open

Status
Parkedtwin port refuted · updated 2026-10-14Not blocking · Stuck at the twin port refuted stage. Answer Q1–Q3 whenever; a “no” redirects the work.
idle since Oct 14 16:54 (44 h ago) · status.json 2026-10-14
Class
Sync bouncer counterours: Sync bouncer counter (sheet) · ours adds: binary counter on the left, eroding 1-block timer on the right, doubling reset · med confidence
On the list
line 453 of BB6_holdouts_663.txt · historical 740 line 500
#37eqv ×1sim 1e15UBRRBA
Your calls on file 7
parked
Parked 2026-10-11 (Dennis: go with recommendations): Park #37 behind the other machines.
funded
option: follow · date: 2026-10-10 · auto: true
next
No port. #37 stays parked (Dennis 2026-10-11). Asset: TM2's representation (cfgL'/cfgR', rest/RIncs, LInc/LIncs/LOv/LRst) is an exact accelerator for #37 under 'a odd'; a nonhalt proof still needs the counter-side invariant (lemma B'/rule M of the follow stage).
2026-10-10 · deepen
#37's visit, reset and halt rules are exact. What is open is the counter-word grammar K (its closure under inc and reset) and the reason every reset lands on bit 0 = 0. Spend one deepen stage pinning K, or park #37? (Dennis: go with all recommendations (2026-10-10))
2026-10-10 · deepen2
#37's sync now rests on one open lemma B (its bottom counter run never again becomes an erasable 11 digit): fund a second deepen round on B, or park #37? (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-10 · follow
#37's sync now hinges on whether a short run ever reaches the bottom during an excursion: port the jump simulator to C and follow the real orbit through the next excursions, or park #37? (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.)
decision.json · answered 2026-10-11: park
#37 stays in sync to phase 1,857, and its next excursion (phase 3,321) is predicted benign: park it, spend one round deriving the merge-wave rule, or first confirm phase 3,321 on the real orbit? Decisions →

Mechanism

How it works: 3 notes
  • Each visit (right record in C) maps 0^inf L 1^n 0^g C> 0^inf to 0^inf inc(L) 1^(n-2) 0^(g+4) C> 0^inf: the head stripes the block going left, adds 1 to the counter L, zigzags back and erases the block's last 2 cells (early in a phase, filler cells of L can merge into the block).
  • inc is a binary +1: the carry depth follows the ruler sequence (27,084/27,124 visits). Digits are 1 or 2 cells, separated by 00 gaps or 1-runs the carry passes; the layout is rebuilt at each reset and migrates early in a phase (the open part).
  • Reset at n=2: L0 0 1^2 0^g C> -> L0 1^(g+6) C> with g = 4(visits-1), so the block about doubles. All 12 resets to 2.5e9 hit a bit-0 = 0 visit; 35/36 off-sync variants leave an odd pad and halt next visit. Not a cryptid: plain +1, linear timer.

Figures for Checkpoint A

Fig 1 · Left/right records to 9.4 million stepsQ1

One row per new edge cell. Follow each white triangle down to the full-width white row that ends it.

Left/right records to 9.4 million steps
bbchallenge-defaultStart blankRows left/right recordsWindow cells -73..3324, 1 px = 1 cellColors 1 0 or never visited head just moved right/left
Rows: the start, then one row per new leftmost or rightmost cell (3,398 rows, steps 0..9,400,000; rows are not equal time)
Fig 2 · The left counter, one row per visitQ2

Each row is the tape at a visit start. Read right to left from the white block; compare flip rates.

The left counter, one row per visit
customStart mid-run: step 38,014,318Rows one row per visit startWindow cells -104..-36, 1 px = 0.167 cellsColors 1 0
Start: visit 3,346; phase 10, block n = 6,702 · Rows: (right record in state C): visits 3,346..3,473, steps 38,014,318..43,105,312; each row is 4 px tall · Window: each cell is 6 px wide · Colors: no head drawn (the head is at the far right, off the window, in every row)
Fig 3 · One carry, every step

Every step of one visit's counter part. Top: sweep left; middle: turn at the carry; bottom: zigzag back.

One carry, every step
bbchallenge-defaultStart mid-run: step 10,090,380Rows every step (281 rows: steps 10,090,380..10,090,660)Window cells -72..-4, 1 px = 0.33 cellsColors 1 0 or never visited head just moved right/left
Start: head at cell -8 in state A sweeping left; this visit carries through 4 digits · Rows: each row is 3 px tall · Window: each cell is 3x3 px
More figures (2)Fig 4–5: bbchallenge default view, 10,000 steps · Lowest 48 runs per phase, real orbit
Fig 4 · bbchallenge default view, 10,000 stepsviewer ↗

The site's own view: the first four phases as growing bands.

bbchallenge default view, 10,000 steps
bbchallenge-defaultStart blankRows every step 0..10,000Window cells -200..199, 1 px = 1 cellColors 1 0 or never visited head just moved right/left
Rows: squeezed to 500 rows by the site's bilinear filter (20 steps per row)
Fig 5 · Lowest 48 runs per phase, real orbit

Columns are runs above the block. Vertical stripes are frozen runs; diagonal bands are the waves after excursions.

Lowest 48 runs per phase, real orbit
customStart mid-run: step 603,050,744Rows one row per phase startWindow runs a0..a47 counted up from the blockColors run length on a log scale 5 cells 4,096 cells or more run of 1 to 4 cells no run
Start: start of phase 12; rows from the C jump simulator, phases 12..1857 · Rows: every 3rd phase plus every phase whose bottom run is 2 (617 rows); each row is 1 px tall · Window: (a0 = bottom run), 1 run = 8 px; not a cell window: run lengths range from 2 to over 5,000 cells · Colors: dark; blue: word shorter than 48 runs
Rules (9/10 validated)1 failing · exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
V visit
0∞ L 1m 0g C> 0∞
⟶ 0∞ inc(L) 1m+d 0g+4 C> 0∞
m >= 4; g even; (inc(L), d) depend on L only (d = -2 except when bit 0 flips or filler merges); tested on every visit to 2.5e9 with random m' (same parity) and g' (both residues mod 4)6m+2g+c(L)✓54248/54248
Inc binary +1
carry depth of visit k in a phase
⟶ v2(k+c)+1 digits flipped
one offset c per phase; 40 misses are early-phase digit migrations (a filler zero joins a digit)—✗27084/27124
R0 bit-0 visit
0∞ L0 0 1n 0g C> 0∞
⟶ 0∞ L0 1n-1 0g+4 C> 0∞
n even >= 4, g even, any word L06n+2g-10✓600/600
R1s bit-1 carry (1 cell)
0∞ L0 1 0 00 1 1n 0g C> 0∞
⟶ 0∞ L0 1 1 00 0 1n-2 0g+4 C> 0∞
n even >= 4, g even, any L0 (phase-10 layout)6n+2g+10✓600/600
R1d bit-1 carry (2 cells)
0∞ L0 1 0 00 00 00 1 1n 0g C> 0∞
⟶ 0∞ L0 1 0 00 11 00 0 1n-2 0g+4 C> 0∞
n even >= 4, g even, any L0 (phase-9 layout)6n+2g+14✓600/600
R reset
0∞ L0 0 12 0g C> 0∞
⟶ 0∞ L0 1g+6 C> 0∞
g = 0 mod 4 (always: g = 4(visits-1)); any L0; all 12 real resets plus random g—✓636/636
P pad fill
0∞ X 1n 0g C> 0∞
⟶ 0∞ X 1n-1 <F 1g+3 0∞
g even, n >= 1g+4✓400/400
H odd pad
0∞ X 1n 0g C> 0∞
⟶ halt
g odd: E reads the last block cellg+4✓5825/5825
S stripe
L 12k+1 <F R
⟶ L <A 1 (01)k R
k >= 02k+1✓400/400
Z zigzag
1a C> (01)k 1b 0∞
⟶ 1a+2k-1 C> 1b+1 0∞
a, k, b >= 110k-5✓400/400
Compressed historythe tape as 0∞ L 1m 0g C> 0∞ at 36 moments: where the rules are read off
0∞ L 1m 0g C> 0∞
stepphasemgvisitspan
1316027
1122140519
47221016932
83622321344
91133801447
3,589325442578
6,027328836108
6,214494037111
19,2824509661160
30,1904219285216
30,5855198086219
90,2775105208138332
138,56752412189438
139,40264180190441
379,6346210416294650
576,70662832398866
578,38178380399869
1,543,46374218366081,287
2,333,933721,6728171,706
2,337,28881,67808181,709
6,208,30288411,6761,2372,548
9,377,196823,3521,6563,394
9,383,91193,35801,6573,397
24,898,37791,6813,3562,4965,088
37,597,555926,7123,3356,770
37,610,990106,71803,3366,773
99,808,022103,3626,7205,01610,154
150,715,86610213,4406,69613,518
150,742,7571113,44606,69713,521
399,462,331116,72513,44410,05820,243
602,996,95711226,88813,41926,970
603,050,7441226,894013,42026,973
1,597,795,6141213,44926,89220,14340,428
2,411,745,73212253,78426,86653,878
2,411,853,3111353,790026,86753,881
9,646,815,51814107,5820-107,697
phaselast 14
141139.6e9log xstep 13: phase = 1step 112: phase = 2step 472: phase = 2step 836: phase = 2step 911: phase = 3step 3589: phase = 3step 6027: phase = 3step 6214: phase = 4step 19282: phase = 4step 30190: phase = 4step 30585: phase = 5step 90277: phase = 5step 138567: phase = 5step 139402: phase = 6step 379634: phase = 6step 576706: phase = 6step 578381: phase = 7step 1543463: phase = 7step 2333933: phase = 7step 2337288: phase = 8step 6208302: phase = 8step 9377196: phase = 8step 9383911: phase = 9step 24898377: phase = 9step 37597555: phase = 9step 37610990: phase = 10step 99808022: phase = 10step 150715866: phase = 10step 150742757: phase = 11step 399462331: phase = 11step 602996957: phase = 11step 603050744: phase = 12step 1597795614: phase = 12step 2411745732: phase = 12step 2411853311: phase = 13step 9646815518: phase = 14
mlast 107,582
1.1e52139.6e9log xstep 13: m = 6step 112: m = 14step 472: m = 10step 836: m = 2step 911: m = 38step 3589: m = 25step 6027: m = 2step 6214: m = 94step 19282: m = 50step 30190: m = 2step 30585: m = 198step 90277: m = 105step 138567: m = 2step 139402: m = 418step 379634: m = 210step 576706: m = 2step 578381: m = 838step 1543463: m = 421step 2333933: m = 2step 2337288: m = 1678step 6208302: m = 841step 9377196: m = 2step 9383911: m = 3358step 24898377: m = 1681step 37597555: m = 2step 37610990: m = 6718step 99808022: m = 3362step 150715866: m = 2step 150742757: m = 13446step 399462331: m = 6725step 602996957: m = 2step 603050744: m = 26894step 1597795614: m = 13449step 2411745732: m = 2step 2411853311: m = 53790step 9646815518: m = 107582
glast 0
53,7840139.6e9log xstep 13: g = 0step 112: g = 0step 472: g = 16step 836: g = 32step 911: g = 0step 3589: g = 44step 6027: g = 88step 6214: g = 0step 19282: g = 96step 30190: g = 192step 30585: g = 0step 90277: g = 208step 138567: g = 412step 139402: g = 0step 379634: g = 416step 576706: g = 832step 578381: g = 0step 1543463: g = 836step 2333933: g = 1672step 2337288: g = 0step 6208302: g = 1676step 9377196: g = 3352step 9383911: g = 0step 24898377: g = 3356step 37597555: g = 6712step 37610990: g = 0step 99808022: g = 6720step 150715866: g = 13440step 150742757: g = 0step 399462331: g = 13444step 602996957: g = 26888step 603050744: g = 0step 1597795614: g = 26892step 2411745732: g = 53784step 2411853311: g = 0step 9646815518: g = 0
visitlast -
26,8672132.4e9log xstep 13: visit = 2step 112: visit = 5step 472: visit = 9step 836: visit = 13step 911: visit = 14step 3589: visit = 25step 6027: visit = 36step 6214: visit = 37step 19282: visit = 61step 30190: visit = 85step 30585: visit = 86step 90277: visit = 138step 138567: visit = 189step 139402: visit = 190step 379634: visit = 294step 576706: visit = 398step 578381: visit = 399step 1543463: visit = 608step 2333933: visit = 817step 2337288: visit = 818step 6208302: visit = 1237step 9377196: visit = 1656step 9383911: visit = 1657step 24898377: visit = 2496step 37597555: visit = 3335step 37610990: visit = 3336step 99808022: visit = 5016step 150715866: visit = 6696step 150742757: visit = 6697step 399462331: visit = 10058step 602996957: visit = 13419step 603050744: visit = 13420step 1597795614: visit = 20143step 2411745732: visit = 26866step 2411853311: visit = 26867
spanlast 107,697
1.1e57139.6e9log xstep 13: span = 7step 112: span = 19step 472: span = 32step 836: span = 44step 911: span = 47step 3589: span = 78step 6027: span = 108step 6214: span = 111step 19282: span = 160step 30190: span = 216step 30585: span = 219step 90277: span = 332step 138567: span = 438step 139402: span = 441step 379634: span = 650step 576706: span = 866step 578381: span = 869step 1543463: span = 1287step 2333933: span = 1706step 2337288: span = 1709step 6208302: span = 2548step 9377196: span = 3394step 9383911: span = 3397step 24898377: span = 5088step 37597555: span = 6770step 37610990: span = 6773step 99808022: span = 10154step 150715866: span = 13518step 150742757: span = 13521step 399462331: span = 20243step 602996957: span = 26970step 603050744: span = 26973step 1597795614: span = 40428step 2411745732: span = 53878step 2411853311: span = 53881step 9646815518: span = 107697
Template comparisonSBCv7.v TM4: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB0LF
B1RC1RB
C0RD0RC
D1LE1LF
E1LD---
F0LB1LA
file
SBCv7.v:610
module
TM4 (line 610); also SBCv11.v GenericNonhalt
machine
1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_0RA--- (11 transitions apart)
diff
11 of 12 transitions differ: a class-level match, not a delta
note
Same macro shape (left binary counter, right side reset in sync, progress_nonhalt_cond). TM4's fixed digit words d0/d1 and BC.Mul2 do not fit: here digits are 1 or 2 cells with phase-dependent fillers. No solved machine within 3 transitions (nearest: CTLv1, RWL_mod, CPS_LRU deciders at 4).
Proof strategy & riskshow the formal proof will go · 3 risks to watch

Visit-level proof: invariant = L in a counter language K (with bit-0 alignment to the block), g = 0 mod 4. Prove V for L in K from S, P, Z and per-digit carry lemmas; R for the reset (plus the absorption visits); then progress_nonhalt_cond. Open: write down K (digit/filler grammar) and prove it closed under inc and the reset, including the sync.

  • ▲The counter's digits (1 or 2 cells) and fillers change layout at each reset and migrate early in a phase; the grammar K is not pinned, and its closure is the proof.
  • ▲Sync: all 12 resets landed on a bit-0 = 0 visit, but visits per phase are not always odd (phase 5: 104, after 10 absorbed cells). 35/36 off-sync resets halt on the next visit (tested), so the sync must come out of the grammar.
  • ▲No close template (SBCv7/SBCv11 are class-level only): expect a long custom .v, kill #4-sized or larger.
Stats & provenance1.2·1010 steps simulated · 115,087 cells · the status in full · files
simulated
1.2·1010 steps
tape
115,087 cells · 114,968 nonzeros
growth
span ~ t^0.5: the block about doubles each phase and a phase costs ~2.5 n^2 steps (~4x the last); left edge -175 at 1.2e10
status now
Twin port refuted (different halting event). 500 follows TM2's macro run exactly: 220/220 recorded counter words equal to the follow-stage simulator, to phase 370, and TM2's b = n-1 per phase. TM2 exits 16 macro steps after its 374th overflow (early in 500's phase 375) and halts at step 13,297 when B reads 1. On the same configuration, with a and b kept symbolic, 500 makes the A0 turn, runs 72,652 steps without halting and re-enters TM2's own cfgL' a b r'' (next rule LIncs). TM2's left lemmas (LInc, LRst_101, LRst_11) hold for 500 iff a is odd, and a = 3 mod 4 throughout the orbit, so 500 can only halt on the counter side. It was already followed to phase 1,857 with no halt. Machine stays parked. (status.json, 2026-10-14)
observer's note
Mechanism found (binary counter + eroding block + doubling reset); 10 rules validated (V on every visit to 2.5e9, 54,248/54,248; reset 636/636); confidence med because the counter's digit grammar and its closure under resets are open.
files
observe.json · notes.md · status.json

Proof & checks

No proof work yet.

Files

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

namesizechanged
notes.md ↓31 KB2026-10-14 16:54
status.json ↓3.3 KB2026-10-14 16:54
observe.json ↓14 KB2026-10-10 15:11
deepen.json ↓12 KB2026-10-10 15:13
decision.json ↓3.1 KB2026-10-11 08:19
decisions/3 items2026-10-10 15:14
img/6 items2026-10-10 15:11
scripts/24 items2026-10-14 16:29
work/21 items2026-10-14 16:29
status.json in full
{
 "tm": "1RB0LF_1RC1RB_0RD0RC_1LE1LF_1LD---_0LB1LA",
 "label": "P-500",
 "status": "STUCK",
 "stage": "twin_port_refuted",
 "updated": "2026-10-14",
 "holdout_line_740": 500,
 "parent": "SBCv9.v Module TM2 (1RB0RF_0LC---_1LD1LC_0LE0LD_1RE1RF_0RC1RA), HALT",
 "relation": "mirror(500) with states A,B,C,D,E,F -> TM2's A,C,D,E,G,F equals TM2 except A0 (TM2: A0 1RB, B0 0LC, C1 1LC = 3 steps, halts if B reads 1; 500: 1 step) and the E self-loop (500 alternates D/E over 0s and halts at E1 after an odd number of 0s); same start, same tape at all times",
 "reason": "Twin port refuted (different halting event). 500 follows TM2's macro run exactly: 220/220 recorded counter words equal to the follow-stage simulator, to phase 370, and TM2's b = n-1 per phase. TM2 exits 16 macro steps after its 374th overflow (early in 500's phase 375) and halts at step 13,297 when B reads 1. On the same configuration, with a and b kept symbolic, 500 makes the A0 turn, runs 72,652 steps without halting and re-enters TM2's own cfgL' a b r'' (next rule LIncs). TM2's left lemmas (LInc, LRst_101, LRst_11) hold for 500 iff a is odd, and a = 3 mod 4 throughout the orbit, so 500 can only halt on the counter side. It was already followed to phase 1,857 with no halt. Machine stays parked.",
 "checks": {
  "check_twin": "scripts/port/check_twin.py (T1-T6, ~6 min; work/port/check_twin.log)",
  "layouts": "work/port/cmp_tm2_vs_500_layouts.log (202/202 with b = n-1; check_twin T4: 220/220 words)",
  "exit_window": "work/port/exit_window.log"
 },
 "confidence": "high",
 "funded": {
  "option": "follow",
  "date": "2026-10-10",
  "auto": true
 },
 "parked": "Parked 2026-10-11 (Dennis: go with recommendations): Park #37 behind the other machines.",
 "prior_reason": "Parked 2026-10-11 (Dennis: go with recommendations): Park #37 behind the other machines. Follow (funded 2026-10-10, auto-applied recommendation) done; new priority call in decision.json (recommended: park). A C port of the jump simulator (exact: 160/160 phases equal to Python, random instances 90/90 vs Python and 90/90 vs exact fastphase) followed the real orbit to the start of phase 1,857 (n ~ 2^1860): no off-sync, no halt. Excursions at phases 91, 119, 215, 487 were all benign, with 14, 77, 93 and 700 cells in the run that became the bottom; the 3-run that sat 16 runs up at phase 171 was absorbed by a merge wave at phases 231-233. Between excursions the bottom run loses 1 cell per phase (1,777/1,779 steady phase pairs) and the runs below the wave front are frozen; after each excursion a merge wave climbs at ~0.5 runs per phase. A fast-forward check (bottom run cut short) reproduces the real excursion at phase 487 and its cascade exactly (45/45 phases) and predicts the next excursions at phases 3,321, 4,866 and 5,172 as benign. Candidate maturation rule M (the new bottom and the new a1 are merge products after every cascade, so a1 >= 6 at each excursion) holds in 4 real + 3 predicted cascades but is not derived; a proof would need a wave grammar on unbounded run words, with no busycoq template near. Not a cryptid as tested.",
 "next": "No port. #37 stays parked (Dennis 2026-10-11). Asset: TM2's representation (cfgL'/cfgR', rest/RIncs, LInc/LIncs/LOv/LRst) is an exact accelerator for #37 under 'a odd'; a nonhalt proof still needs the counter-side invariant (lemma B'/rule M of the follow stage)."
}
observe.json contract (tools/README-card.md):
1 contract warning
  • diagrams[4].window: not "cells A..B, 1 px = k cells"