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-6
1RB---_0RC0RF_0RD0RA_1RE0LB_1LF0LE_1RC0LE
Where it stands
Parked at the deeper analysis
Funded 2026-10-12 (Dennis: b (fund all five), 2026-10-12): Fund one ~2 h chain-length stage. Funded stage chain_law done (2026-10-12).
Read the full status
Chain-length law found: a level-q chain has l = t1(((k^c)>>(2q+1)) ^ m_q[s]), s = bits q+1..2q of k^c, with 2^q irregular masks per level (0 conflicts on all cycles to 1e11, both lines, and on 2^20 cycles at k = 2^24). But the invariant it was meant to give is false: a faithful C simulator (cycle map + cell-level TM fallback) shows that from k = 650,686 (about 8.5e11 steps) D meets double walls (R10 x6 to k = 2^26, walls merge), F once (R12 at k = 44,953,023), and the right end is reached in phase D; the region past wall ~17 becomes irregular and the masks of levels >= 5 change. No halt and no misaligned tape to k = 2^28 (about 1.4e17 steps), no new event after k = 61,730,238, A never at a zero gap (A/F zero-gap events are record-level conditions on the first even gap and the gap after it). Stuck: non-halting needs a merge-tolerant invariant keeping A/F off double walls in an irregular high region; none known. Optional reopening route in decision.json.
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
Head bounces between movable walls (extra 0s) in (01) runs; local rules exact, counter level and proof open
- Status
- Parkedchain law · updated 2026-10-12Not blocking · Stuck at the chain law stage. Answer Q1–Q3 whenever; a “no” redirects the work.idle since Oct 12 23:02 · status.json 2026-10-12
- Class
- Unknownours: sheet Unknown ≠ ours Skelet-like nested bouncer: walls between (01) runs, a left buffer, multi-level counter (no rule table yet) · low confidence
- On the list
- line 89 of
BB6_holdouts_663.txt· historical 740 line 99
Your calls on file 7
- priority call (answered)
- Fund a wall-level model stage (covers 740 lines 99 and 612), run a bigger CTL search only, or park?
- parked
- Parked by Dennis 2026-10-12 (decision queue: go with recommendations: park). Covers its twin, 740 line 612.
- funded
- option: chain_law · date: 2026-10-12
- 2026-10-12 · carry_stage
- W4-6 and its twin (line 612) now have an exact parity-only cycle map: fund one ~2 h carry stage to derive the level recursion and the invariant, try a wall-level closed-language search instead, or park? (Dennis: apply recommendations (2026-10-12))
- 2026-10-12 · chain_law
- W4-6 and its twin (line 612) now reduce to one chain per cycle at a known level: fund one more ~2 h stage for the chain-length law above level 0, try a wall-level closed-language search instead, or park? (Dennis: b (fund all five), 2026-10-12)
- 2026-10-11 · wall_model
- W4-6 and its E-start twin (740 line 612) are a nested wall-bouncer with a clean 2^(j+1)-periodic hierarchy: fund a ~2 h wall-model stage, run only a bigger CTL search in the background, or park both? (Dennis: go with recommendations (2026-10-11))
- 2026-10-12 · park
- W4-6 and its twin (line 612) have no steady state past 1e11 (walls merge and the far walls turn irregular): keep both parked, fund one merge-tolerant closed-language search, or only watch for a misaligned tape? (Dennis 2026-10-12: 'go with recommendations')
Mechanism
How it works: 3 notes
- Every E left record is K(n; a) = 0^inf <E 01^n 0 01^a1 0 ... 0 01^aL 0^inf: a buffer of n pairs (n+1 per cycle), then walls (single extra 0s); true at all 223,095 records to 1e11.
- Leftward E/F sweeps close open walls and bounce at the first closed one (L3); rightward A/F or C/D phases shift a wall (R5), open it (R6, R7) or turn back (R8, R9, R11). 20 local rules, 6,000/6,000 checks.
- a_j is exactly 2^(j+1)-periodic in cycles (j = 1..8) and the right end is reached at doubling intervals: a counter hierarchy. Halts seen only from a1 = 0, n odd; on the orbit a1 is 7 or 8. Twin: line 612 (start E).
Figures for Checkpoint A
The site's view. The tape grows left; on the right, slanted bursts reach a little deeper each time.
bbchallenge-defaultStart blankRows every step: steps 0..9,999 squeezed into 500 px rows as on bbchallenge.orgWindow cells -200..199, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: each px row blends steps 20y+9 and 20y+10, so 1 px row = 20 steps · Colors: red/green: pale = blended by the squeeze
Each black line is a wall. Compare the walls next to the grey buffer with the deep ones.
customStart blankRows one row per cycleWindow cells -359..0, 1 px = 1 cellColors wall cells of the (01) runs the buffer (01)^n or not yet written
Rows: the tape at the k-th new leftmost cell entered in state E, k = 1..1,024 (steps 23..3,354,849; not evenly spaced in time) · Window: counted from the right end of the written tape (the last 1 is the last column); the buffer (01)^n is cut off at the left · Colors: black: an extra 0 between (01) runs
Fig 3 · Far run: walls merge, right part rearranges
Left walls stay put. The right part jumps at wall merges; the first (k = 650,686) shows at row 20.
customStart blankRows one row per 32,768 cyclesWindow cells 0..719, 1 px = 1 cellColors wall (an extra 0) cells of the (01) runs past the right end
Rows: the E left record at k = 32,768 i, i = 1..1,023 (k to 33,521,664, about 2.3e15 steps), from scripts/hyb2 (cycle map with cell-level TM fallback); faster wall motion is aliased by the sampling · Window: counted from wall 1 (which never moves); the buffer (01)^n left of wall 1 is cut off · Colors: two black px side by side = a double wall (gap 0)
More figures (2)Fig 4–5: From blank: the first cycles · Left records, right edge fixed
Fig 4 · From blank: the first cycles
One row per step. Follow the head: leftward sweeps end two cells further left each time; the right part bounces.
bbchallenge-exploreStart blankRows every step, steps 0..400Window cells -8..39, 1 px = 1/10 cellColors 0 1
Rows: (row r = the configuration after r steps), 10 px per row · Window: 10 px per cell · Colors: head cell coloured by state: A red, B orange, C blue, D green, E magenta, F cyan
Fig 5 · Left records, right edge fixed
Same walls as Fig 2 but in raw cells: a wall shows as a break in the stripe phase.
bbchallenge-defaultStart blankRows the start, then one row per new leftmost cellWindow cells -259..0, 1 px = 1 cellColors 1 0 or never visited head (just moved left)
Rows: (1,665 rows, steps 0..2,400,000; two rows per cycle, E then F); not evenly spaced in time · Window: counted from the right edge (each row's rightmost visited cell is pinned to the last column)
Rules (12/12 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
| rule | from ⟶ to | cases | steps | checked |
|---|---|---|---|---|
| L-sweep | (10)j <E ⟶ <E (01)j | j >= 1 | 2j | ✓300/300 |
| AF-sweep | A> (01)2j ⟶ (10)2j A> | same for F | 4j | ✓300/300 |
| CD-sweep | C> (01)2j ⟶ (10)2j C> | zigzag C,D phases | 12j | ✓300/300 |
| R1/R2 phase flip | A> 01 ⟶ 10 F> | F> 01 -> 10 A> (2 steps) | 2 | ✓300/300 |
| R3/R4 C/D half-pairs | C> 01 ⟶ 00 D> | then 00 D> 01 -> 1010 C> (8 steps) | 4 | ✓300/300 |
| R5 A shifts wall | A> 0 01 ⟶ 10 0 A> | wall moves one pair right | 3 | ✓300/300 |
| R6 F opens wall | F> 0 01 ⟶ 1 00 D> | extra 0 becomes an extra 1 | 5 | ✓300/300 |
| R7 C opens wall | 10 C> 0 01 ⟶ 1 10 10 C> | open wall one pair further left | 9 | ✓300/300 |
| R8/R9/R11 turn back | 11 C> 0 01 ⟶ <E 00100 | 00 D> 0 01 -> <E 01010 (13); 10 C> 0 0 01 -> <E 001010 (15) | 7 | ✓300/300 |
| R10 D at double wall | 00 D> 0 0 01 ⟶ 101010 A> | — | 10 | ✓300/300 |
| L2 open wall closes | 1 <E ⟶ <E 0 | — | 1 | ✓300/300 |
| L3 bounce at wall | 0 0 <E ⟶ 1 0 A> | on the blank this is the edge step 0^inf <E -> 0^inf 10 A> | 3 | ✓300/300 |
Compressed historythe tape as 0∞ <E (01)n 0 (01)a1 0 (01)a2 0 (01)a3 0 (01)a4 ... 0 (01)aL 0∞ at 19 moments: where the rules are read off
0∞ <E (01)n 0 (01)a1 0 (01)a2 0 (01)a3 0 (01)a4 ... 0 (01)aL 0∞
| step | k (cycle) | n | a1 | a2 | a3 | a4 | L (walls) | region cells (2 sum a + L) |
|---|---|---|---|---|---|---|---|---|
| 23 | 1 | 0 | 4 | - | - | - | 1 | 9 |
| 83 | 2 | 1 | 8 | - | - | - | 1 | 17 |
| 389 | 4 | 3 | 7 | 12 | - | - | 2 | 40 |
| 1,883 | 8 | 7 | 7 | 13 | 24 | - | 3 | 91 |
| 7,329 | 16 | 15 | 7 | 13 | 25 | 6 | 9 | 139 |
| 38,745 | 32 | 31 | 7 | 13 | 25 | 5 | 17 | 195 |
| 106,569 | 64 | 63 | 7 | 13 | 25 | 9 | 19 | 229 |
| 183,183 | 128 | 127 | 7 | 13 | 25 | 9 | 17 | 229 |
| 415,233 | 256 | 255 | 7 | 13 | 25 | 9 | 17 | 255 |
| 1,174,333 | 512 | 511 | 7 | 13 | 25 | 9 | 21 | 303 |
| 3,354,849 | 1,024 | 1,023 | 7 | 13 | 25 | 9 | 21 | 303 |
| 11,270,137 | 2,048 | 2,047 | 7 | 13 | 25 | 9 | 23 | 337 |
| 40,337,701 | 4,096 | 4,095 | 7 | 13 | 25 | 9 | 27 | 413 |
| 148,285,829 | 8,192 | 8,191 | 7 | 13 | 25 | 9 | 27 | 413 |
| 566,783,241 | 16,384 | 16,383 | 7 | 13 | 25 | 9 | 29 | 427 |
| 2,209,908,413 | 32,768 | 32,767 | 7 | 13 | 25 | 9 | 31 | 441 |
| 8,719,958,853 | 65,536 | 65,535 | 7 | 13 | 25 | 9 | 33 | 455 |
| 34,637,156,209 | 131,072 | 131,071 | 7 | 13 | 25 | 9 | 37 | 483 |
| 99,999,873,061 | 223,095 | 223,094 | 7 | 13 | 26 | 10 | 37 | 483 |
k (cycle)last 223,095nlast 223,094a1last 7a2last 13a3last 26a4last 10L (walls)last 37region cells (2 sum a + L)last 483Template comparison1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v: partly applies · the nearest solved proof, what carries over, and the transitions that differ
| 0 | 1 | |
|---|---|---|
| A | 1RB | --- |
| B | 0RC | 0RF |
| C | 0RD | 0RA |
| D | 1RE | 0LB |
| E | 1LF | 0LE |
| F | 1RC | 0LE |
- file
machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v⚠ not at pin- module
- —
- machine
1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---(11 transitions apart)- diff
different table; #3 has digit blocks s(d) = 0001/0010 and one sweep per decrement, this machine has single-cell walls and nested bounces- note
- Only #3's proof plumbing carries over: sweep lemmas folded over a block list (RP/LP, PassesR/PassesL) and progress_nonhalt_cond with an invariant. Its macro rules (Dec_k, DecMerge, End, Ov, X1, X2) have no counterpart; here a cycle is a nested bounce over walls, not one decrement.
Proof strategy & riskshow the formal proof will go · 3 risks to watch
Next: a wall-level abstract simulator built from R1-R11/L1-L3 plus the right-end routine, checked against the TM to 1e11; derive the cycle map on (n; a) and the carry hierarchy. Then either an invariant (a1 >= 1, wall spacing) with progress_nonhalt_cond, or a closed-tape-language certificate (robust: no halts from random K with a1 >= 1).
- ▲No macro (cycle-level) rule yet: one cycle is a nested bounce whose depth depends on the whole wall vector; the right-end routine reads a long left context.
- ▲The settled digits (7 13 25 9 3 10 9 6 34 ...) have no closed form yet, so an inductive invariant may need a new idea.
- ▲25 busycoq CTL parameter sets (NG n-gram 4-24, RWL_mod, CPS_LRU) found no certificate; 4 hit the 6 GB cap.
Stats & provenance1011 steps simulated · 446,672 cells · the status in full · files
- simulated
- 1011 steps
- tape
- 446,672 cells
- growth
- left buffer: 2 cells per cycle, cycles ~ sqrt(steps/2); wall region ~ log2(cycles), 483 cells at 1e11
- status now
- Funded 2026-10-12 (Dennis: b (fund all five), 2026-10-12): Fund one ~2 h chain-length stage. Funded stage chain_law done (2026-10-12). Chain-length law found: a level-q chain has l = t1(((k^c)>>(2q+1)) ^ m_q[s]), s = bits q+1..2q of k^c, with 2^q irregular masks per level (0 conflicts on all cycles to 1e11, both lines, and on 2^20 cycles at k = 2^24). But the invariant it was meant to give is false: a faithful C simulator (cycle map + cell-level TM fallback) shows that from k = 650,686 (about 8.5e11 steps) D meets double walls (R10 x6 to k = 2^26, walls merge), F once (R12 at k = 44,953,023), and the right end is reached in phase D; the region past wall ~17 becomes irregular and the masks of levels >= 5 change. No halt and no misaligned tape to k = 2^28 (about 1.4e17 steps), no new event after k = 61,730,238, A never at a zero gap (A/F zero-gap events are record-level conditions on the first even gap and the gap after it). Stuck: non-halting needs a merge-tolerant invariant keeping A/F off double walls in an irregular high region; none known. Optional reopening route in decision.json. (status.json, 2026-10-12)
- observer's note
- Local rules exact (20/20 rules, 6,000/6,000 random checks); cycle-level rules and a non-halting argument are open.
- files
- observe.json · notes.md · status.json
Proof & checks
No proof work yet.
Files
machines/<tm>/: 8 entries · raw notes, status, scripts, images
| name | size | changed |
|---|---|---|
| notes.md ↓ | 29 KB | 2026-10-12 12:24 |
| status.json ↓ | 2.2 KB | 2026-10-12 23:02 |
| observe.json ↓ | 13 KB | 2026-10-12 12:05 |
| deepen.json ↓ | 9.6 KB | 2026-10-12 12:24 |
| data/ | 38 items | 2026-10-12 12:15 |
| decisions/ | 4 items | 2026-10-12 23:02 |
| img/ | 8 items | 2026-10-12 12:03 |
| scripts/ | 30 items | 2026-10-12 12:08 |
status.json in full
{
"tm": "1RB---_0RC0RF_0RD0RA_1RE0LB_1LF0LE_1RC0LE",
"label": "W4-6",
"status": "STUCK",
"stage": "chain_law",
"updated": "2026-10-12",
"confidence": "low",
"reason": "Funded 2026-10-12 (Dennis: b (fund all five), 2026-10-12): Fund one ~2 h chain-length stage. Funded stage chain_law done (2026-10-12). Chain-length law found: a level-q chain has l = t1(((k^c)>>(2q+1)) ^ m_q[s]), s = bits q+1..2q of k^c, with 2^q irregular masks per level (0 conflicts on all cycles to 1e11, both lines, and on 2^20 cycles at k = 2^24). But the invariant it was meant to give is false: a faithful C simulator (cycle map + cell-level TM fallback) shows that from k = 650,686 (about 8.5e11 steps) D meets double walls (R10 x6 to k = 2^26, walls merge), F once (R12 at k = 44,953,023), and the right end is reached in phase D; the region past wall ~17 becomes irregular and the masks of levels >= 5 change. No halt and no misaligned tape to k = 2^28 (about 1.4e17 steps), no new event after k = 61,730,238, A never at a zero gap (A/F zero-gap events are record-level conditions on the first even gap and the gap after it). Stuck: non-halting needs a merge-tolerant invariant keeping A/F off double walls in an irregular high region; none known. Optional reopening route in decision.json.",
"siblings": [
"1RB0RA_1LC0RA_0LF0LD_1LE---_0LC0LB_1LA0RE"
],
"sibling_note": "740 line 612 (778 line 648) is this table started in state E; same K(n; a) family and the same cycle map (rule model = TM on 223,102/223,102 records to 1e11; data/avec_startE_1e11.txt.gz).",
"holdout_line_740": 99,
"holdout_line_778": 106,
"upstream": "Eqv_v3.v TM1 proves halts(1RB---_0RC0RF_0RD0RA_1RE0RD_1LF0LE_1RC0LE) <-> halts(this) (D1 = 0LB replaced by 0RD, which skips the D/B/C zigzag); TM4 does the same for line 612. Equivalence only, no nonhalt proof; the simplified machine is not a holdout and has identical tapes at every E record.",
"priority_call_answered": "Fund a wall-level model stage (covers 740 lines 99 and 612), run a bigger CTL search only, or park?",
"funded": {
"option": "chain_law",
"date": "2026-10-12"
},
"parked": "Parked by Dennis 2026-10-12 (decision queue: go with recommendations: park). Covers its twin, 740 line 612."
}observe.json contract (tools/README-card.md):
2 contract warnings
- rank: missing
- template file not in the pinned tree: machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v