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 / W4-8

`1RB1RA_1LC0RE_1LE0LD_0LB1LB_1RA0LF_1LD---`

W4-8ParkedUnknownbbchallenge ↗Explorer

Where it stands

Parked at the deeper analysis

Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Keep parked (STUCK). Funded seams stage (2026-10-10) ended by its stop rule: the seam alphabet is still growing at 1e10.

Read the full status

A lossless phase-tracked token extractor (verified against tools/sim.py) gives 513/783/1,028 distinct seam words at 1e8/1e9/1e10. Abstracted counts also grow: 449/662/844 with runs abstracted, and 182/226/270 elementary pieces. Collision types are 416/635/842. Deposits turn into u-runs through long (10)-runs (up to (10)^8429), and the result depends on residues and local context. No closed language was built. Pointing the other way: re-drawing run lengths in real cycle starts gives 0/1,200 halts. C reads 0 only at the blank left edge (33,051 of 33,051 cycles, never inside), so non-halting is equivalent to one invariant: D never steps left onto 0 0 inside the tape. Not flagged as cryptid; the epoch-level length map is not modelled. Optional next step in decision.json.

Observe

Deepen

Informal proof

Rocq

Overview

In one sentence

Bouncer over a 01001111 sea: quiet epochs (rule Q) validated; epoch changes are irregular and not closed yet.

Status: Parkedseams · updated 2026-10-12Not blocking · Stuck at the seams stage. Answer Q1–Q3 whenever; a “no” redirects the work.
idle since Oct 12 08:59 · status.json 2026-10-12
Class: Unknownours: sheet Unknown ≠ ours Fossil bouncer: one bounce per cycle over a sea of u = 01001111 with seams; the wall leaves 1-deposits that later fossilize · low confidence
On the list: line 578 of BB6_holdouts_663.txt · historical 740 line 644
eqv ×1table ×3sim 1e15

Your calls on file 5

priority call (answered): Fund one stage to map the seam words and test a closed tape language, or park W4-8 as STUCK at observe?
parked: Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Keep parked (STUCK).
funded: option: seams · date: 2026-10-11
2026-10-11 · seams: Fund one 2 h stage to map the seam words and test a closed tape language for this table, or park W4-8 as STUCK at observe? (Dennis: go with recommendations (2026-10-11))
decision.json · answered 2026-10-12: park: Keep W4-8 parked, or fund one 2 h native search for a closed tape language that only has to forbid 00 <B inside the tape? Decisions →

Mechanism

How it works: 3 notes

The tape is a sea of u = 01001111 (any rotation) with short seams. Each cycle the head sweeps right (RS: 20 steps per block), turns at a wall and sweeps back (LS: 40 per block); the left turn LT adds 3 cells.
Quiet epoch (rule Q): the left reservoir u^a gains a block, the wall eats one block of u^b and leaves 111 behind (1^c +3), and the active sea shifts +5 cells. 248 consecutive cycles from 9.5e7 to 1.1e8 match Q exactly.
Epochs end when b runs out or a seam (riding right at +5 cells per cycle) reaches the wall; the 1-deposit then fossilizes and at irregular cycles u^a freezes into a new segment (22 freezes to 2e9, a = 9 ... 2535). No closed epoch grammar yet.

Figures for Checkpoint A

Fig 1 · bbchallenge default view, first 10,000 stepsviewer ↗
The site's view. The left edge grows; the stripes are the 01001111 sea, rewritten on every pass.

Fig 2 · Segment map to 1e9 stepsQ1
One row per 10 cycles. Follow the green turning point; compare grey wedges with the dark fossil blocks.

Fig 3 · One cycle of the quiet-epoch rule QQ2
Rows are single steps. Find the turn near cell 196; check whether any cell right of it changes.

More figures (2)Fig 4–5: Segment map to 2e7 steps, every cycle · Segment map to 1e10, right part

Rules (6/6 validated)exact tape rewrites the proof will formalize, each re-checked by simulation

rule	from ⟶ to	cases	steps	checked
RS right sweep	111 A> (01001111)ⁿ ⟶ 111 (01110111)ⁿ A>	any left and right context (random words up to 12 cells), n = 0..40	20n	✓80/80
LS left sweep	(01110111)ⁿ 0 <B ⟶ 0 <B (01001111)ⁿ	any context. RS leaves the blocks in place as (0111)^2, which is 4-periodic, and LS reads them back 4 cells off, so a full pass moves the sea by -3 cells (= +5 mod 8); seams move +5 cells per cycle	40n	✓80/80
LT left turn	0^∞ <B ⟶ 0^∞ 111 A>	any right context; the left edge gains 3 cells per cycle	5	✓80/80
RO ones	A> 1ⁿ ⟶ 1ⁿ A>	A1 = 1RA; any context	n	✓80/80
Q quiet epoch	0^∞ <C (10100111)^a 1 (110100)² 1⁶ (10100111)^d (010011111)² (11010011)^e (10100111)² 0100 1¹⁰ (01001111)^b 1 (10100)² 1^c (10100111111)² (10100111)^f 0100 1⁵ 0^∞ ⟶ same with a+1, b-1, c+3	a, b, c, d, e, f >= 1 independent (random a <= 60, b <= 40, c <= 120, d <= 40, e <= 30, f <= 40); c and f are never read. Also 247/247 consecutive cycles from blank, 9.49e7..1.10e8 (d = 751, e = 23, f = 198), ending at b = 0	60(a+b+d+e)+595	✓80/80
H halting pattern	11 0 <C ⟶ halt	the only halt: F1 is undefined, F is entered only by E1 (0LF), and E reads a 1 with a 1 to its left only after C0 (1LE). So the machine halts iff C reads 0 with 11 on its left	3	✓40/40

Compressed historythe tape as 0^∞ <C (10100111)^a 1 (110100)² 1⁶ (10100111)⁷⁵¹ (010011111)² (11010011)²³ (10100111)² 0100 1¹⁰ (01001111)^b 1 (10100)² 1^c (10100111111)² (10100111)¹⁹⁸ 0100 1⁵ 0^∞ at 32 moments: where the rules are read off

0^∞ <C (10100111)^a 1 (110100)² 1⁶ (10100111)⁷⁵¹ (010011111)² (11010011)²³ (10100111)² 0100 1¹⁰ (01001111)^b 1 (10100)² 1^c (10100111111)² (10100111)¹⁹⁸ 0100 1⁵ 0^∞

step	`a`	`b`	`c`
94,875,591	9	247	2
95,374,751	17	239	26
95,873,911	25	231	50
96,373,071	33	223	74
96,872,231	41	215	98
97,371,391	49	207	122
97,870,551	57	199	146
98,369,711	65	191	170
98,868,871	73	183	194
99,368,031	81	175	218
99,867,191	89	167	242
100,366,351	97	159	266
100,865,511	105	151	290
101,364,671	113	143	314
101,863,831	121	135	338
102,362,991	129	127	362
102,862,151	137	119	386
103,361,311	145	111	410
103,860,471	153	103	434
104,359,631	161	95	458
104,858,791	169	87	482
105,357,951	177	79	506
105,857,111	185	71	530
106,356,271	193	63	554
106,855,431	201	55	578
107,354,591	209	47	602
107,853,751	217	39	626
108,352,911	225	31	650
108,852,071	233	23	674
109,351,231	241	15	698
109,850,391	249	7	722
110,287,156	256	0	743

alast 256

blast 0

clast 743

Template comparisonBouncer_v2.v TM1: does not apply · the nearest solved proof, what carries over, and the transitions that differ

	0	1
A	1RB	1RA
B	1LC	0RE
C	1LE	0LD
D	0LB	1LB
E	1RA	0LF
F	1LD	---

file: Bouncer_v2.v:9
module: TM1
machine: 1RB0LB_1RC0LC_1LD1RF_---1LE_0RC1LA_0RB1RA (11 transitions apart)
diff: —
note: No proved neighbour within 3 transitions (any start); Bouncer_v2 is the nearest proof by class. It proves S1 n -> S1 (1+n) with one es' call after 4,760,139 steps: the tape becomes a fixed word list with two blocks repeated 1+n times. Ours never settles into one S1: seams and fossil segments keep appearing (22 freezes to 2e9). Q is the analogue of BigStep only inside one epoch.

Proof strategy & riskshow the formal proof will go · 3 risks to watch

Collect the seam words and their collisions (seam meets wall, b = 0, freeze), then look for a tape language (u-runs separated by seams from a finite set) that one cycle maps into itself and that excludes 11 0 <C. Prove it CTL-style, with RS/LS/Q as the inside-epoch lemmas.

▲The seam set may be infinite: distinct seam words between u-runs keep growing (170 at 1e6, 526 at 1e8, 800 at 1e9, 829 at 2e9; crude count).
▲Freeze sizes look irregular (9, 20, 12, 41, ... 2483, 29, 2535); if they come from arithmetic on reservoir sizes, this is cryptid-like.
▲61 and 704 share the table and the u-sea but run different orbits; one proof covers them only if it is a language-closure proof.

Stats & provenance2·10⁹ steps simulated · 31,819 cells · the status in full · files

simulated: 2·10⁹ steps
tape: 31,819 cells · 22,003 nonzeros
growth: left edge ~ t^0.5 (lo = -30659 at 1e9, -43525 at 1.9e9); right edge grows only in bursts (hi = 1159 at 1e9, 1219 at 1.9e9); no halt to 2e9
status now: Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Keep parked (STUCK). Funded seams stage (2026-10-10) ended by its stop rule: the seam alphabet is still growing at 1e10. A lossless phase-tracked token extractor (verified against tools/sim.py) gives 513/783/1,028 distinct seam words at 1e8/1e9/1e10. Abstracted counts also grow: 449/662/844 with runs abstracted, and 182/226/270 elementary pieces. Collision types are 416/635/842. Deposits turn into u-runs through long (10)-runs (up to (10)^8429), and the result depends on residues and local context. No closed language was built. Pointing the other way: re-drawing run lengths in real cycle starts gives 0/1,200 halts. C reads 0 only at the blank left edge (33,051 of 33,051 cycles, never inside), so non-halting is equivalent to one invariant: D never steps left onto 0 0 inside the tape. Not flagged as cryptid; the epoch-level length map is not modelled. Optional next step in decision.json. (status.json, 2026-10-12)
observer's note: Observe done at low confidence: quiet-epoch rule Q and the sweep rules are validated, but the epoch changes (seams meeting the wall, reservoir freezes) are not understood, so there is no non-halting argument yet.
files: observe.json · notes.md · status.json

Proof & checks

No proof work yet.

Files

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

name	size	changed
notes.md ↓	14 KB	2026-10-12 08:59
status.json ↓	1.8 KB	2026-10-12 08:59
observe.json ↓	13 KB	2026-10-11 08:33
deepen.json ↓	3.3 KB	2026-10-11 08:35
decision.json ↓	2.5 KB	2026-10-12 08:59
decisions/	1 item	2026-10-11 08:36
img/	6 items	2026-10-11 08:33
scripts/	15 items	2026-10-11 08:34
work/	23 items	2026-10-11 08:35

status.json in full

{
 "tm": "1RB1RA_1LC0RE_1LE0LD_0LB1LB_1RA0LF_1LD---",
 "label": "W4-8",
 "status": "STUCK",
 "stage": "seams",
 "confidence": "low",
 "updated": "2026-10-12",
 "reason": "Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Keep parked (STUCK). Funded seams stage (2026-10-10) ended by its stop rule: the seam alphabet is still growing at 1e10. A lossless phase-tracked token extractor (verified against tools/sim.py) gives 513/783/1,028 distinct seam words at 1e8/1e9/1e10. Abstracted counts also grow: 449/662/844 with runs abstracted, and 182/226/270 elementary pieces. Collision types are 416/635/842. Deposits turn into u-runs through long (10)-runs (up to (10)^8429), and the result depends on residues and local context. No closed language was built. Pointing the other way: re-drawing run lengths in real cycle starts gives 0/1,200 halts. C reads 0 only at the blank left edge (33,051 of 33,051 cycles, never inside), so non-halting is equivalent to one invariant: D never steps left onto 0 0 inside the tape. Not flagged as cryptid; the epoch-level length map is not modelled. Optional next step in decision.json.",
 "family_note": "Same table (canon, all 6 starts): 61 1RB0LF_1RC1RB_1LD0RA_1LA0LE_0LC1LC_1LE--- is this table started in E, and 704 1RB---_0RC1RC_1RD0LE_1RE0RB_1LF0RA_1LC1LF is it started in F (mirrored). Both build the same 01001111 sea and seams (no halt to 1e9) but run different orbits. Starts C and D are not on the lists; the start-B table is Eqv_v2 TM2046's tm, proved equivalent to 61 (an equivalence, not a decision).",
 "priority_call_answered": "Fund one stage to map the seam words and test a closed tape language, or park W4-8 as STUCK at observe?",
 "funded": {
  "option": "seams",
  "date": "2026-10-11"
 },
 "parked": "Parked 2026-10-12 (Dennis: apply recommendations (2026-10-12)): Keep parked (STUCK)."
}

observe.json contract (tools/README-card.md):

1 contract warning

rank: missing

Rendered 2026-10-16 13:29 by tools/machinepage.py from status.json, observe.json (the card) and the dashboard records · rebuild: python3 -B tools/card.py 1RB1RA_1LC0RE_1LE0LD_0LB1LB_1RA0LF_1LD---