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-5

`1RB0LF_1RC0LB_1RD1RB_1RE1RF_1LA---_0RC1LA`

W4-5ParkedCounter Class 2bbchallenge ↗Explorer

Where it stands

Parked at the deeper analysis

Parked after the funded inv_search stage (2026-10-11), as its exit rule says. Covers holdouts 469 (start A) and 599 (start D).

Read the full status

No inductive invariant found. Precise obstruction: splice the closed-block stacks of two reachable E-events at a common window, keeping one's head and window, and the TM halts. This happens for windows of 1-4 exact blocks, 1-5 when both stacks are spliced, and 1-7 with blocks read as exact below 8, else mod 4. 45/45 halting splices were confirmed by direct simulation (halts at steps 2,595-279,060); right-side splices never halt (0/560). So no product n-gram/CPS invariant with such windows exists, under any value abstraction; all 173 macro-level closure settings fail accordingly. The defect surfaces 47-6,628 macro steps after the head reaches the splice. A global parity GP (0 at all 6e6 sampled E-events) explains 24/45 halting splices; the rest need more global information. TM-level CTL: 300 settings false. The mechanism is still exact: macro model 34.5M/34.5M E-events, no halt to 1e11. Resume only with coupled left/right automata, a non-regular invariant, or a compiled closure with exact windows of 6+ on both sides.

Observe

Deepen

Informal proof

Rocq

Overview

In one sentence

Blocks left of the head, pairs right of it; exact macro rules; halting needs an even zero run; parity holds, proof open.

Status: Parkedinv search · updated 2026-10-11Not blocking · Stuck at the inv search stage. Answer Q1–Q3 whenever; a “no” redirects the work.
idle since Oct 11 09:06 · status.json 2026-10-11
Class: Counter Class 2ours: sheet Counter Class 2 ≠ ours two-zone block/pair shuffler (chaotic two-stack list machine), not a counter · med confidence
On the list: line 426 of BB6_holdouts_663.txt · historical 740 line 469 · observe.json rank #469
eqv ×4table ×2sim 1e13

Your calls on file 3

priority call (answered): Fund one ~2 h stage to search for an inductive context invariant over the macro model (covers 469 and 599), or park both?
funded: option: inv_search · date: 2026-10-11
2026-10-11 · inv_search: W4-5 (469) and its same-table sibling 599 have an exact macro model where halting needs one parity defect: fund one ~2 h stage to search for an inductive context invariant, or park both? (Dennis: go with recommendations (2026-10-11))

Mechanism

How it works: 3 notes

Two zones split at the head: left = 1-blocks split by single 0s, right = (10)-pairs split by zero runs (plus a rare lone 1). A/F sweeps left turn a block into pairs; B/C passes right turn pairs into blocks. E-event K(L; a; r; R) = L 1^a E> 0^r R.
Exact rules (12,000/12,000 random, all 34.5M E-events from blank to 1e9): even a -> Ee eats the last two closed blocks y, b: K(L; y+3; b+1; (10)^(a/2) 0^(r-2) R). Odd a -> Eo closes a block 2, then a C-pass turns pairs into blocks until a run 0^n, n >= 3 (a = x+2, r = n-2) or a lone 1 (a = y+3, r = x+1). The block list is shuffled chaotically.
Halting needs a C-pass to meet exactly 0^2. Closed blocks stay even and zero runs odd (1.7M E-events to 5e7), and every rule keeps this, but only under side conditions (no lone pair before a run; a = 2 only at the edge) that are not yet shown inductive.

Figures for Checkpoint A

Fig 1 · First 10,000 steps (site view)
The site's own picture. The head zigzags inside the tape; the right edge advances in small steps.

Fig 2 · Sweeps at the block/pair interfaceQ1
Left of the zigzag: solid 1-blocks. Right: fine (10) stripes and black zero runs. Compare both sides of each turn.

Fig 3 · One row per E bounce (macro step)Q2
Each row is one E-event of the model. Follow the red head: rows drifting left, then jumps right.

More figures (3)Fig 4–6: Records view to 2e9 · Long run to 1e9 (sampled) · Spliced block stack halts at step 2,595

Fig 6 · Spliced block stack halts at step 2,595
Both halves occur on the real run; the bottom row is the halt. Compare the left zigzag with Fig 2.

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

rule	from ⟶ to	cases	steps	checked
Ee (even head block, a = 2k)	L 1^y 0 1^b 0 1^2k E> 0^r R ⟶ L 1^y+3 E> 0^b+1 (10)^k 0^r-2 R	k >= 1, r >= 3. r = 1: tail (10)^(k-1) 1 R (creates a lone 1). r = inf: tail (10)^k 0^inf. Missing y, b count as 0 (left edge: a' = 3, r' = 1, tape grows left by 1).	a + b + 7	✓6398/6398
Eo (odd head block, a = 2k+1)	L 1^2k+1 E> 0^r R ⟶ L 1² 0 C> (10)^k 0^r-2 R (then the C-pass)	r = 1: L 1^2 0 C> (10)^(k-1) 1 R. r = inf: L 1^2 0 C> (10)^k 0^inf.	a + 4 + C-pass	✓5289/5289
C1-C2 (C-pass over pairs)	1^x C> (10)^j Q \| 1^x C> 0 (10)^j Q ⟶ 1^x+2j C> Q \| 1^x+2 0 1^2j-2 C> Q	C2 closes the block x+2 at a single 0; needs j >= 1 after it (always so).	2j \| 2j + 1	✓5289/5289
C3 (C-pass meets 0^n, n >= 3 or inf)	L 1^x C> 0ⁿ Q ⟶ K(L; x+2; n-2; Q) = L 1^x+2 E> 0^n-2 Q	n = 3 gives r = 1; n = inf is the right edge (right record, +4 cells).	2	✓4364/4364
C4 (C-pass meets a lone 1)	L 1^y 0 1^x C> 1 (10)^j Q ⟶ L 1^y+3 E> 0^x+1 (10)^j-1 Q	A zero run at the front of (10)^(j-1) Q merges into r. A missing y counts as 0.	x + 5	✓925/925
H (halting pattern)	1^x C> 0 0 1 ⟶ halt: C, D write 1, E reads 1	The only way E reads 1. It needs an even zero run of length 2 after a pair, which INV excludes.	3	✓313/313

Compressed historythe tape as right-edge E-events (r = inf, R empty): 0^∞ 1^b1 0 1^b2 0 ... 0 1^bp 0 1^a E> 0^∞ at 40 moments: where the rules are read off

right-edge E-events (r = inf, R empty): 0^∞ 1^b1 0 1^b2 0 ... 0 1^bp 0 1^a E> 0^∞

step	`p (closed blocks)`	`a (head block)`	`span (cells)`	`closed blocks = 0 mod 4`
4	0	4	5	0
195	3	4	21	1
912	4	10	34	1
2,182	5	8	51	1
5,934	7	4	65	1
15,754	8	2	82	1
28,563	8	16	94	0
41,765	9	16	111	1
64,855	9	14	123	0
190,061	14	8	144	2
279,077	15	2	157	0
437,383	16	2	174	1
581,748	15	10	185	0
1,034,022	17	6	203	0
1,481,322	17	6	215	0
2,339,126	19	6	229	0
2,748,634	22	4	248	0
3,370,370	22	4	260	0
7,378,184	27	4	281	1
10,589,382	28	2	294	1
17,823,345	28	10	310	1
19,332,473	28	10	322	1
23,873,217	30	6	340	1
29,338,813	33	6	355	2
58,601,289	34	2	372	1
123,457,390	33	10	383	0
172,853,682	36	10	402	1
184,161,220	36	8	414	0
246,727,084	37	8	427	1
676,875,382	39	4	445	1
890,627,926	40	2	458	1
1,341,079,131	41	38	475	0
1,347,364,851	41	38	487	0
1,356,744,367	41	38	503	0
1,363,195,717	42	38	516	1
1,539,011,869	43	34	533	0
1,605,475,733	45	32	547	1
2,290,941,963	47	30	565	0
2,738,645,111	51	30	581	2
3,561,025,639	52	24	598	0

p (closed blocks)last 52

a (head block)last 24

span (cells)last 598

closed blocks = 0 mod 4last 0

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

	0	1
A	1RB	0LF
B	1RC	0LB
C	1RD	1RB
D	1RE	1RF
E	1LA	---
F	0RC	1LA

differs from the template

file: CounterClass2v1.v
module: —
machine: 1RB1RD_1LC---_1LE0LD_0RE1LC_1RA1RF_1RE0LF (11 transitions apart)
diff: 1 transition: our A0 = 1RB, template (in our names) A0 = 1LC; v2-v4 have 0LB there (v4 also E0 = 1LD)
note: All four proved neighbours differ exactly at A0, the turn that starts rule Ee. v1 is a deterministic counter on a fixed skeleton (SkelE n, Bnext on (n, j, b), ClosedCall, GoodB). Here the block list is a shuffled stack, so only the top-level shape (progress_nonhalt_cond + an invariant) carries over.

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

Find an inductive invariant over the validated macro model: closed blocks even, runs odd, plus local context conditions. Search it mechanically (regular/bigram closure over abstract tokens, or a TM-level CTL certificate). Then write rules Ee/Eo/C1-C4 as es/ind lemmas and close with progress_nonhalt_cond; one proof would cover 469 and 599 (start D).

▲The context conditions may not be local: simple versions fail random closure (~2% of steps), and 'r = 1 implies next group >= 3 pairs' fails on the real run at step 2,403,364.
▲Chaotic list dynamics: if no small invariant closes, a CTL certificate may be large; 85 small RWL_mod/NG settings returned false.
▲No template help: the proved neighbours differ exactly in the slot that drives rule Ee.

Stats & provenance10¹¹ steps simulated · 779 cells · the status in full · files

simulated: 10¹¹ steps
tape: 779 cells · 349 nonzeros
growth: span 462 at 1e9, 779 at 1e11 (about t^0.23); +4 cells per right record
status now: Parked after the funded inv_search stage (2026-10-11), as its exit rule says. Covers holdouts 469 (start A) and 599 (start D). No inductive invariant found. Precise obstruction: splice the closed-block stacks of two reachable E-events at a common window, keeping one's head and window, and the TM halts. This happens for windows of 1-4 exact blocks, 1-5 when both stacks are spliced, and 1-7 with blocks read as exact below 8, else mod 4. 45/45 halting splices were confirmed by direct simulation (halts at steps 2,595-279,060); right-side splices never halt (0/560). So no product n-gram/CPS invariant with such windows exists, under any value abstraction; all 173 macro-level closure settings fail accordingly. The defect surfaces 47-6,628 macro steps after the head reaches the splice. A global parity GP (0 at all 6e6 sampled E-events) explains 24/45 halting splices; the rest need more global information. TM-level CTL: 300 settings false. The mechanism is still exact: macro model 34.5M/34.5M E-events, no halt to 1e11. Resume only with coupled left/right automata, a non-regular invariant, or a compiled closure with exact windows of 6+ on both sides. (status.json, 2026-10-11)
observer's note: Observe done at med confidence: exact macro model (34.5M/34.5M E-events from blank to 1e9, 12,000 random), halting reduced to one parity pattern; inductive invariant open.
files: observe.json · notes.md · status.json

Proof & checks

No proof work yet.

Files

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

name	size	changed
notes.md ↓	15 KB	2026-10-11 09:06
status.json ↓	1.9 KB	2026-10-11 09:06
observe.json ↓	13 KB	2026-10-11 09:00
deepen.json ↓	7.2 KB	2026-10-11 09:06
decisions/	1 item	2026-10-11 09:03
img/	6 items	2026-10-11 08:55
scripts/	27 items	2026-10-11 08:53

status.json in full

{
 "tm": "1RB0LF_1RC0LB_1RD1RB_1RE1RF_1LA---_0RC1LA",
 "label": "W4-5",
 "status": "STUCK",
 "stage": "inv_search",
 "updated": "2026-10-11",
 "confidence": "med",
 "reason": "Parked after the funded inv_search stage (2026-10-11), as its exit rule says. Covers holdouts 469 (start A) and 599 (start D). No inductive invariant found. Precise obstruction: splice the closed-block stacks of two reachable E-events at a common window, keeping one's head and window, and the TM halts. This happens for windows of 1-4 exact blocks, 1-5 when both stacks are spliced, and 1-7 with blocks read as exact below 8, else mod 4. 45/45 halting splices were confirmed by direct simulation (halts at steps 2,595-279,060); right-side splices never halt (0/560). So no product n-gram/CPS invariant with such windows exists, under any value abstraction; all 173 macro-level closure settings fail accordingly. The defect surfaces 47-6,628 macro steps after the head reaches the splice. A global parity GP (0 at all 6e6 sampled E-events) explains 24/45 halting splices; the rest need more global information. TM-level CTL: 300 settings false. The mechanism is still exact: macro model 34.5M/34.5M E-events, no halt to 1e11. Resume only with coupled left/right automata, a non-regular invariant, or a compiled closure with exact windows of 6+ on both sides.",
 "relation": "one table, two holdout starts: A = 469 (this), D = 599",
 "siblings": [
  "1RB1RD_1LC---_1RF0LD_0RE1LC_1RA1RF_1RE0LF"
 ],
 "holdout_line_740": 469,
 "existing_work": "none found: sheet Results row is class Counter Class 2 only (no status/notes/done-by); Direct Simulation tab lists it as not simulated to 1e14/1e15; no Discord hit; upstream has only the Eqv_v3 TM540 / Eqv_v2 TM359 equivalences to other unproved tables.",
 "priority_call_answered": "Fund one ~2 h stage to search for an inductive context invariant over the macro model (covers 469 and 599), or park both?",
 "funded": {
  "option": "inv_search",
  "date": "2026-10-11"
 }
}

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

1 contract warning

diagrams: 6 (want 3-5)

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 1RB0LF_1RC0LB_1RD1RB_1RE1RF_1LA---_0RC1LA