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 / W6-4

`1RB0LE_1RC1RB_1LD0RE_1LA1LC_1RB0LF_0LC---`

W6-4ParkedChaotic Bell Class 1bbchallenge ↗Explorer

Where it stands

Parked at the observation

Observe + halting go/no-go done (about 1 h 20 min). The machine is ChaoticBell1Halt.v TM13's table renamed (ours A,B,C,D,E,F = TM13 D,A,B,C,E,F, no mirror), started in TM13's D; all TM13 lemmas hold verbatim (26 rules + the halt window validated 40/40 each from random instances).

Read the full status

An untrusted Python port of ccz181078's certified executor CBSim reproduces the upstream halts exactly (TM13 at tick 64,832, TM7 at 65,400) and matches direct simulation for 4,000 ticks (21,071,295 steps). From our start it runs 16,551,000 ticks (165x ccz181078's 100,000) with no halt; the same table from 602's start runs 10,000,000 ticks and from 299's start 7,627,000 ticks, no halt. NO-GO for the HALT route at this budget; no nonhalting attempt (plan). New: after ~4e5 ticks every run enters a regular phase, a left stack of PL(n)^k_n (n = 0..~80, k ~1e31) whose counts fall ~5x per two levels with small remainders (k_n - 5 k_(n+2) in -89..178); the executor eats it from the near end at ~1 level per 3e6 ticks.

Observe

Deepen

Informal proof

Rocq

Overview

In one sentence

TM13's table (ChaoticBell1Halt.v) from TM13's D: CB1 bell; certified-executor port finds no halt in 16.5M ticks.

Status: Parkedobserving · updated 2026-10-14Not blocking · Stuck at the observing stage. Answer Q1–Q3 whenever; a “no” redirects the work.
idle since Oct 14 16:43 (44 h ago) · status.json 2026-10-14
Class: Chaotic Bell Class 1ours: Chaotic Bell Class 1 (sheet) · ours adds: ChaoticBell1Halt.v TM13's table (renamed), started in TM13's D · med confidence
On the list: line 373 of BB6_holdouts_663.txt · historical 740 line 412 · observe.json rank #412
eqv ×2table ×3sim 1e13

Your calls on file 3

priority call (answered): No halt in 16.5M executor ticks. Park the CB1 cluster (412, 602, 299), or fund one 2 h stage for an exact level accelerator of the late PL stack (cryptid stop if the per-level map branches on remainders mod 5)?
parked: Dennis 2026-10-14: park
2026-10-14 · park: W6-4's halting go/no-go found no halt at 165x upstream's budget: park the CB1 cluster (412, 602, 299), or fund one 2 h stage?

Mechanism

How it works: 3 notes

Same table as ChaoticBell1Halt.v TM13 (ours A,B,C,D,E,F = TM13 D,A,B,C,E,F; no mirror): our blank start is TM13 started in D. All TM13 lemmas hold verbatim; 26 rules + the halt window pass 40/40 random instances here.
A bell over digits D n = 1^(2n+1) 00: B> 0100 sweeps right (D n -> S n = 1(01)^(n+1)), <C 1 sweeps back. Each 111 on the left is one call (sweep to the right end, append 100 100); PL blocks replay calls; the far left turns the head (over1/over2). Direct sim: no halt to 1e9 (sheet: 1e13); left-end tapes are clean D-digit lists.
Port of ccz181078's certified executor (CBSim): reproduces TM13's halt (tick 64,832) and TM7's (65,400), matches direct sim for 4,000 ticks (21.1M steps). Our start: no halt in 16,551,000 ticks; 602's start: none in 10,000,000; 299's: none in 7,627,000. After ~4e5 ticks the run turns regular: a stack of PL(n)^k_n, n = 0,1,2,..., counts ~1e31 falling ~5x per two levels, small remainders.

Figures for Checkpoint A

Fig 1 · bbchallenge Default view, 10,000 stepsviewer ↗
Orientation: the head sweeps the whole tape; the right edge moves out a little per sweep.

Fig 2 · Every 10^6 steps up to 10^9Q2
Rows are snapshots 10^6 steps apart. Compare the fixed left edge with the right edge.

Fig 3 · Close-up: two calls from a constructed tapeQ1
Start: two 111 groups left of the head. Follow each sweep to the right end and back.

More figures (1)Fig 4: Explore view: the first 50 steps

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

rule	from ⟶ to	cases	steps	checked
moveR	l B> 0100 1²ⁿ⁺¹ 00 r ⟶ l 1(01)ⁿ⁺¹ B> 0100 r	all parameters >= 0, any l, r	—	✓40/40
moveL	l 1(01)ⁿ⁺¹ <C 1 r ⟶ l <C 1 1²ⁿ⁺¹ 00 r	all parameters >= 0, any l, r	—	✓40/40
emptyR	l B> 0100 0^∞ ⟶ l <C 1 100 100 0^∞	right context is 0^inf	—	✓40/40
blank	l B> 0100 000 r ⟶ l <C 1 100 100 r	all parameters >= 0, any l, r	—	✓40/40
restartL	l 111 (01)^b+1 <C 1 r ⟶ l (01)^b+1 B> 0100 r	all parameters >= 0, any l, r	—	✓40/40
moveJ	l 1(01)ⁿ⁺¹ <D 100 r ⟶ l <C 1 1²ⁿ⁺³ 00 r	all parameters >= 0, any l, r	—	✓40/40
restartJ	l 111 (01)^b <D 100 r ⟶ l (01)^b+1 B> 0100 r	all parameters >= 0, any l, r	—	✓40/40
finishPL	l 101 10 (01)^b+1 <C 1 r ⟶ l <D 100 1^2b+3 00 r	all parameters >= 0, any l, r	—	✓40/40
collide	l B> 0100 10 100 100 r ⟶ l <D 100 11111 00 10 r	all parameters >= 0, any l, r	—	✓40/40
pairR	l B> 0100 10 (1²ⁿ⁺⁵ 00)² r ⟶ l 101 101 1²ⁿ (01)ⁿ⁺⁴ B> 0100 10 r	all parameters >= 0, any l, r	—	✓40/40
even	l B> 0100 1²ⁿ⁺² 00 r ⟶ l <C 1 1²ⁿ⁺³ 00 10 r	all parameters >= 0, any l, r	—	✓40/40
over2	0^∞ 11 (01)^b+1 <C 1 r ⟶ 0^∞ 1^2b+2 0101 B> 0100 1 r	left context is 0^inf; b >= 0	—	✓40/40
over1	0^∞ 1 (01)^b+1 <C 1 1²ⁿ⁺¹ 00 r ⟶ 0^∞ 1^2b (01)ⁿ⁺² B> 0100 10 r	left context is 0^inf (far left end); b, n >= 0	—	✓40/40
collision	l 101100 <C 1 r ⟶ l <D 100 1111 r	all parameters >= 0, any l, r	—	✓40/40
turnB	l 11 <C 1 1²ⁿ⁺¹ 00 r ⟶ l (01)ⁿ⁺¹ B> 0100 r	all parameters >= 0, any l, r	—	✓40/40
defect0	l B> 0100 10 100 1 1^2m 0 r ⟶ l <D 100 1111 1^2m+1 00 1 r	all parameters >= 0, any l, r	—	✓40/40
defect1	l B> 0100 10 11100 1 1^2m 0 r ⟶ l <C 1 100 100 1^2m+3 00 1 r	all parameters >= 0, any l, r	—	✓40/40
defect2	l B> 0100 10 1²ⁿ⁺⁵ 00 1 1^2m 0 r ⟶ l 101 101 1²ⁿ (01)^m+2 B> 0100 1 r	all parameters >= 0, any l, r	—	✓40/40
defectBlank0	l B> 0100 10 100 00 r ⟶ l 101 1001 B> 0100 r	all parameters >= 0, any l, r	—	✓40/40
defectBlankS	l B> 0100 10 1²ⁿ⁺³ 00 00 r ⟶ l 101 101 1 1²ⁿ 01 B> 0100 r	all parameters >= 0, any l, r	—	✓40/40
paired	l B> 0100 (10)^2k 1²ⁿ⁺¹ 00 r ⟶ l 101 (1011)^k (01)ⁿ B> 0100 r	k >= 1, n >= 0	—	✓40/40
calls	l (111)^h (01)^b+1 <C 1 D(v1)..D(vk) 0^∞ ⟶ l (01)^b+1 <C 1 D(v1)..D(vk) (100)^2h 0^∞	h >= 1, b >= 0, any digit list; right context 0^inf	—	✓40/40
scanR	l B> 01 (11)^k r ⟶ l (01)^k B> 01 r	all parameters >= 0, any l, r	—	✓40/40
scanB	l (10)^k <C r ⟶ l <C (11)^k r	all parameters >= 0, any l, r	—	✓40/40
scanC	l (01)^k <D r ⟶ l <D (11)^k r	all parameters >= 0, any l, r	—	✓40/40
scanPair	l B> 01 (0101)^k r ⟶ l (1011)^k B> 01 r	all parameters >= 0, any l, r	—	✓40/40
halt_window	l 11100 <C r halts (C reads 0 ⟶ 1LD, ..., F reads 1 = ---)	any l, r	—	✓40/40
executor = machine	blank, our A (= TM13 from D) ⟶ each of the first 4,000 executor configurations, in order	Python port of CBSim; exact tape match at every tick	21,071,295 direct steps	✓4000/4000

Compressed historythe tape as left-end visits (direct sim): 0^∞ <X D(n1) D(n2) ... D(nk) 0^∞, D n = 1²ⁿ⁺¹ 00 at 30 moments: where the rules are read off

left-end visits (direct sim): 0^∞ <X D(n1) D(n2) ... D(nk) 0^∞, D n = 1²ⁿ⁺¹ 00

step	`span`	`digits k`	`max digit`	`non-digit 1-runs`
7	4	1	0	0
8,344	144	39	10	0
15,406	172	24	3	0
25,504	225	24	9	1
61,044	341	48	17	0
91,570	406	67	10	0
172,077	523	52	12	0
292,222	700	93	14	0
325,715	764	115	13	0
416,080	805	74	19	1
881,676	1,246	209	15	0
1,424,555	1,566	255	16	0
2,161,493	1,914	293	20	0
3,572,559	2,456	399	18	1
5,520,918	3,076	517	22	0
6,836,134	3,165	305	21	0
10,850,073	3,973	392	21	1
11,038,753	4,040	415	21	1
17,619,623	5,055	524	21	0
35,574,720	7,527	1,140	24	1
56,207,068	9,427	1,432	24	0
69,081,798	9,852	983	26	0
109,402,360	12,356	1,255	26	0
170,969,389	15,487	1,608	27	0
218,840,414	18,501	2,810	26	0
220,347,775	18,594	2,855	32	0
344,466,415	23,308	3,611	24	0
537,353,468	29,125	4,510	29	0
1,032,545,059	37,732	3,707	28	1
1,613,253,747	47,146	4,609	33	0

spanlast 47,146

digits klast 4,609

max digitlast 33

non-digit 1-runslast 0

Template comparisonChaoticBell1Halt.v TM13: partly applies · the nearest solved proof, what carries over, and the transitions that differ

	0	1
A	1RB	0LE
B	1RC	1RB
C	1LD	0RE
D	1LA	1LC
E	1RB	0LF
F	0LC	---

file: ChaoticBell1Halt.v ⚠ not at pin
module: TM13
machine: 1RB1RA_1LC0RE_1LD1LB_1RA0LE_1RA0LF_0LB--- (8 transitions apart)
diff: same table renamed (ours A,B,C,D,E,F = TM13 D,A,B,C,E,F; no mirror); only the start differs (ours = TM13 from D)
note: All TM13 lemmas (scan*, right, left, blank, even, restart, overflow1/2, collision, leftJ, turnB, turnJ, finishP, defect*, paired, halt_window, core) are about the table only and hold here after renaming B->A, C->B, D->C. A HALT .v = the CB1/CBMacros/CBSim modules with the state letters renamed, our TM string, check_spec with fuel above the halting tick. That needs a halt, which the port did not find.

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

HALT route by the certified executor: no halt in 16.5M ticks (165x). If funded: an exact per-level map for the late PL stack, iterated to the bottom (~80 levels, ~2e8 ticks); cryptid stop on residue branching.

▲ccz181078 very likely ran the same executor on the whole class and kept only TM7/TM13; our 100x+ runs agree that these starts do not halt early.
▲The late phase looks like division by 5 with small remainders: a cryptid sign; a fitted law may branch on residues.
▲The Python port only predicts; a kill would still need the Coq check_spec run (one coqc) after a halt.

Stats & provenance2·10⁹ steps simulated · 47,146 cells · the status in full · files

simulated: 2·10⁹ steps
tape: 47,146 cells · 22,051 nonzeros
growth: direct: span ~ sqrt(steps) (37,750 at 1.03e9; 47,146 at 1.6e9). Executor: 10^31 cells at 4.2e5 ticks, then ~10^33 to 1.65e7 ticks; the PL stack is eaten ~1 level per 3e6 ticks
status now: Observe + halting go/no-go done (about 1 h 20 min). The machine is ChaoticBell1Halt.v TM13's table renamed (ours A,B,C,D,E,F = TM13 D,A,B,C,E,F, no mirror), started in TM13's D; all TM13 lemmas hold verbatim (26 rules + the halt window validated 40/40 each from random instances). An untrusted Python port of ccz181078's certified executor CBSim reproduces the upstream halts exactly (TM13 at tick 64,832, TM7 at 65,400) and matches direct simulation for 4,000 ticks (21,071,295 steps). From our start it runs 16,551,000 ticks (165x ccz181078's 100,000) with no halt; the same table from 602's start runs 10,000,000 ticks and from 299's start 7,627,000 ticks, no halt. NO-GO for the HALT route at this budget; no nonhalting attempt (plan). New: after ~4e5 ticks every run enters a regular phase, a left stack of PL(n)^k_n (n = 0..~80, k ~1e31) whose counts fall ~5x per two levels with small remainders (k_n - 5 k_(n+2) in -89..178); the executor eats it from the near end at ~1 level per 3e6 ticks. (status.json, 2026-10-14)
observer's note: Rules exact (26/26 validated). Halting go/no-go: NO-GO, the certified-executor port finds no halt in 16,551,000 ticks from our start (602's start: 1e7; 299's: 7,627,000). Nonhalting not attempted (plan); the late phase is a regular PL stack with a /5-with-remainder look.
files: observe.json · notes.md · status.json

Proof & checks

No proof work yet.

Files

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

name	size	changed
notes.md ↓	12 KB	2026-10-14 15:10
status.json ↓	3.1 KB	2026-10-14 16:43
observe.json ↓	17 KB	2026-10-14 15:10
decisions/	1 item	2026-10-14 16:43
img/	5 items	2026-10-14 14:06
work/	33 items	2026-10-14 15:09

status.json in full

{
 "tm": "1RB0LE_1RC1RB_1LD0RE_1LA1LC_1RB0LF_0LC---",
 "label": "W6-4",
 "status": "STUCK",
 "stage": "observe",
 "updated": "2026-10-14",
 "confidence": "med",
 "reason": "Observe + halting go/no-go done (about 1 h 20 min). The machine is ChaoticBell1Halt.v TM13's table renamed (ours A,B,C,D,E,F = TM13 D,A,B,C,E,F, no mirror), started in TM13's D; all TM13 lemmas hold verbatim (26 rules + the halt window validated 40/40 each from random instances). An untrusted Python port of ccz181078's certified executor CBSim reproduces the upstream halts exactly (TM13 at tick 64,832, TM7 at 65,400) and matches direct simulation for 4,000 ticks (21,071,295 steps). From our start it runs 16,551,000 ticks (165x ccz181078's 100,000) with no halt; the same table from 602's start runs 10,000,000 ticks and from 299's start 7,627,000 ticks, no halt. NO-GO for the HALT route at this budget; no nonhalting attempt (plan). New: after ~4e5 ticks every run enters a regular phase, a left stack of PL(n)^k_n (n = 0..~80, k ~1e31) whose counts fall ~5x per two levels with small remainders (k_n - 5 k_(n+2) in -89..178); the executor eats it from the near end at ~1 level per 3e6 ticks.",
 "siblings": [
  "1RB0LE_1RC1RA_1LD0RE_1LA1LD_1LD0RF_0RA---",
  "1RB1RD_1LC0RE_1LD1LC_1RA0LE_1LC0RF_0RD---"
 ],
 "sibling_note": "Same table (canon over all starts and the mirror): 299 = TM13 from B (mirrored), 602 = TM13 from C (mirrored); our start C and D give them. Our start B = TM13 itself (halts, upstream). eqv-1590 partner of 412: 1RB0LE_1RC1RB_1LD0RA_1LF1LC_0LC---_1RB0LA (= TM13 from E, not on the 740 list). 338, 577, 730 are not this table: their eqv members are TM7 from B, D (and F), C; cousins, not run here.",
 "holdout_line_740": 412,
 "upstream": "verify/ChaoticBell1Halt.v (ccz181078, busycoq BB6 HEAD cdaf693) proves TM13 and TM7 halting from A; 412 itself is in no upstream file. No claim in data/discord or data/sheet (results row: class only; direct-simulation sheet: run to 1e13 without a halt).",
 "template": "verify/ChaoticBell1Halt.v Module TM13 (+ CB1, CBMacros, CBSim): rules apply verbatim after renaming; only the start differs",
 "executor_runs": {
  "port": "work/cbsim_fast2.py (untrusted Python transcription of CBSim; checks: upstream halt ticks, 4,000-tick direct-sim match)",
  "TM13_from_D_412": {
   "ticks": 16551000,
   "halted": false,
   "tape_cells_log10": 33,
   "checkpoint": "work/ckpt_TM13_D.pkl"
  },
  "TM13_from_C_602": {
   "ticks": 10000000,
   "halted": false,
   "tape_cells_log10": 33,
   "checkpoint": null
  },
  "TM13_from_B_299": {
   "ticks": 7627000,
   "halted": false,
   "tape_cells_log10": 33,
   "checkpoint": "work/ckpt_TM13_B.pkl"
  },
  "TM13_from_A_check": {
   "ticks": 64832,
   "halted": true
  },
  "TM7_from_A_check": {
   "ticks": 65400,
   "halted": true
  }
 },
 "priority_call_answered": "No halt in 16.5M executor ticks. Park the CB1 cluster (412, 602, 299), or fund one 2 h stage for an exact level accelerator of the late PL stack (cryptid stop if the per-level map branches on remainders mod 5)?",
 "parked": "Dennis 2026-10-14: park"
}

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

1 contract warning

template file not in the pinned tree: ChaoticBell1Halt.v

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 1RB0LE_1RC1RB_1LD0RE_1LA1LC_1RB0LF_0LC---