Built . It shows the files as they were then (ages and “working now” follow your clock).
tools/rebuild_pages.sh rebuilds the site within 5 minutes of a change; by hand: python3 -B tools/site.py.Machines / #13
1RB0LE_1LC1RD_1LA0RB_1RC1RB_1LF0LC_---0RC
Where it stands
Parked at the informal proof
Parked by Dennis 2026-10-10 (decision queue: park; proof.md kept as the conditional reduction). Fatal skeptic gap stands: the edge lemma is unproved, so non-halting is only conditional.
Read the full status
(E) as first stated just restates 'the edge never breaks'. proof.md now sharpens it to (E'): a one-sided right-part system with a fixed 16-round-trip protocol at the boundary one cell left of the X0|D cut (checks IFACE, E'). No closed language L is known, and none of the regular candidates closes: SFT_k invariants are refuted for k <= 36 (verified chains in work/sft_refutations), and plain n-gram CPS does not close, whole-machine n <= 26 or edge-system n <= 24. Whether any regular invariant exists is unknown. Everything else (rules, bounces, cycle law, init at 784,041 via the Bouncer_v3 pattern) is routine and checked. Minor gaps 2-7 fixed (review log in proof.md section 9). PRIORITY CALL for Dennis: spend more budget on (E')? Routes: native reimplementation of busycoq CTL modes for a whole-machine certificate (days, unknown odds), or edge-only closed set plus a new Coq checker (1-3 weeks plus finding the set).
Observe
Deepen
Informal proof
Rocq
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
Clean period-10 bouncer; every 7 bounces a fixed probe stirs a ~144-564-cell chaotic tail D. Tail = the whole problem.
- Status
- Parkedinformal proof · updated 2026-10-10Not blocking · Stuck at the informal proof stage. Answer Q1–Q3 whenever; a “no” redirects the work.idle since Oct 10 12:52 · status.json 2026-10-10
- Informal proof
- proof.mdconditional; see Proof for what is still open
- Class
- Bouncer + Chaotic Edgeours: Bouncer + Chaotic Edge (sheet) · ours adds: translating period-10 bouncer feeding a 1-sided chaotic edge map · high confidence
- On the list
- line 401 of
BB6_holdouts_663.txt· historical 740 line 443
Your calls on file 3
- priority call (answered)
- Continue investing in the edge lemma (E') or park the machine?
- parked
- Parked by Dennis 2026-10-10 (decision queue: park; proof.md kept as the conditional reduction).
- decision.json · answered 2026-10-10: park
- Continue investing in the edge lemma (E') or park the machine? Decisions →
Mechanism
How it works: 3 notes
- Bulk (1101101101)^a sits on a left wall; each bounce shifts it 1 cell left (70a steps).
- A fixed 54-cell junction cycles through 7 shapes; the bulk gains 1 block per 7 bounces.
- Only every 7th bounce enters the tail D (the same 16 round trips = 32 crossings, one cell left of the cut, each time). D stays 144-564 cells, content chaotic.
Figures for Checkpoint A
One row per bounce from a built tape: bulk at left, junction seam in the middle, tail D at right.
bbchallenge-defaultStart constructed: 0∞ <A (1101101101)20 X0 D0 0∞Rows left recordsWindow cells -320..725, 1 px = 0.5 cellsColors 1 0 or never visited head just moved right/left
Start: X0 = the fixed 54-cell junction; D0 = the real 261-cell tail at step 784,041, where the real bulk is a = 59, not 20 · Rows: the start, then one row per new leftmost cell = one row per bounce (321 rows, steps 0..1,200,000; 7 rows = one probe cycle) · Window: each cell is 2x2 px; cell 0 = the cell the head reads at the start
Each row is shifted so the right edge stays put. Compare the noisy band's width at top and bottom.
bbchallenge-defaultStart blankRows left recordsWindow cells -1199..0, 1 px = 1 cellColors 1 0 or never visited head just moved right/left
Rows: the start, then one row per new leftmost cell = one row per bounce (4,297 rows, steps 0..100,000,000; rows are not equal time) · Window: counted from the right edge (each row is shifted so its rightmost visited cell is at 0; the bulk continues off-picture to the left)
Blaze view to 1e7 steps. Compare the left edge with the right edge.
bbchallenge-blazeStart blankRows Blaze time blocks of 16,384 stepsWindow cells -1256..1085, 1 px = 2.93 cellsColors 0 1 mixed
Rows: (averaged), 611 blocks stretched to 500 px, so 1 px row ~ 20,000 steps (steps 0..10,000,000) · Colors: paler orange: each pixel averages its cells over its time block; no head drawn
More figures (1)Fig 4: bbchallenge Default view, first 10,000 steps
For orientation: the start of the run as bbchallenge.org shows it.
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 20:1 into 500 px as on bbchallenge.org (px row y blends steps 20y+9 and 20y+10)
Rules (8/8 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
| rule | from ⟶ to | cases | steps | checked |
|---|---|---|---|---|
| cycle (7 bounces) | 0∞ <A (1101101101)a X0 D 0∞ ⟶ 0∞ <A (1101101101)a+1 X0 P(D) 0∞ | P(D) chaotic; holds every cycle from step 784,041 (a=59) | 490a + O(|D|^2) | ✓1951/1951 |
| probe bounce | 0∞ <A (1101101101)a X0 D 0∞ ⟶ 0∞ <A (1101101101)a X1 011 P(D) 0∞ | P independent of a; fixed 16 round trips (32 crossings) one cell left of the cut | 70a + c(D), c in [2235,10775] | ✓180/180 |
| junction bounces k=1..5 | 0∞ <A (1101101101)a X_k D 0∞ ⟶ 0∞ <A (1101101101)a+[k=5] X_(k+1) D 0∞ | D untouched (any D); X_k in notes.md | 70a+b_k, b=(9,473,55,49,77) | ✓80/80 |
| cycle close k=6 | 0∞ <A (1101101101)a X6 011 D 0∞ ⟶ 0∞ <A (1101101101)a X0 D 0∞ | cut moves +3 cells | 70a+9 | ✓16/16 |
| right sweep | 1 B> (0110110111)n ⟶ (0111101101)n 1 B> | — | 12n | ✓16/16 |
| left sweep | (1011110110)n 11110101 <E 0 ⟶ 11110101 <E 0 (1101101101)n | — | 58n | ✓16/16 |
| left wall | 0∞ <A r ⟶ 0∞ 1 B> r | — | 1 | ✓30/30 |
| halt pattern | 001 C> 0 ⟶ halt | the only halting route | 4 | ✓20/20 |
Compressed historythe tape as 0∞ <A (1101101101)a X0 D 0∞ (X0 = 110111100110011101100100100111101100100110110111010011) at 33 moments: where the rules are read off
0∞ <A (1101101101)a X0 D 0∞ (X0 = 110111100110011101100100100111101100100110110111010011)
| step | a | |D| | D (first 24 cells) |
|---|---|---|---|
| 784,041 | 59 | 261 | 1.1·1022 |
| 819,860 | 60 | 258 | 1.1·1022 |
| 852,629 | 61 | 255 | 1.11·1022 |
| 889,610 | 62 | 252 | 1·1021 |
| 924,145 | 63 | 249 | 1.1·1022 |
| 960,508 | 64 | 246 | 1.11·1022 |
| 996,135 | 65 | 243 | 1·1021 |
| 1,141,833 | 69 | 231 | 1.1·1022 |
| 1,259,438 | 72 | 222 | 1·1021 |
| 1,462,875 | 77 | 207 | 1.11·1022 |
| 1,730,709 | 83 | 249 | 1.1·1022 |
| 2,116,305 | 91 | 255 | 1.11·1022 |
| 2,638,489 | 101 | 285 | 1.11·1022 |
| 3,459,863 | 115 | 363 | 1.11·1022 |
| 4,721,116 | 134 | 336 | 1.1·1022 |
| 6,636,675 | 159 | 321 | 1.11·1022 |
| 9,643,128 | 192 | 312 | 1.1·1022 |
| 14,607,161 | 237 | 327 | 1.1·1022 |
| 22,589,584 | 296 | 300 | 1·1021 |
| 35,992,489 | 375 | 363 | 1.1·1022 |
| 58,743,103 | 481 | 285 | 1.11·1022 |
| 97,252,227 | 621 | 255 | 1.1·1022 |
| 164,063,019 | 809 | 321 | 1.1·1022 |
| 279,751,465 | 1,059 | 411 | 1·1021 |
| 482,122,705 | 1,393 | 279 | 1.11·1022 |
| 835,786,657 | 1,837 | 387 | 1·1021 |
| 999,751,742 | 2,010 | 348 | 1.1·1022 |
| 2.45·1014 | 1,000,059 | 261 | edge map (|D| 144-519 in window) |
| 9.8·1014 | 2,000,059 | 321 | edge map (|D| 180-561 in window) |
| 2.2·1015 | 3,000,059 | 261 | edge map (|D| 171-534 in window) |
| 3.92·1015 | 4,000,059 | 381 | edge map (|D| 183-564 in window) |
| 6.12·1015 | 5,000,059 | 291 | edge map (|D| 174-519 in window) |
| 7.41·1015 | 5,500,059 | 321 | edge map (|D| 171-552 in window) |
alast 5,500,059|D|last 321D (first 24 cells)last edge map (|D| 171-552 in window)Template comparisonBouncer_v3.v TM1: partly applies · the nearest solved proof, what carries over, and the transitions that differ
| 0 | 1 | |
|---|---|---|
| A | 1RB | 0LE |
| B | 1LC | 1RD |
| C | 1LA | 0RB |
| D | 1RC | 1RB |
| E | 1LF | 0LC |
| F | --- | 0RC |
differs from the template
- file
Bouncer_v3.v:44- module
TM1- machine
1LB1RA_0RA0RC_---1RD_1RE1RB_1LF0LE_0RD0LE(10 transitions apart)- diff
8 transitions apart under best relabel (A0 A1 B0 B1 C0 C1 E0 F1): class template, not a neighbour- note
- Shape carries over: left wall (sideRLs_wall) + whole tape as right side + k-bounce BigStep (ours k=7, theirs 128). Its RInc native check needs a periodic edge; our D never repeats (5500000 cycles), so D needs a closed-language lemma.
Proof strategy & riskshow the formal proof will go · 3 risks to watch
Longitudinal split as in Bouncer_v3/LongNv1: wall + bulk sweeps by ind (12n, 58n) + 7 fixed junction bounces reduce nonhalt to the 1-sided edge map D -> P(D) with a fixed 16-round-trip (32-crossing) input one cell left of the cut (sideRLs list). Then find a closed regular language for D outside Rocq (CTL/FAR-style automaton on the edge map) and check it in Rocq verified-checker style (Fixpoint + soundness + vm_compute).
- ▲No small closed language for D may exist (FAR failed on the full machine; the SFT {000,0101,01101111} is not closed).
- ▲Proving P independent of a and the junction lemmas needs segRLs/sideRLs plumbing (LongN/InfiniteRect style, 15-30 KB).
- ▲|D| bounded only empirically (144-564); a very long transient could still end in 001 C> 0.
Stats & provenance109 steps simulated · 20,564 cells · the status in full · files
- simulated
- 109 steps
- tape
- 20,564 cells · 14,332 nonzeros
- growth
- both edges ~sqrt(t) (lo -0.44sqrt t, hi +0.21sqrt t); edge map 5500000 cycles ~ 7.4e+15 steps, |D| 144-564
- status now
- Parked by Dennis 2026-10-10 (decision queue: park; proof.md kept as the conditional reduction). Fatal skeptic gap stands: the edge lemma is unproved, so non-halting is only conditional. (E) as first stated just restates 'the edge never breaks'. proof.md now sharpens it to (E'): a one-sided right-part system with a fixed 16-round-trip protocol at the boundary one cell left of the X0|D cut (checks IFACE, E'). No closed language L is known, and none of the regular candidates closes: SFT_k invariants are refuted for k <= 36 (verified chains in work/sft_refutations), and plain n-gram CPS does not close, whole-machine n <= 26 or edge-system n <= 24. Whether any regular invariant exists is unknown. Everything else (rules, bounces, cycle law, init at 784,041 via the Bouncer_v3 pattern) is routine and checked. Minor gaps 2-7 fixed (review log in proof.md section 9). PRIORITY CALL for Dennis: spend more budget on (E')? Routes: native reimplementation of busycoq CTL modes for a whole-machine certificate (days, unknown odds), or edge-only closed set plus a new Coq checker (1-3 weeks plus finding the set). (status.json, 2026-10-10)
- observer's note
- Mechanism found and validated (bulk, junction, probe); tail D is chaotic but bounded, not arithmetic (no Collatz-like growth), so not a cryptid. Next: closed language for the edge map.
- files
- observe.json · notes.md · proof.md · status.json
Proof & checks
- proof.md · the informal proof
- check_proof.py · the numeric checks of proof.md
Files
machines/<tm>/: 9 entries · raw notes, status, scripts, images
| name | size | changed |
|---|---|---|
| notes.md ↓ | 8.9 KB | 2026-10-10 12:49 |
| proof.md ↓ | 24 KB | 2026-10-10 04:25 |
| status.json ↓ | 1.4 KB | 2026-10-10 12:52 |
| observe.json ↓ | 12 KB | 2026-10-10 04:41 |
| decision.json ↓ | 3.9 KB | 2026-10-10 12:49 |
| img/ | 10 items | 2026-10-10 02:00 |
| scripts/ | 7 items | 2026-10-10 04:25 |
| work/ | 19 items | 2026-10-10 04:20 |
| check_proof.py ↓ | 16 KB | 2026-10-10 04:24 |
status.json in full
{
"tm": "1RB0LE_1LC1RD_1LA0RB_1RC1RB_1LF0LC_---0RC",
"status": "STUCK",
"stage": "informal_proof",
"updated": "2026-10-10",
"reason": "Parked by Dennis 2026-10-10 (decision queue: park; proof.md kept as the conditional reduction). Fatal skeptic gap stands: the edge lemma is unproved, so non-halting is only conditional. (E) as first stated just restates 'the edge never breaks'. proof.md now sharpens it to (E'): a one-sided right-part system with a fixed 16-round-trip protocol at the boundary one cell left of the X0|D cut (checks IFACE, E'). No closed language L is known, and none of the regular candidates closes: SFT_k invariants are refuted for k <= 36 (verified chains in work/sft_refutations), and plain n-gram CPS does not close, whole-machine n <= 26 or edge-system n <= 24. Whether any regular invariant exists is unknown. Everything else (rules, bounces, cycle law, init at 784,041 via the Bouncer_v3 pattern) is routine and checked. Minor gaps 2-7 fixed (review log in proof.md section 9). PRIORITY CALL for Dennis: spend more budget on (E')? Routes: native reimplementation of busycoq CTL modes for a whole-machine certificate (days, unknown odds), or edge-only closed set plus a new Coq checker (1-3 weeks plus finding the set).",
"parked": "Parked by Dennis 2026-10-10 (decision queue: park; proof.md kept as the conditional reduction).",
"priority_call_answered": "Continue investing in the edge lemma (E') or park the machine?"
}