BB(6) hunt
Machines / #5

1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD

#5Cryptid candidateBouncer + Chaotic Edgebbchallenge ↗Explorer

Where it stands

Cryptid candidate, parked at the Rocq proof

Dennis 2026-10-10: flag as cryptid candidate, deprioritize. research/erosion.md: no deterministic erosion bound found (potentials miss by 5-12x; edge ~0.63 bits/cell); no halt in 1e8 bounces (~9.6e15 steps). Cryptid protocol still owes a formal rule reduction in Rocq (bounce = 7 local rules) before the label is final.

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

Bouncer; chaotic left edge slowly eats the 1-block. No-00 invariant: it can only halt if the edge eats the whole block

Status
Cryptid candidateresearch · updated 2026-10-12Parked · Dennis 2026-10-10: flag as cryptid candidate, deprioritize. The 3 open questions are optional.
idle since Oct 12 10:06 · status.json 2026-10-12
Class
Bouncer + Chaotic Edgeours: Bouncer + Chaotic Edge (sheet) · ours adds: edge erodes the bouncer block; golden-mean invariant · high confidence
On the list
line 331 of BB6_holdouts_663.txt · historical 740 line 365
#5eqv ×1sim 1e15UBRRBA

Mechanism

How it works: 3 notes
  • Bouncer: a solid 1-block gains one 1 per bounce; left of it sits a chaotic, aperiodic edge (~0.6 bits/cell).
  • Each bounce C dives into the edge in zigzag waves; the edge eats ~0.06 block cells per bounce on average, up to 11.
  • No 00 ever lies between head and rightmost 1 (checked to 1e9, local proof): it halts only if the block falls to 2 cells.

Figures for Checkpoint A

Fig 1 · The edge eating into the block, to 1e9Q1

One row per 400,000 steps to 1e9. Compare the left stripes with the textured fringe at the white block.

The edge eating into the block, to 1e9
bbchallenge-defaultStart blankRows every 400,000 stepsWindow cells -349..2250, 1 px = 1 cellColors 1 0 or never visited dot: head (last move R/L)
Rows: 2,501 rows for steps 0..1e9 (506 bounces between the first rows, 6 between the last) · Window: the left 2,600 cells of the 32,607-cell tape; the block runs on to cell 32,261 · Colors: blue numbered dots = notes
Fig 2 · Close-up: bounces 54 to 57, every stepQ2viewer ↗

Bounces 54 to 57, every step. Look between the head and the white block for adjacent black cells.

Close-up: bounces 54 to 57, every step
bbchallenge-defaultStart mid-run: step 12,287Rows every step: steps 12,287..12,992 = bounces 54 to 57Window cells -76..59, 1 px = 0.2 cellsColors 1 0 head moving R/L line: block's left end at the last bounce circle: wave turns at 00
Start: bounce 54, simulated from the blank tape · Rows: 1 step = 2 px tall · Window: each cell 5 px wide; the whole visited tape
Fig 3 · Block length vs erosion, per bounceQ3viewer ↗

Four panels, one value per bounce. Bottom left: cells eaten per trip (orange band = min..max per 128 bounces).

Block length vs erosion, per bounce
customStart blankRows one point per bounceWindow not a tape pictureColors block length n edge width |w| and erosion band: min..max per 128 bounces
Rows: bounces 1..32,262 = steps 0..999,944,025 · Window: x = bounce number, y = cells (block length, edge width, cells eaten) · Colors: orange: block cells eaten per trip
More figures (1)Fig 4: bbchallenge default view, first 10,000 steps
Fig 4 · bbchallenge default view, first 10,000 stepsviewer ↗

The site's view: the textured edge on the left, the growing white block on the right.

bbchallenge default view, first 10,000 steps
bbchallenge-defaultStart blankRows every step 0..10,000 squeezed into 500 px rows as on the siteWindow cells -200..199, 1 px = 1 cellColors 1 0 or never visited head moving R/L
Rows: each px row blends steps 20y+9 and 20y+10
Rules (9/9 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
Bounce off the right end
x A> 1n 0∞
⟶ x <C 1n+1 0∞
any left side x, n >= 02n+3✓48/48
C walks left over 1s
x 0 1k <C y
⟶ x 0 <C 1k y
any x, y; k >= 1k✓48/48
Wave turns at 00
x 0 0 <C y
⟶ x 1 0 A> y
C on 0 with a 0 to its left3✓40/40
Wave carry 010
x 0 1 0 <C y
⟶ x <C 0 1 1 y
C on 0, left cells 0 1; wave continues3✓40/40
Wave fold 110
x 1 1 0 <C y
⟶ x <D 1 0 1 y
C on 0, left cells 1 1 (with the two rules above: complete split of C on 0)7✓40/40
Bounce map (block = wall)
0∞ w <C 1n 0∞
⟶ 0∞ f(w) <C 1n+1-e(w) 0∞
n >= e(w)+3; f, e, s from the wall model (does not depend on n); also exact on 32,061 consecutive real bouncess(w)+2(n-e(w))+3✓120/120
Halting door (only way to halt)
x A> 0 1 0j 1 0 0 y
⟶ halt
j >= 0; the only path into E0 is A0, B1, F0^j, F1, D0 (traced back from the transition table)j+5✓48/48
No 00 right of head (invariant)
any configuration reached from blank
⟶ cells head+1 .. rightmost 1 contain no 00
Only B0 moves left writing 0, and its right neighbour is always 1. Validated at every step; arbitrary-left search: 182,877 states, 0 violations—✓1000000000/1000000000
End doors (door + invariant)
x A> 0 1 1 0∞ | x A> 0 1 0 1 0∞
⟶ halt
with the invariant these are the only halting configurations: the block has been eaten down to 2 cells5 | 6✓40/40
Compressed historythe tape as 0∞ w 1n A> 0∞ at 32 moments: where the rules are read off
0∞ w 1n A> 0∞
stepbounce|w| (edge width)n (block)lodive depth of next bouncelast 16 cells of w
7221-2610
36381-71110,110,010
2325191-16101.01·1015
75110302-23311.1·1015
1,51514417-35451.01·1013
2,08716532-40321.01·1014
2,52720518-4091.11·1015
3,813305227-50471.11·1014
10,819507939-69101.1·1014
36,13310016076-1371491.11·1015
99,583200195196-19291.11·1015
391,927500325418-244101.1·1014
1,279,8871,000364923-288231.01·1015
4,517,1872,0003711,924-296261.01·1015
9,733,6493,0003892,906-2961471.11·1015
23,935,9094,7905554,578-344161.1·1015
36,764,1636,0007395,604-344461.11·1015
63,891,9778,0008197,524-344201.11·1015
98,657,73710,0009299,414-3441251.11·1014
141,448,41512,00079811,545-344761.11·1014
192,212,80114,00086613,477-3441351.1·1015
250,521,93916,0001,01115,332-34481.11·1014
316,323,16918,0001,26817,075-344201.1·1015
389,050,18320,0001,46718,876-344161.01·1014
469,510,48322,0001,41020,933-3441771.01·1014
557,615,57124,0001,60722,736-34491.11·1015
623,953,00025,4071,76123,989-3448881.11·1014
653,003,23526,0001,79224,551-344691.01·1014
755,917,53928,0001,91526,428-344101.1·1014
866,138,56130,0002,00928,334-344101.01·1015
983,977,63132,0002,17130,172-344201.11·1015
999,882,96632,2612,20530,399-344471.1·1015
bouncelast 32,261
32,261271e9log xstep 7: bounce = 2step 36: bounce = 3step 232: bounce = 5step 751: bounce = 10step 1515: bounce = 14step 2087: bounce = 16step 2527: bounce = 20step 3813: bounce = 30step 10819: bounce = 50step 36133: bounce = 100step 99583: bounce = 200step 391927: bounce = 500step 1279887: bounce = 1000step 4517187: bounce = 2000step 9733649: bounce = 3000step 23935909: bounce = 4790step 36764163: bounce = 6000step 63891977: bounce = 8000step 98657737: bounce = 10000step 141448415: bounce = 12000step 192212801: bounce = 14000step 250521939: bounce = 16000step 316323169: bounce = 18000step 389050183: bounce = 20000step 469510483: bounce = 22000step 557615571: bounce = 24000step 623953000: bounce = 25407step 653003235: bounce = 26000step 755917539: bounce = 28000step 866138561: bounce = 30000step 983977631: bounce = 32000step 999882966: bounce = 32261
|w| (edge width)last 2,205
2,205271e9log xstep 7: |w| (edge width) = 2step 36: |w| (edge width) = 8step 232: |w| (edge width) = 19step 751: |w| (edge width) = 30step 1515: |w| (edge width) = 41step 2087: |w| (edge width) = 53step 2527: |w| (edge width) = 51step 3813: |w| (edge width) = 52step 10819: |w| (edge width) = 79step 36133: |w| (edge width) = 160step 99583: |w| (edge width) = 195step 391927: |w| (edge width) = 325step 1279887: |w| (edge width) = 364step 4517187: |w| (edge width) = 371step 9733649: |w| (edge width) = 389step 23935909: |w| (edge width) = 555step 36764163: |w| (edge width) = 739step 63891977: |w| (edge width) = 819step 98657737: |w| (edge width) = 929step 141448415: |w| (edge width) = 798step 192212801: |w| (edge width) = 866step 250521939: |w| (edge width) = 1011step 316323169: |w| (edge width) = 1268step 389050183: |w| (edge width) = 1467step 469510483: |w| (edge width) = 1410step 557615571: |w| (edge width) = 1607step 623953000: |w| (edge width) = 1761step 653003235: |w| (edge width) = 1792step 755917539: |w| (edge width) = 1915step 866138561: |w| (edge width) = 2009step 983977631: |w| (edge width) = 2171step 999882966: |w| (edge width) = 2205
n (block)last 30,399
30,399171e9log xstep 7: n (block) = 1step 36: n (block) = 1step 232: n (block) = 1step 751: n (block) = 2step 1515: n (block) = 7step 2087: n (block) = 2step 2527: n (block) = 8step 3813: n (block) = 27step 10819: n (block) = 39step 36133: n (block) = 76step 99583: n (block) = 196step 391927: n (block) = 418step 1279887: n (block) = 923step 4517187: n (block) = 1924step 9733649: n (block) = 2906step 23935909: n (block) = 4578step 36764163: n (block) = 5604step 63891977: n (block) = 7524step 98657737: n (block) = 9414step 141448415: n (block) = 11545step 192212801: n (block) = 13477step 250521939: n (block) = 15332step 316323169: n (block) = 17075step 389050183: n (block) = 18876step 469510483: n (block) = 20933step 557615571: n (block) = 22736step 623953000: n (block) = 23989step 653003235: n (block) = 24551step 755917539: n (block) = 26428step 866138561: n (block) = 28334step 983977631: n (block) = 30172step 999882966: n (block) = 30399
lolast -344
-2-34471e9log xstep 7: lo = 2step 36: lo = 7step 232: lo = 16step 751: lo = 23step 1515: lo = 35step 2087: lo = 40step 2527: lo = 40step 3813: lo = 50step 10819: lo = 69step 36133: lo = 137step 99583: lo = 192step 391927: lo = 244step 1279887: lo = 288step 4517187: lo = 296step 9733649: lo = 296step 23935909: lo = 344step 36764163: lo = 344step 63891977: lo = 344step 98657737: lo = 344step 141448415: lo = 344step 192212801: lo = 344step 250521939: lo = 344step 316323169: lo = 344step 389050183: lo = 344step 469510483: lo = 344step 557615571: lo = 344step 623953000: lo = 344step 653003235: lo = 344step 755917539: lo = 344step 866138561: lo = 344step 983977631: lo = 344step 999882966: lo = 344
dive depth of next bouncelast 47
888671e9log xstep 7: dive depth of next bounce = 6step 36: dive depth of next bounce = 11step 232: dive depth of next bounce = 10step 751: dive depth of next bounce = 31step 1515: dive depth of next bounce = 45step 2087: dive depth of next bounce = 32step 2527: dive depth of next bounce = 9step 3813: dive depth of next bounce = 47step 10819: dive depth of next bounce = 10step 36133: dive depth of next bounce = 149step 99583: dive depth of next bounce = 9step 391927: dive depth of next bounce = 10step 1279887: dive depth of next bounce = 23step 4517187: dive depth of next bounce = 26step 9733649: dive depth of next bounce = 147step 23935909: dive depth of next bounce = 16step 36764163: dive depth of next bounce = 46step 63891977: dive depth of next bounce = 20step 98657737: dive depth of next bounce = 125step 141448415: dive depth of next bounce = 76step 192212801: dive depth of next bounce = 135step 250521939: dive depth of next bounce = 8step 316323169: dive depth of next bounce = 20step 389050183: dive depth of next bounce = 16step 469510483: dive depth of next bounce = 177step 557615571: dive depth of next bounce = 9step 623953000: dive depth of next bounce = 888step 653003235: dive depth of next bounce = 69step 755917539: dive depth of next bounce = 10step 866138561: dive depth of next bounce = 10step 983977631: dive depth of next bounce = 20step 999882966: dive depth of next bounce = 47
last 16 cells of wlast 1.1·1015
1.1e151071e9log-logstep 7: last 16 cells of w = 10step 36: last 16 cells of w = 10110010step 232: last 16 cells of w = 1010100101110010step 751: last 16 cells of w = 1101101110110010step 1515: last 16 cells of w = 10111110101010step 2087: last 16 cells of w = 101101110110010step 2527: last 16 cells of w = 1110110010101010step 3813: last 16 cells of w = 111011110101010step 10819: last 16 cells of w = 110100101110010step 36133: last 16 cells of w = 1111011110101010step 99583: last 16 cells of w = 1110110010101010step 391927: last 16 cells of w = 110100101110010step 1279887: last 16 cells of w = 1010100110101010step 4517187: last 16 cells of w = 1010100110101010step 9733649: last 16 cells of w = 1111011110101010step 23935909: last 16 cells of w = 1100110110110010step 36764163: last 16 cells of w = 1111011110101010step 63891977: last 16 cells of w = 1111011110101010step 98657737: last 16 cells of w = 111011110101010step 141448415: last 16 cells of w = 111011110101010step 192212801: last 16 cells of w = 1101101110110010step 250521939: last 16 cells of w = 111011001010010step 316323169: last 16 cells of w = 1100101110101010step 389050183: last 16 cells of w = 101101110110010step 469510483: last 16 cells of w = 101011110101010step 557615571: last 16 cells of w = 1110110010101010step 623953000: last 16 cells of w = 111011110101010step 653003235: last 16 cells of w = 101010101110010step 755917539: last 16 cells of w = 110100101110010step 866138561: last 16 cells of w = 1010100101110010step 983977631: last 16 cells of w = 1111011110101010step 999882966: last 16 cells of w = 1101101110110010
Template comparisonBouncer_v3.v TM1: does not apply · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB1RA
B0LC0RF
C1LD1LC
D1RE1LB
E---0RA
F1RF0RD
file
Bouncer_v3.v:44
module
TM1
machine
1LB1RA_0RA0RC_---1RD_1RE1RB_1LF0LE_0RD0LE (10 transitions apart)
diff
8 of 11 transitions differ (best mirror+relabel); InfiniteRect_v1 TM4: 8; LongNv1 TM1/TM2: 9
note
Bouncer_v3 needs a periodic side (RC i -> RC (i+1) every 128 bounces). Here 300/300 snapshots have distinct skeletons, and the mirrored RC 0 does not reach RC 1 after 128 bounces. LongN and InfiniteRect also need periodic interaction streams.
Proof strategy & riskshow the formal proof will go · 3 risks to watch

1) Prove the no-00 invariant as a closed predicate on the right side (progress_nonhalt_cond; checks the 11 transitions). Then halting needs A> 0 11 0^inf or A> 0 101 0^inf. 2) Show the edge never eats the block below 3 cells. This needs a potential that bounds the edge's growth per bounce (open). 3) Get from the blank tape to bounce ~30 (n=29) with es/execute, then apply 1) and 2) with an arbitrary left side l.

  • ▲The crux is a bound on erosion, and the edge's growth looks statistical: 0.057/bounce on average, up to 11 in one bounce, 60 in 50 bounces. If there is no deterministic bound, the machine is cryptid-like.
  • ▲There was an early close call: the block was 2 cells long at bounces 10 and 14-16. The init phase must simulate past it.
  • ▲Twin #26 1RB1RA_1LC1RE_---0LD_1LE1LD_0RA0LF_1LF0LB differs in 6 transitions, so we must re-derive the invariant before claiming 2 kills.
Stats & provenance109 steps simulated · 32,607 cells · the status in full · files
simulated
109 steps
tape
32,607 cells · 31,695 nonzeros
growth
span ~ t^0.5 (block +1 per bounce); edge +0.057 cells/bounce; 32,262 bounces by 1e9
status now
Dennis 2026-10-10: flag as cryptid candidate, deprioritize. research/erosion.md: no deterministic erosion bound found (potentials miss by 5-12x; edge ~0.63 bits/cell); no halt in 1e8 bounces (~9.6e15 steps). Cryptid protocol still owes a formal rule reduction in Rocq (bounce = 7 local rules) before the label is final. (status.json, 2026-10-12)
files
observe.json · notes.md · status.json
other viewers
closeup_bounces54-57 · closeup_waves · edge_every4e5_1e9_labeled

Proof & checks

○ Checkpoint B: no note from Dennis found

  • notes.md L68: - Checkpoint questions are now yes/no questions about the figures. Moved off the card (strategy calls, not figure reading; settle them in proof.md / Checkpoint B):

Files

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

namesizechanged
notes.md ↓12 KB2026-10-12 10:05
status.json ↓1.1 KB2026-10-12 10:06
observe.json ↓13 KB2026-10-10 04:41
img/15 items2026-10-10 02:00
research/3 items2026-10-10 02:26
rocq/3 items2026-10-12 10:04
work/28 items2026-10-10 00:38
status.json in full
{
 "tm": "1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD",
 "status": "CRYPTID_CANDIDATE",
 "stage": "observe+research",
 "updated": "2026-10-12",
 "reason": "Dennis 2026-10-10: flag as cryptid candidate, deprioritize. research/erosion.md: no deterministic erosion bound found (potentials miss by 5-12x; edge ~0.63 bits/cell); no halt in 1e8 bounces (~9.6e15 steps). Cryptid protocol still owes a formal rule reduction in Rocq (bounce = 7 local rules) before the label is final.",
 "rule_reduction": "2026-10-12: Rocq rule reduction compiles (machines/1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD/rocq/rule_reduction.v; no Admitted/Axiom): local rules + no-00 invariant proved; erosion_open stated as open Definition; ~halts <-> erosion_open proved (#5 and twin #26 via flip/perm). NOT a kill.",
 "reduction": "machines/1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD/rocq/reduction.v (2026-10-12): rule-system reduction, compiles 2.8 s, closed under the global context. reduction : EdgeNeverEats a0 -> ~ halts tm c0; reduction_iff; reduction_twin for #26. Open condition EdgeNeverEats is a premise, not proved. NOT a kill."
}
observe.json contract (tools/README-card.md):
1 contract warning
  • diagrams[2].window: not "cells A..B, 1 px = k cells"