BB(6) hunt
Machines / W5-6

1RB0LC_1LC0RE_1LA1LD_1LA1LB_0RF1RA_---0RE

W5-6Claimed elsewhereBell eats counterbbchallenge ↗Explorer

Upstream result

Claimed elsewhere

The blank-start machine never halts: BECv10.v.TM2 ↗. Recorded commit time: 2026-10-13T13:42:06Z. First public push time is not established.

Absent from the current 663 holdout list. Earlier local observations remain below.

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

Each bounce adds 1 to a binary counter and moves 3 bell cells to a middle field; each bell end eats a counter digit.

Upstream
The blank-start machine never halts: BECv10.v.TM2 ↗. Recorded commit time: 2026-10-13T13:42:06Z. First public push time is not established.
Status
Externally Solvedparked (funded stage3 ended at its stop rule) · updated 2026-10-13Not blocking · Stuck at the parked (funded stage3 ended at its stop rule) stage. Answer Q1–Q3 whenever; a “no” redirects the work.
idle since Oct 13 09:21 · status.json 2026-10-13
Class
Bell eats counterours: Bell eats counter (sheet) · ours adds: binary counter on 2-cell digits (10 = 1, 00 = 0) with junk separators, bitten once per bell · med confidence
On the list
not on BB6_holdouts_663.txt (line 88 of the previous list) · historical 740 line 88 · observe.json rank #88
eqv ×1sim 1e15
Your calls on file 3
funded
option: stage3 · date: 2026-10-13
next
Parked; no new decision (stop rule). Reopen only with a history-carrying invariant: state (w, k0, n, m), where m is the n at the last odd eat, and window n >= max(Phi+1, 2^(D-1)), m >= 2^dS for the fresh S. Untested; see notes.md, Funded stage (stage3).
2026-10-13 · stage3
Fund one more capped 2 h stage to turn the computed closed set into a closed-form invariant for W5-6 (which would also cover 280), or park both now? (Dennis 2026-10-13: 'go with recommendations')

Mechanism

How it works: 3 notes
  • Turn config R(u,e) = 0^inf u <C 0 1^e 0^inf, u = w 1 (101)^k (w counter, 1 separator, (101)^k middle field). Bounce: R(w 1 (101)^k, e+3) -> R(inc(w) 1 (101)^(k+1), e) in 6k+4t+9 steps (t = trailing 1-digits); exact on all 60,001 turns to 5.1e7.
  • Eat (e = r in {0,2}): z = inc(inc(w)); z = p 00 -> R(p 1, 3k+3+3[r=2]); z = q c 10 -> R(q 101, 3k+2+3[r=2]). Matches all 631 checked real eats (287 from A, 344 from the certified start B). So e mod 3 is always 0 or 2.
  • Start B (IndBECv1 cert) stays on the clean orbit R(enc(s) 1, 3s) -> R(enc(s+1) 1, 3s+3). Start A keeps leaving it: odd eats make 010 tails and lone-1 separators inside w (90 of 289 cycle starts to 5e7 are not clean); inc passes through separators; w never contains 1111, which every halting inc input up to length 13 but one has. 88 and 280 run the same orbit (identical tape at 1e9): 280's table equals 88's with state B split by entry; they diverge only if 88's F reads 0 or 88's B (entered by D1) reads 1, which are exactly the two halting reads.

Figures for Checkpoint A

Fig 1 · bbchallenge default view, first 10,000 steps

The site's view. Left edge: the counter. White triangles on the right: one bell each.

bbchallenge default view, first 10,000 steps
bbchallenge-defaultStart blankRows 10,000 steps squeezed into 500 px rowsWindow cells -200..199, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: 1 px row = 20 steps, the site's bilinear squeeze
Fig 2 · Every 300th step, first 300,000 stepsQ2

Each white triangle is one bell. Compare the triangle sizes going down, and watch the left edge.

Every 300th step, first 300,000 steps
bbchallenge-defaultStart blankRows every 300 stepsWindow cells -160..74, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: 1,001 rows, steps 0..300,000
Fig 3 · Counter at cycle starts: start A vs BQ1

One row per cycle (first right turn after an eat). Compare colours near each counter's right end in both panels.

Counter at cycle starts: start A vs B
customStart blankRows one per cycle startWindow cells 0..39, 1 px = 0.33 cellsColors 1 and black = 0 in the clean binary part of the counter 1 and maroon = 0 in the junk part separator 1 0 in the middle field gap between the panels
Rows: the last 150 cycles before step 5.1e7 (left: start A, steps 5,770,734..50,808,142; right: start B, steps 7,839,008..42,019,600), 3 px per row · Window: (3 px per cell), counted from the leftmost 1 of each row (it moves left 2-4 cells per cycle); left panel start A, right panel start B, slate gap between · Colors: white: digits 10/00; orange: from the first non-digit cell to the counter's end; middle field and bell
More figures (1)Fig 4: Left and right records to 1e8
Fig 4 · Left and right records to 1e8

One row per new leftmost or rightmost cell. The left edge grows about twice as fast as the right.

Left and right records to 1e8
bbchallenge-defaultStart blankRows left/right recordsWindow cells -1068..524, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: 1,593 rows, steps 0..1e8
Rules (7/7 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
R1 bounce (clean counter)
0∞ enc(v) 1 (101)k <C 0 1e+3 0∞
⟶ 0∞ enc(v+1) 1 (101)k+1 <C 0 1e 0∞
v>=1, k>=0, e>=0; enc(v) = v in binary, digit 1 = 10, digit 0 = 00; t = trailing 1-digits of v (overflow included); cross-checked with tools/sim.py on 20 more6k+4t+9✓200/200
R2 inc through a 110 separator
enc(a) 110 enc_d(b) 1 (101)k <C 0 1e+3
⟶ enc(a) 110 enc_d(b+1) ... if b+1 < 2d, else enc(a+1) 110 (00)d ...
enc_d = d digits with leading 00s; the separator is transparent to the carry—✓200/200
R3 inc through a lone 1 then 00
enc(a) 1 enc_d(b) 1 (101)k <C 0 1e+3
⟶ enc(a) 1 enc_d(b+1) 1 (101)k+1 <C 0 1e
b < 2^(d-1) (top digit 00); when the top digit becomes 10 the word is R2's form—✓200/200
R4 eat, clean counter
0∞ enc(v) 1 (101)k <C 0 1r 0∞
⟶ 0∞ w' <C 0 1e' 0∞, w' by the parity of v (see cases)
r in {0,2}; v=2m -> 0^inf enc(m+1) 1 <C 0 1^(3k+3+3[r=2]); v=2m+1, m+1 odd -> enc((m+1)//2) 1 101 <C 0 1^(3k+2+3[r=2]); v=2m+1, m+1 even -> enc((m+1)/2) 010 1 <C 0 1^(3k+2+3[r=2]) (010 tail = junk)—✓200/200
R5 eat, any counter word
0∞ w 1 (101)k <C 0 1r 0∞
⟶ z = inc(inc(w)): z = p 00 -> 0∞ p 1 <C 0 13k+3+3[r=2]; z = q c 10 -> 0∞ q 101 <C 0 13k+2+3[r=2]
r in {0,2}, k>=1; random words from the run; also exact on all 631 real eats (A and B)—✓200/200
R6 inc does not depend on k, e
0∞ w 1 (101)k <C 0 1e+3
⟶ 0∞ inc(w) 1 (101)k+1 <C 0 1e
2,000 distinct counter words from the run; random k, e pairs give the same inc(w)—✓200/200
R7 certified orbit (start B)
0∞ enc(s) 1 <C 0 13s 0∞
⟶ 0∞ enc(s+1) 1 <C 0 13s+3 0∞
s>=2; s bounces (R1) then one even eat (R4)—✓20/20
Compressed historythe tape as cycle start R(w 1 (101)k, e) after an eat (k = 0 or 1) at 40 moments: where the rules are read off
cycle start R(w 1 (101)k, e) after an eat (k = 0 or 1)
stepe (bell length)counter cells |w|clean counter (1) or junk (0)-lo (left edge)
272004
1,714396132
10,0716511054
28,1639610176
61,84312513096
113,367153121116
186,191179101132
282,524216121156
416,283245150178
586,100282121200
796,806306141218
1,047,457335150238
1,342,806360141254
1,684,524393141276
2,088,433422170298
2,553,088456141318
3,083,256483161338
3,673,633507141354
4,335,252539170378
5,079,378570161396
5,892,136597161414
6,791,028629170438
7,793,930669161462
8,900,098696161480
10,105,754729161502
11,415,984755200522
12,834,566789161542
14,368,231818170562
16,027,820851200586
17,829,276885181608
19,738,346912181626
21,764,234936181642
23,902,065968170662
26,202,2801,002161684
28,653,8451,034190708
31,274,0131,067161730
34,056,8831,100190752
37,005,9351,130190772
40,111,4371,158210792
43,354,6871,181161806
e (bell length)last 1,181
1,1812274.3e7log xstep 27: e (bell length) = 2step 1714: e (bell length) = 39step 10071: e (bell length) = 65step 28163: e (bell length) = 96step 61843: e (bell length) = 125step 113367: e (bell length) = 153step 186191: e (bell length) = 179step 282524: e (bell length) = 216step 416283: e (bell length) = 245step 586100: e (bell length) = 282step 796806: e (bell length) = 306step 1047457: e (bell length) = 335step 1342806: e (bell length) = 360step 1684524: e (bell length) = 393step 2088433: e (bell length) = 422step 2553088: e (bell length) = 456step 3083256: e (bell length) = 483step 3673633: e (bell length) = 507step 4335252: e (bell length) = 539step 5079378: e (bell length) = 570step 5892136: e (bell length) = 597step 6791028: e (bell length) = 629step 7793930: e (bell length) = 669step 8900098: e (bell length) = 696step 10105754: e (bell length) = 729step 11415984: e (bell length) = 755step 12834566: e (bell length) = 789step 14368231: e (bell length) = 818step 16027820: e (bell length) = 851step 17829276: e (bell length) = 885step 19738346: e (bell length) = 912step 21764234: e (bell length) = 936step 23902065: e (bell length) = 968step 26202280: e (bell length) = 1002step 28653845: e (bell length) = 1034step 31274013: e (bell length) = 1067step 34056883: e (bell length) = 1100step 37005935: e (bell length) = 1130step 40111437: e (bell length) = 1158step 43354687: e (bell length) = 1181
counter cells |w|last 16
210274.3e7log xstep 27: counter cells |w| = 0step 1714: counter cells |w| = 6step 10071: counter cells |w| = 11step 28163: counter cells |w| = 10step 61843: counter cells |w| = 13step 113367: counter cells |w| = 12step 186191: counter cells |w| = 10step 282524: counter cells |w| = 12step 416283: counter cells |w| = 15step 586100: counter cells |w| = 12step 796806: counter cells |w| = 14step 1047457: counter cells |w| = 15step 1342806: counter cells |w| = 14step 1684524: counter cells |w| = 14step 2088433: counter cells |w| = 17step 2553088: counter cells |w| = 14step 3083256: counter cells |w| = 16step 3673633: counter cells |w| = 14step 4335252: counter cells |w| = 17step 5079378: counter cells |w| = 16step 5892136: counter cells |w| = 16step 6791028: counter cells |w| = 17step 7793930: counter cells |w| = 16step 8900098: counter cells |w| = 16step 10105754: counter cells |w| = 16step 11415984: counter cells |w| = 20step 12834566: counter cells |w| = 16step 14368231: counter cells |w| = 17step 16027820: counter cells |w| = 20step 17829276: counter cells |w| = 18step 19738346: counter cells |w| = 18step 21764234: counter cells |w| = 18step 23902065: counter cells |w| = 17step 26202280: counter cells |w| = 16step 28653845: counter cells |w| = 19step 31274013: counter cells |w| = 16step 34056883: counter cells |w| = 19step 37005935: counter cells |w| = 19step 40111437: counter cells |w| = 21step 43354687: counter cells |w| = 16
clean counter (1) or junk (0)last 1
10274.3e7log xstep 27: clean counter (1) or junk (0) = 0step 1714: clean counter (1) or junk (0) = 1step 10071: clean counter (1) or junk (0) = 0step 28163: clean counter (1) or junk (0) = 1step 61843: clean counter (1) or junk (0) = 0step 113367: clean counter (1) or junk (0) = 1step 186191: clean counter (1) or junk (0) = 1step 282524: clean counter (1) or junk (0) = 1step 416283: clean counter (1) or junk (0) = 0step 586100: clean counter (1) or junk (0) = 1step 796806: clean counter (1) or junk (0) = 1step 1047457: clean counter (1) or junk (0) = 0step 1342806: clean counter (1) or junk (0) = 1step 1684524: clean counter (1) or junk (0) = 1step 2088433: clean counter (1) or junk (0) = 0step 2553088: clean counter (1) or junk (0) = 1step 3083256: clean counter (1) or junk (0) = 1step 3673633: clean counter (1) or junk (0) = 1step 4335252: clean counter (1) or junk (0) = 0step 5079378: clean counter (1) or junk (0) = 1step 5892136: clean counter (1) or junk (0) = 1step 6791028: clean counter (1) or junk (0) = 0step 7793930: clean counter (1) or junk (0) = 1step 8900098: clean counter (1) or junk (0) = 1step 10105754: clean counter (1) or junk (0) = 1step 11415984: clean counter (1) or junk (0) = 0step 12834566: clean counter (1) or junk (0) = 1step 14368231: clean counter (1) or junk (0) = 0step 16027820: clean counter (1) or junk (0) = 0step 17829276: clean counter (1) or junk (0) = 1step 19738346: clean counter (1) or junk (0) = 1step 21764234: clean counter (1) or junk (0) = 1step 23902065: clean counter (1) or junk (0) = 0step 26202280: clean counter (1) or junk (0) = 1step 28653845: clean counter (1) or junk (0) = 0step 31274013: clean counter (1) or junk (0) = 1step 34056883: clean counter (1) or junk (0) = 0step 37005935: clean counter (1) or junk (0) = 0step 40111437: clean counter (1) or junk (0) = 0step 43354687: clean counter (1) or junk (0) = 1
-lo (left edge)last 806
8064274.3e7log xstep 27: -lo (left edge) = 4step 1714: -lo (left edge) = 32step 10071: -lo (left edge) = 54step 28163: -lo (left edge) = 76step 61843: -lo (left edge) = 96step 113367: -lo (left edge) = 116step 186191: -lo (left edge) = 132step 282524: -lo (left edge) = 156step 416283: -lo (left edge) = 178step 586100: -lo (left edge) = 200step 796806: -lo (left edge) = 218step 1047457: -lo (left edge) = 238step 1342806: -lo (left edge) = 254step 1684524: -lo (left edge) = 276step 2088433: -lo (left edge) = 298step 2553088: -lo (left edge) = 318step 3083256: -lo (left edge) = 338step 3673633: -lo (left edge) = 354step 4335252: -lo (left edge) = 378step 5079378: -lo (left edge) = 396step 5892136: -lo (left edge) = 414step 6791028: -lo (left edge) = 438step 7793930: -lo (left edge) = 462step 8900098: -lo (left edge) = 480step 10105754: -lo (left edge) = 502step 11415984: -lo (left edge) = 522step 12834566: -lo (left edge) = 542step 14368231: -lo (left edge) = 562step 16027820: -lo (left edge) = 586step 17829276: -lo (left edge) = 608step 19738346: -lo (left edge) = 626step 21764234: -lo (left edge) = 642step 23902065: -lo (left edge) = 662step 26202280: -lo (left edge) = 684step 28653845: -lo (left edge) = 708step 31274013: -lo (left edge) = 730step 34056883: -lo (left edge) = 752step 37005935: -lo (left edge) = 772step 40111437: -lo (left edge) = 792step 43354687: -lo (left edge) = 806
Template comparisonIndBECv1.v Others: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB0LC
B1LC0RE
C1LA1LD
D1LA1LB
E0RF1RA
F---0RE
file
IndBECv1.v:626
module
Others (nonhalt17)
machine
1LB0RD_1LC1LE_1RA0LB_0RF1RC_1LC1LA_---0RD (10 transitions apart)
diff
same table, start B (its A..F = our B,C,A,E,D,F; no mirror); our start A = its C
note
Cert = hlin with side_binary_inc_rule d1=[0;1] (our names: l 00 (10)^n <C 0 r -> l 10 (00)^n 0 F> r), i.e. R1 on clean words; its orbit is R7 and uses only R4's even case. Ours also needs odd eats (e = 2 mod 3 cycles), separators (R2, R3) and the generic eat R5; 7 hlinx configs already fail on start A.
Proof strategy & riskshow the formal proof will go · 3 risks to watch

Find one regular language L of counter words w (clean digits, lone-1 separators, 010 tail) closed under inc (R1-R3, R6) and the eat (R5), with e = 0 or 2 mod 3; halting needs an inc on words with 1111-type runs, which L must exclude. Then a hand proof (Rocq: inc lemmas per word shape + progress_nonhalt_cond), with 280 covered by the shared orbit.

  • ▲No closed language yet: separators are born at odd eats and die when eaten (29 junk-eat shapes in 83 junk eats); an 8-gram closure (words <= 20) reaches halting words after 3 rounds.
  • ▲inc on general words is known only operationally (R1-R3 cover clean and single-separator words; multi-separator words rest on sampling, R6).
  • ▲280 halts on different reads (B after D1 reading 1); a shared proof must exclude both 88's and 280's halting reads.
Stats & provenance1010 steps simulated · 7,346 cells · the status in full · files
simulated
1010 steps
tape
7,346 cells · 5,089 nonzeros
growth
span ~ t^(1/3) (3,420 cells at 1e9, 7,346 at 1e10; bell grows ~3 cells per cycle, cycle cost ~ bell^2)
status now
Parked 2026-10-13 (Dennis 2026-10-13: 'go with recommendations' -> stage3; its stop rule: no closed form after 2 h means park, with no further asking). Funded stage stage3 found no closed-form invariant. Greatest closed set n >= g(w) at 22 cells: 179,610 states, g = 1 for 178,926, max g = 16. Max g doubles every 2 cells (2/4/8/16 at 16-22 cells), and g is not a function of the 1-runs (at 20 cells, 130 states with runs <= 3 have g > 1). New exact object: the forward-least closed set (least n per cycle start from the real seeds) has 0 halts at 18/20/22 cells (5,071 / 14,547 / 40,998 states) and lies in a small grammar G* = (d|F)* (nothing | L with k0 = 1 | S 0^j 1 | L S 0^j 1). On it n >= Phi + 1 (30,242 / 30,242 parsable at 22 cells) and h >= 2^(D-1). The real orbit to step 1.78e7 lies in G* (204 / 204 cycle starts). But no window built from those bounds is closed: max(Phi+1, 2^(D-1)) gives 571 exits at 18 cells, the S-freeze bound still 472, and pure digit windows exit or halt. The coupling needs history (the n at the last odd eat / last L), which is not a function of the word. The bounded checks stay clean: 0 halts in every forward-least set and in every window closure that uses 2^(D-1) or the Phi bound. 280 (line 280) is parked with it. (status.json, 2026-10-13)
observer's note
Mechanism pinned: every turn to 5.1e7 is a bounce (R1/R6) or an eat (R5); the certified start B is the clean orbit R7. Ours leaves the clean words (junk separators from odd eats), and no closed invariant language is known yet.
files
observe.json · notes.md · status.json

Proof & checks

No proof work yet.

Files

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

namesizechanged
notes.md ↓27 KB2026-10-13 09:21
status.json ↓4.7 KB2026-10-13 09:21
observe.json ↓13 KB2026-10-13 02:44
deepen.json ↓3.1 KB2026-10-13 09:21
data/5 items2026-10-13 09:19
decisions/1 item2026-10-13 09:21
img/4 items2026-10-13 02:41
scripts/8 items2026-10-13 08:59
status.json in full
{
 "tm": "1RB0LC_1LC0RE_1LA1LD_1LA1LB_0RF1RA_---0RE",
 "label": "W5-6",
 "status": "STUCK",
 "stage": "parked (funded stage3 ended at its stop rule)",
 "updated": "2026-10-13",
 "confidence": "med",
 "reason": "Parked 2026-10-13 (Dennis 2026-10-13: 'go with recommendations' -> stage3; its stop rule: no closed form after 2 h means park, with no further asking). Funded stage stage3 found no closed-form invariant. Greatest closed set n >= g(w) at 22 cells: 179,610 states, g = 1 for 178,926, max g = 16. Max g doubles every 2 cells (2/4/8/16 at 16-22 cells), and g is not a function of the 1-runs (at 20 cells, 130 states with runs <= 3 have g > 1). New exact object: the forward-least closed set (least n per cycle start from the real seeds) has 0 halts at 18/20/22 cells (5,071 / 14,547 / 40,998 states) and lies in a small grammar G* = (d|F)* (nothing | L with k0 = 1 | S 0^j 1 | L S 0^j 1). On it n >= Phi + 1 (30,242 / 30,242 parsable at 22 cells) and h >= 2^(D-1). The real orbit to step 1.78e7 lies in G* (204 / 204 cycle starts). But no window built from those bounds is closed: max(Phi+1, 2^(D-1)) gives 571 exits at 18 cells, the S-freeze bound still 472, and pure digit windows exit or halt. The coupling needs history (the n at the last odd eat / last L), which is not a function of the word. The bounded checks stay clean: 0 halts in every forward-least set and in every window closure that uses 2^(D-1) or the Phi bound. 280 (line 280) is parked with it.",
 "siblings": [
  "1RB0LC_1LC0RE_1LA1LD_1LA1LF_0RB1RA_1LC---"
 ],
 "family_note": "No other 740 entry shares 88's table (canon over all starts, renaming + mirror). 280 (line 280) is a different table with the same orbit: 88's B split by entry. The runs coincide while 88's F reads 1 and 88's B entered by D1 reads 0, so one orbit proof excluding both reads covers both machines.",
 "solved_relative": "1LB0RD_1LC1LE_1RA0LB_0RF1RC_1LC1LA_---0RD (IndBECv1.v:626, Others nonhalt17, start B of this table)",
 "checks": {
  "byte_exact_740": "line 88",
  "claims": "none (sheet results row 1010: class only; no Discord hit)",
  "upstream_9cf9e88": "not proved (only start B of the table)"
 },
 "stage1_wave5": {
  "date": "2026-10-13",
  "outcome": "progress",
  "regular_counter_language": "impossible (free closure halts: data/stage1/free_closure_any.txt, free_closure_min12.txt)",
  "token_rules": "T1-T4 validated 400/400 (scripts/stage1/tokrules.py)",
  "random_starts": "0 halts / 1,300 (data/stage1/randstart_*.txt)",
  "coupled_closure": "0 halts; value-window exits 2,875 / 42.0M checks at 20 cells (data/stage1/coupled_closure.txt)",
  "effective_value_window": "0 exits on 4,664 checked states at 18 cells; 6 near-boundary exits on 13,443 at 20 cells (scripts/stage1/cclos_veff.c)"
 },
 "stage2_wave5": {
  "date": "2026-10-13",
  "outcome": "progress",
  "confidence": "med",
  "phi_closed_form": "0 mismatches vs simulated v_eff on 2,416 / 5,989 / 15,089 parsable closure states at 16 / 18 / 20 cells (scripts/stage2/phi.h, cclos_phi.c)",
  "inc_on_G0": "exact at every length (cell-level carry argument, notes.md); 6,111/6,111 canonical G0 words to 16 cells (scripts/stage2/g0check.py)",
  "upper_window": "not invariant: odd eat on z = 11 0^m 1 gives Phi = 1; real run step 21,875 (1S001, n = 28)",
  "lower_window_phi": "n >= Phi - 3 not closed (8 exits at 18 cells, all pending-gain 11-top words); lambda up to 2 still exits",
  "n_ge_50_closure": "0 halts, 0 r=1 at 16/18/20 cells (1,880 / 6,819 / 22,786 states; 40.3M transitions at 20)",
  "greatest_closed_g": "20 cells: 56,845 states, g = 1 for 56,674, max g = 8 (long 1-run junk); real seeds inside (data/stage2/gfix20_n1.out)"
 },
 "next": "Parked; no new decision (stop rule). Reopen only with a history-carrying invariant: state (w, k0, n, m), where m is the n at the last odd eat, and window n >= max(Phi+1, 2^(D-1)), m >= 2^dS for the fresh S. Untested; see notes.md, Funded stage (stage3).",
 "funded": {
  "option": "stage3",
  "date": "2026-10-13"
 },
 "stage3_wave5": {
  "date": "2026-10-13",
  "outcome": "park (stop rule)",
  "confidence": "med",
  "greatest_closed_g_22": "179,610 states, 380.6M transitions, 971 unsafe, g = 1 for 178,926, max g 16 (data/stage3/gfix22_n1.out, g22_gt1.txt)",
  "forward_least_set": "0 halts / 0 r=1 at 18/20/22 cells (5,071 / 14,547 / 40,998 states; 126.2M transitions at 22), all in G*, n >= Phi+1 on all parsable states (scripts/stage3/hmin.c, data/stage3/hmin*.txt)",
  "junk_grammar": "G* = (d|F)* T, T in {nothing, L (k0=1), S 0^j 1 (k0=0), L S 0^j 1 (k0=0)}; real orbit to 1.78e7: 204/204 cycle starts in G*",
  "windows": "no closed window: 2^(D-C) exits for C=1..4 (halts for C=2..4); max(Phi+1, 2^(D-1)) 571 exits; plus S-freeze bound 472-483 exits and 268 states outside G* (data/stage3/window_tests.txt)"
 }
}