BB(6) hunt
Machines / R8

1RB0RA_1RC1RF_1LD0LC_1RA1LE_1RA0LC_---0RD

R8ParkedUnknownbbchallenge ↗Explorer

Where it stands

Parked at the informal proof

Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Park. Funded f3_first stage done (2026-10-11): F3 has no closed family.

Read the full status

The big region after the marker is a fourth zone shaped like M (ternary word, AC/DC interface, exact rules 40,766/40,766 visits), and its gliders build new throttle levels with K = 3 at the right end (GX/NB 33/33), so from m ~ 236 the run is an unbounded tower of levels. B^j A^n with j up to ~1e6 never halted (300 + 54 runs), and glider bursts B^5/B^4 are safe, but zone T halts on small bursts with short gaps (B^1 15/200, B^3 2/200) and on A-on-junk words. Deeper levels can receive B^3 bursts and arbitrary gaps. Excluding the unsafe patterns needs control of pseudo-random burst timing (heuristically ~2^-m per epoch), which is cryptid-like for a proof. Non-halting is heuristically very likely, but proof confidence is low. Recommendation: park; a decision is queued.

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

TM31 cousin: binary counter left, ternary throttle right; the overflow pause and a one-off creep are unruled

Status
Parkedf3 first · updated 2026-10-12Not blocking · Stuck at the f3 first stage. Answer Q1–Q3 whenever; a “no” redirects the work.
idle since Oct 12 08:59 · status.json 2026-10-12
Informal proof
proof.mdconditional; see Proof for what is still open
Class
Unknownours: sheet Unknown ≠ ours Sync bouncer counter (SBCv8 TM31 cousin): binary counter left, ternary throttle right, nested overflow pause · low confidence
On the list
line 482 of BB6_holdouts_663.txt · historical 740 line 534
R8eqv ×1table ×3sim 1e15
Your calls on file 7
parked
Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Park.
funded
option: f3_first · date: 2026-10-11
2026-10-10 · deepen
Spend one deepen stage, with a stop rule, decoding the overflow pause and the creep, or park R8? (Dennis: go with all recommendations (2026-10-10))
2026-10-10 · exact_rules
Spend one more stage deriving exact block rules for the sweep, the glider absorption and the MS overflow before proof.md, start proof.md now, 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 · f3_first
Spend the next stage on F3 (the unbounded overflow bursts into the throttle), on F1 and F2 (the pause counter and the absorption tail), or park? (Dennis: go with recommendations (2026-10-11))
2026-10-10 · proof_now
Write proof.md now with the absorption tail, the MS overflow and the pause counter as flagged lemmas, spend one more stage making them exact, 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.)
decision.json · answered 2026-10-12: park
Park R8, spend one research stage on the tower (the safe input language of a level plus a burst-timing lemma), or flag it as a cryptid candidate? Decisions →

Mechanism

How it works: 3 notes
  • The head shuttles between a left binary counter (6-cell digits) and a right ternary throttle, across 150 transparent middle blocks (0011 <-> 1110 per pass).
  • Each trip adds 1 on the left. On the right, s3 forwards 2 of 3 trips into K ternary digits; their carry-out appends one block, so a record comes every (3/2)*3^K trips.
  • A full left counter (3*2^m trips) starts an ~80*2^m-step pause. Only at m=14 did it end in a 150-trip creep that cost K a digit (3 -> 2). No halt to 2e11; hand tests with K=1,0,-1 keep running.

Figures for Checkpoint A

Fig 1 · Records view to step 22.8 millionQ3

One row per new left or right record. Compare the steady right diagonal with the rare full-width rows (left records).

Records view to step 22.8 million
bbchallenge-defaultStart blankRows left/right recordsWindow cells -69..2330, 1 px = 2 cellsColors 1 0 or unvisited head moving R/L
Rows: one row per new leftmost or rightmost cell, 2,400 rows (row limit), up to step 22,765,042 · Window: every 2nd column sampled
Fig 2 · Ordinary overflow pause at step 3.62 millionQ2

Rows 60..860 are the pause. Compare the left strip (cells -60..50) with the unchanging columns to its right.

Ordinary overflow pause at step 3.62 million
bbchallenge-defaultStart mid-run: step 3,620,000Rows every 50 stepsWindow cells -80..119, 1 px = 1 cellColors 1 0 or unvisited head moving R/L
Start: pause runs from step 3,622,995 to 3,664,343 · Rows: steps 3,620,000..3,668,000 (961 rows) · Window: absolute positions; cell 0 = the start cell
Fig 3 · The m=14 overflow: creep across the middleQ1

Rows 0..70 end the pause. Follow the thin diagonal from cell 30 to about 620, then the right-counter columns.

The m=14 overflow: creep across the middle
bbchallenge-defaultStart mid-run: step 148,740,000Rows every 250 stepsWindow cells -100..699, 1 px = 1 cellColors 1 0 or unvisited head moving R/L
Rows: steps 148,740,000..148,890,000 (601 rows) · Window: absolute positions
More figures (2)Fig 4–5: bbchallenge Default, first 10,000 steps · Right throttle close-up at step 3e8
Fig 4 · bbchallenge Default, first 10,000 stepsviewer ↗

The site's own view. Look at the right edge moving out while the left edge stays nearly put.

bbchallenge Default, first 10,000 steps
bbchallenge-defaultStart blankRows steps 0..10,000 squeezed into 500 rows by the site's bilinear filterWindow cells -200..199, 1 px = 1 cellColors 1 0 or unvisited head moving R/L
Rows: about 20 steps per row · Window: site canvas, cell 0 at column 200
Fig 5 · Right throttle close-up at step 3e8

Cells 619..634 hold s3, t0, t1 and the 1011 marker. Watch the 4-cell digits change at head visits.

Right throttle close-up at step 3e8
bbchallenge-defaultStart mid-run: step 300,032,419Rows every 10 stepsWindow cells 590..669, 1 px = 1 cellColors 1 0 or unvisited head moving R/L
Start: head at cell 301 moving right; canonical point, K = 2 · Rows: steps 300,032,419..300,061,839 (2,943 rows; stopped by the stored-cell cap) · Window: absolute positions
Rules (4/5 validated)1 failing · exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
RL left binary counter
canonical point (head steps 300 -> 301), V = (D_15..D_1 D_0)_2 with D_i at cell -86+6(15-i), D_0 at 16..21; 0 = 001101, 1 = 101101
⟶ next canonical point with V+1
V < 2^16 - 1 (no overflow); the overflow case is rule OVone round trip (about 1,250 steps + 8e on a record trip)✓600/600
RS first right digit s3 (cells 619..622)
s3 = P (1001) | Q (1011) | R (1000)
⟶ P -> Q, no carry | Q -> R, carry | R -> P, carry
3 cases; forwards 2 of every 3 trips—✓600/600
RT ternary throttle + record
digits t_0..t_(K-1) at 623+4j (P=0, R=1, Q=2), marker 1011, (0011)e, carry c from RS
⟶ T + c; if T + c = 3K: digits -> 0, the trip runs to the right end, right edge +4 (e -> e+1); else right edge unchanged
K = 0..5 tested; carry-out vs not—✓600/600
RM middle is transparent
cells 22..618 at a canonical point ((0011)150, toggled to (1110)150 by each rightward pass)
⟶ the same cells at the next canonical point
——✓300/300
OV left overflow (empirical, ordinary case)
left counter full after 3*2m trips (minus the previous residual)
⟶ pause of about 80*2m steps confined to cells -90..50; counter restarts with residual 10..23; middle and right counter unchanged
fails once: m = 14 ends with a 150-trip creep that rebuilds the middle; the throttle loses its top digit (K 3 -> 2), residual 7742,030 * 2m-9 roughly✗9/10
Compressed historythe tape as 0∞ 1 [binary digits D_m..D_0: 001101=0, 101101=1] (1110)150 [s3 t_0..t_(K-1) 1011] (0011)e 0∞ (at each left-counter overflow) at 11 moments: where the rules are read off
0∞ 1 [binary digits D_m..D_0: 001101=0, 101101=1] (1110)150 [s3 t_0..t_(K-1) 1011] (0011)e 0∞ (at each left-counter overflow)
stepm (overflow ends the 3*2^m-trip period)pause stepsK (ternary digits after)right edge (cell)
3,664,3439 (start-up)42,0303898
7,645,6811081,56431,198
15,759,54311161,92831,806
32,542,53912320,58233,018
68,335,91713639,88435,442
148,780,41514 (creep)1,299,366210,294
626,342,411152,550,784239,374
2,854,429,677165,099,496297,622
12,401,584,36317~101948182214,130
51,855,760,94718~203916322447,142
200,000,000,000(run end)-2886,362
m (overflow ends the 3*2^m-trip period)last (run end)
18107.6e65.2e10log xstep 7645681: m (overflow ends the 3*2^m-trip period) = 10step 15759543: m (overflow ends the 3*2^m-trip period) = 11step 32542539: m (overflow ends the 3*2^m-trip period) = 12step 68335917: m (overflow ends the 3*2^m-trip period) = 13step 626342411: m (overflow ends the 3*2^m-trip period) = 15step 2854429677: m (overflow ends the 3*2^m-trip period) = 16step 12401584363: m (overflow ends the 3*2^m-trip period) = 17step 51855760947: m (overflow ends the 3*2^m-trip period) = 18
pause stepslast -
5.1e642,0303.7e62.9e9step 3664343: pause steps = 42030step 7645681: pause steps = 81564step 15759543: pause steps = 161928step 32542539: pause steps = 320582step 68335917: pause steps = 639884step 148780415: pause steps = 1299366step 626342411: pause steps = 2550784step 2854429677: pause steps = 5099496
K (ternary digits after)last 2
323.7e62e11log xstep 3664343: K (ternary digits after) = 3step 7645681: K (ternary digits after) = 3step 15759543: K (ternary digits after) = 3step 32542539: K (ternary digits after) = 3step 68335917: K (ternary digits after) = 3step 148780415: K (ternary digits after) = 2step 626342411: K (ternary digits after) = 2step 2854429677: K (ternary digits after) = 2step 12401584363: K (ternary digits after) = 2step 51855760947: K (ternary digits after) = 2step 200000000000: K (ternary digits after) = 2
right edge (cell)last 886,362
8.9e58983.7e62e11log xstep 3664343: right edge (cell) = 898step 7645681: right edge (cell) = 1198step 15759543: right edge (cell) = 1806step 32542539: right edge (cell) = 3018step 68335917: right edge (cell) = 5442step 148780415: right edge (cell) = 10294step 626342411: right edge (cell) = 39374step 2854429677: right edge (cell) = 97622step 12401584363: right edge (cell) = 214130step 51855760947: right edge (cell) = 447142step 200000000000: right edge (cell) = 886362
Template comparisonSBCv8.v TM31: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB0RA
B1RC1RF
C1LD0LC
D1RA1LE
E1RA0LC
F---0RDtpl 0RE

differs from the template

file
SBCv8.v:9675
module
TM31 (nonhalt via Longitudinal segRLs lemmas, BigStep312, progress_nonhalt_cond)
machine
1RB0RA_1RC1RF_1LD0LC_1RA1LE_1RA0LC_---0RE (1 transition apart)
diff
F1: 0RD (ours) vs 0RE (TM31); the other 11 transitions are equal
note
Same vocabulary and layout: the 10 wall, d = 011011 blocks on the left (our binary digits), w = 0011/0110 blocks in the middle, and a (1110)^e right region. Simulated TM31: its tape at right records reads 0^inf 10 ...(1011)^30 0 (1101)^451 ... (1110)^4416, but its right edge grows in bursts (no right record from 4.65e8 to 1e9). Ours grows steadily under a ternary P/Q/R throttle and has nested overflow pauses. Reuse the segRLs transfer-lemma machinery (Incs_d/Incs_w style, DivModCases for the mod-3 digits), not TM31's P ls i c invariant or BigStep312.
Proof strategy & riskshow the formal proof will go · 3 risks to watch

Longitudinal proof like TM31: segRLs transfer lemmas per block (binary d digits, ternary P/Q/R digits, transparent 0011 middle). Invariant over (V, wall state, s3, T, K, e, middle length). Blocker: rules for the overflow pause and the creep (rule OV).

  • ▲The overflow pause has no rules yet: an inner counter in the middle receives about 2^m trips, and how it exits decides creep vs no creep.
  • ▲The creep trigger (only m = 14 among m = 9..18) may depend on arithmetic such as the base-3 digits of ~2^m. That would be cryptid-like in when it happens, though K drops proved harmless in tests.
  • ▲Hand tests show K = 1, 0, -1 keep running, but what a creep does once no ternary digits are left is untested.
Stats & provenance2·1011 steps simulated · 191,526 cells · the status in full · files
simulated
2·1011 steps
tape
191,526 cells · 126,623 nonzeros
growth
right edge +4 cells per record, records every (3/2)*3^K trips; ~t^0.5 asymptotically (t^0.70 over 1.3e8..1e10); left edge ~log t (capacity 3*2^m)
status now
Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Park. Funded f3_first stage done (2026-10-11): F3 has no closed family. The big region after the marker is a fourth zone shaped like M (ternary word, AC/DC interface, exact rules 40,766/40,766 visits), and its gliders build new throttle levels with K = 3 at the right end (GX/NB 33/33), so from m ~ 236 the run is an unbounded tower of levels. B^j A^n with j up to ~1e6 never halted (300 + 54 runs), and glider bursts B^5/B^4 are safe, but zone T halts on small bursts with short gaps (B^1 15/200, B^3 2/200) and on A-on-junk words. Deeper levels can receive B^3 bursts and arbitrary gaps. Excluding the unsafe patterns needs control of pseudo-random burst timing (heuristically ~2^-m per epoch), which is cryptid-like for a proof. Non-halting is heuristically very likely, but proof confidence is low. Recommendation: park; a decision is queued. (status.json, 2026-10-12)
observer's note
Normal regime ruled and validated (4 rules, 600/600 random instances; RM 300/300). The overflow pause and the m=14 creep are unruled. Confidence low, so this waits for Dennis before any proof work. Not cryptid so far: no halt to 2e11.
files
observe.json · notes.md · proof.md · status.json

Proof & checks

Files

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

namesizechanged
notes.md ↓35 KB2026-10-12 08:59
proof.md ↓16 KB2026-10-10 15:18
status.json ↓1.2 KB2026-10-12 08:59
observe.json ↓11 KB2026-10-10 10:58
deepen.json ↓16 KB2026-10-11 08:52
decision.json ↓2.5 KB2026-10-12 08:59
data/9 items2026-10-11 08:34
decisions/4 items2026-10-11 08:49
img/6 items2026-10-10 10:56
scripts/21 items2026-10-11 08:21
check_proof.py ↓18 KB2026-10-10 15:18
compress_track_1e9.txt ↓4.4 KB2026-10-10 10:16
ovf_1e10.txt ↓5.3 KB2026-10-10 10:32
ovf_2e11.txt ↓5.3 KB2026-10-10 10:52
records_1e10.jsonl ↓19 MB2026-10-10 10:14
sim_1e9.txt ↓193 B2026-10-10 10:14
sweeps_1e10.txt ↓1.0 MB2026-10-10 10:21
sweeps_2e11.txt ↓5.0 MB2026-10-10 10:52
sweeps_3e8.txt ↓4.0 MB2026-10-10 10:19
validation.json ↓281 B2026-10-10 10:52
validation_seed2.json ↓334 B2026-10-10 10:57
status.json in full
{
 "tm": "1RB0RA_1RC1RF_1LD0LC_1RA1LE_1RA0LC_---0RD",
 "status": "STUCK",
 "stage": "f3_first",
 "updated": "2026-10-12",
 "reason": "Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Park. Funded f3_first stage done (2026-10-11): F3 has no closed family. The big region after the marker is a fourth zone shaped like M (ternary word, AC/DC interface, exact rules 40,766/40,766 visits), and its gliders build new throttle levels with K = 3 at the right end (GX/NB 33/33), so from m ~ 236 the run is an unbounded tower of levels. B^j A^n with j up to ~1e6 never halted (300 + 54 runs), and glider bursts B^5/B^4 are safe, but zone T halts on small bursts with short gaps (B^1 15/200, B^3 2/200) and on A-on-junk words. Deeper levels can receive B^3 bursts and arbitrary gaps. Excluding the unsafe patterns needs control of pseudo-random burst timing (heuristically ~2^-m per epoch), which is cryptid-like for a proof. Non-halting is heuristically very likely, but proof confidence is low. Recommendation: park; a decision is queued.",
 "funded": {
  "option": "f3_first",
  "date": "2026-10-11"
 },
 "confidence": "low",
 "parked": "Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Park."
}
observe.json contract (tools/README-card.md):
1 contract warning
  • rank: not an int