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-7
1RB0RA_1RC0RD_1RD0LC_1LE1RA_---1LF_1RB0LC
Where it stands
Parked at the Rocq proof
Parked 2026-10-12 by the stop rule of the funded 'invariant' stage (Dennis: 'Invariant stage'): no small invariant closes. Covers W4-7 (line 317) and sibling 707.
Read the full status
No property of the digit word excludes the unsupported cases: 237 orbit states at left visits with one number changed and the digit word kept reach case (b) within 30,000 passes (n0 -1/+1: 3/2, a -1/+1: 1/3; unperturbed 0/237); the orbit avoids them by exact sizes (each field-2 bell pushes older waves to the top; counter value near n0 at left visits). Of the 69 distinct hits, 35 are parse artifacts (another 6-encoding parse is supported; all 1,578 such parses match the real TM) and 66 do not halt in 2e9 TM steps, but 3 halt (B> into ready (0,0) followed by ready (2,0) at the top, right after a large width redraw): halting tapes are word-level grammatical, so a proof needs a quantitative invariant. Not a cryptid candidate (long perturbed runs never halt). Line 707: absim2 exact on 226,216/226,216 marker turns from step 117 to 1e9. Restart route in notes.md.
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
Same table as a decider-proved machine; from start A it runs two bells into a wide-digit ternary counter
- Status
- Parkedinvariant · updated 2026-10-12Answered · On Oct 12: Q1–Q3, all yes. Work goes on: stuck at the invariant stage.idle since Oct 12 21:37 · status.json 2026-10-12
- Class
- Bell eats counterours: Bell eats counter (sheet) · ours adds: two bells: the IndBECv1 _3ary table (decider-proved from start B) run from start A · med confidence
- On the list
- line 287 of
BB6_holdouts_663.txt· historical 740 line 317 · observe.json rank #317
Your calls on file 6
- funded
- option: invariant · date: 2026-10-12
- 2026-10-11 · decider2
- Spend one more short stage on decider configurations, or go straight to a hand proof (two bells + ternary counter)? (Dennis: go with recommendations (2026-10-11))
- 2026-10-12 · grammar
- The hand-over rules and an exact field-size law are now pinned: fund a grammar stage (exact digit encodings, J2, the merge carry, checked by an abstract simulator), or park W4-7 and 707? (Dennis: b (fund all five), 2026-10-12)
- 2026-10-12 · grammar2
- The grammar stage found 6 digit encodings and a digit-level rule set that reproduce 1,540 consecutive turns exactly: fund one more stage to pin the top case and run the check to 1e9, or park W4-7 and 707? (Dennis 2026-10-12: 'fund w4-7')
- 2026-10-12 · hand
- The decider route found nothing (384 hlin and 178 CTL runs, all false): start the hand proof with one stage that pins the open rules, or park W4-7 and its sibling 707? (Dennis: apply recommendations (2026-10-12))
- 2026-10-12 · invariant
- The digit-level simulator now matches all 227,414 marker turns to 1e9 with validated rules: fund an invariant stage that shows the unsupported cases never occur (then proof.md), or park W4-7 and 707? (Dennis 2026-10-12: 'Invariant stage')
Mechanism
How it works: 3 notes
- Bell + counter: a 00 marker in a field of 101 blocks moves one block right per pass (F); each pass first adds 1 to a base-3 counter on the right (K1-K6 = the cert's side_3ary rule, mirrored).
- Counter digits can be wide: d (110)^n 0 with d = 000/110/010 for 0/1/2 (n = 0 gives 0000/1100/0100); rules I0, I2, I1a, I1b. A digit right after a wide 2 uses 0011/1111/0111 (J0, J1).
- From A the tape holds two big bells that take turns (the idle one is a wide digit), one small wide digit and 4-cell digits, up to 5e9; start B has one bell. Bell hand-over (E) and the carry past J2 are not pinned. Only halt: A> 0 1 0; none in 1e10 steps.
Figures for Checkpoint A
Fig 1 · bbchallenge default view, first 10,000 steps
The site's own view. Look at the zigzag fill and the two edges growing at different speeds.
bbchallenge-defaultStart blankRows every step 0..9,999Window cells -200..199, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Rows: squeezed into 500 px by the site's bilinear filter (px row y blends steps 20y+9 and 20y+10)
One row per step. Follow the head: short bounces between two columns near x = 270..318, then long trips right.
bbchallenge-defaultStart mid-run: step 2,980,444Rows every step, steps 2,980,444..2,981,843Window cells -198..387, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Start: config 0∞ (101)89 00 (101)15 11 C> (110)82 ... , head at cell 120 · Rows: the first 1,400 rows of a 6,000-step trace · Window: absolute positions; the whole visited span at that time
One row per new leftmost or rightmost cell. Compare the vertical streaks inside with Fig 4 (same table, start B).
bbchallenge-defaultStart blankRows left/right records onlyWindow cells -624..1211, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Rows: the start, then one row per new leftmost or rightmost cell (1,836 rows to step 100,000,000; not evenly spaced in time)
More figures (2)Fig 4–5: Records from blank, start B (certified) · Blaze, 100 million steps
The IndBECv1 _3ary nonhalt3 run in our orientation: one field, one marker drifting along it.
bbchallenge-defaultStart constructed: 0∞ B> 0∞Rows left/right records onlyWindow cells -530..1082, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Rows: 1,613 rows to step 100,000,000; not evenly spaced in time
Fig 5 · Blaze, 100 million steps
Overall growth: both edges keep moving out, the right one faster.
bbchallenge-blazeStart blankRows Blaze time blocks of 131,072 stepsWindow cells -624..1211, 1 px = 2.3 cellsColors 0 1 1 only part of the time (or in part of the cells) of that pixel's block
Rows: (each averaged), 763 blocks to step 1e8, stretched to 500 px · Window: Blaze image: 1 column per 2 cells, 918 columns stretched to 800 px · Colors: no head
Rules (13/15 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
| rule | from ⟶ to | cases | steps | checked |
|---|---|---|---|---|
| K1 digit 0 -> 1 | l 1 C> 0000 r ⟶ l <C 0 1100 r | any l, r | 4 | ✓200/200 |
| K2 digit 1 -> 2 | l 1 C> 1100 r ⟶ l <C 0 0100 r | any l, r | 2 | ✓200/200 |
| K3 digit 2 carries | l 1 C> 0100 r ⟶ l 1111 1 C> r | any l, r | 4 | ✓200/200 |
| K4 carry cleared on the way back | l 1111 <C 0 r ⟶ l <C 0 0000 r | any l, r | 4 | ✓200/200 |
| K5 top digit 1 -> 2 | l 1 C> 11 0∞ ⟶ l <C 0 01 0∞ | any l | 2 | ✓200/200 |
| K6 top digit 2 overflows | l 1 C> 01 0∞ ⟶ l <C 0 0000 11 0∞ | any l | 12 | ✓200/200 |
| F bell step (marker moves one block) | l (101)a 00 (101)b+1 1 <C 0 r ⟶ l (101)a+1 00 (101)b 11 C> r | a >= 1, b >= 0, any l, r | 8b+16 | ✓200/200 |
| I0 wide digit 1 -> 2 | l 1 C> 110 (110)n r ⟶ l <C 0 010 (110)n r | n >= 1 (n = 0 is K2), any l, r | 2 | ✓200/200 |
| I2 wide digit 0 -> 1 | l 1 C> 000 (110)n r ⟶ l <C 0 (110)n+1 r | n >= 1 (n = 0 is K1 without the separator), any l, r | 4 | ✓200/200 |
| I1a wide digit 2 carries (crossing) | l 1 C> 010 (110)n 0 r ⟶ l 1111 (011)n 1 C> r | n >= 0 (n = 0 is K3), any l, r | 3n+4 | ✓200/200 |
| I1b wide carry cleared on return | l 1111 (011)n <C 0 r ⟶ l <C 0 000 (110)n 0 r | n >= 0 (n = 0 is K4), any l, r | 5n+4 | ✓200/200 |
| J0 digit after a wide 2: 0 -> 1 | l 1 C> 010 (110)n 0 0011 r ⟶ l <C 0 000 (110)n 0 1111 r | n >= 1, any l, r (the digit's sweep reaches back into the crossed wire) | 8n+12 | ✓200/200 |
| J1 digit after a wide 2: 1 -> 2 | l 1 C> 010 (110)n 0 1111 r ⟶ l <C 0 000 (110)n 0 0111 r | n >= 1, any l, r | 8n+10 | ✓200/200 |
| J2 digit after a wide 2: 2 carries | l 1111 (011)n 1 C> 0111 r ⟶ (digit -> 1100-like, head leaves right in state A: ...11111 00 A> r) | next digit then read from an A arrival; encoding not pinned | — | –untested |
| E bell hand-over | l 111 (110)k 100 (101)3 11 C> R (active bell, marker 3 blocks from its end) ⟶ l' 11 C> 000 (110)k+4 R' (the bell becomes a wide digit 0; the bell to its left takes one step; R' = R after one visit) | seen in traces only (2,011,920 -> 2,013,101; 2,082,683 -> 2,083,906; ~1.0e8) | — | –untested |
Compressed historythe tape as 0∞ (101)a 02 (101)b 14 (101)c 02 (101)d 1e (110)f 1g C> 0∞ at 29 moments: where the rules are read off
0∞ (101)a 02 (101)b 14 (101)c 02 (101)d 1e (110)f 1g C> 0∞
| step | a | b | c | d | e | f | g |
|---|---|---|---|---|---|---|---|
| 725,418,061 | 2 | 605 | 152 | 413 | 7 | 1 | 19 |
| 729,111,543 | 3 | 605 | 152 | 413 | 7 | 2 | 19 |
| 755,105,777 | 3 | 612 | 134 | 432 | 3 | 8 | 23 |
| 762,690,155 | 3 | 614 | 144 | 431 | 7 | 1 | 19 |
| 781,826,007 | 2 | 620 | 132 | 448 | 3 | 1 | 23 |
| 785,704,865 | 3 | 620 | 129 | 453 | 26 | 0 | 0 |
| 789,597,903 | 3 | 621 | 128 | 454 | 3 | 1 | 23 |
| 793,497,627 | 2 | 623 | 126 | 458 | 26 | 0 | 0 |
| 797,529,303 | 3 | 623 | 155 | 429 | 11 | 1 | 15 |
| 801,454,357 | 3 | 624 | 154 | 430 | 11 | 2 | 15 |
| 805,316,455 | 2 | 626 | 133 | 452 | 7 | 2 | 19 |
| 809,239,461 | 3 | 626 | 124 | 461 | 7 | 3 | 19 |
| 825,207,971 | 3 | 630 | 144 | 447 | 11 | 1 | 15 |
| 829,186,073 | 2 | 632 | 133 | 458 | 7 | 2 | 19 |
| 833,190,677 | 3 | 632 | 125 | 466 | 7 | 3 | 19 |
| 837,207,235 | 3 | 633 | 119 | 473 | 3 | 3 | 23 |
| 841,243,123 | 2 | 635 | 115 | 477 | 3 | 4 | 23 |
| 845,296,375 | 3 | 635 | 111 | 481 | 3 | 5 | 23 |
| 849,385,305 | 3 | 636 | 113 | 485 | 26 | 0 | 0 |
| 854,266,203 | 2 | 638 | 393 | 205 | 19 | 1 | 7 |
| 857,931,347 | 3 | 638 | 204 | 395 | 15 | 1 | 11 |
| 895,020,275 | 3 | 647 | 102 | 500 | 3 | 7 | 23 |
| 942,242,719 | 2 | 659 | 93 | 525 | 3 | 2 | 23 |
| 955,468,597 | 2 | 662 | 97 | 524 | 7 | 2 | 19 |
| 977,717,875 | 3 | 666 | 92 | 535 | 7 | 1 | 19 |
| 982,189,411 | 2 | 668 | 84 | 544 | 3 | 1 | 23 |
| 986,707,917 | 3 | 668 | 81 | 549 | 26 | 0 | 0 |
| 991,251,617 | 3 | 669 | 82 | 548 | 7 | 1 | 19 |
| 995,809,893 | 2 | 671 | 85 | 545 | 7 | 2 | 19 |
alast 2blast 671clast 85dlast 545elast 7flast 2glast 19Template comparisonIndBECv1.v _3ary: partly applies · the nearest solved proof, what carries over, and the transitions that differ
| 0 | 1 | |
|---|---|---|
| A | 1RB | 0RA |
| B | 1RC | 0RD |
| C | 1RD | 0LC |
| D | 1LE | 1RA |
| E | --- | 1LF |
| F | 1RB | 0LC |
- file
IndBECv1.v:258- module
_3ary (nonhalt3)- machine
1LB0LC_1LC0RB_1RD1LF_---1RE_1LA0RB_1LA0LF(11 transitions apart)- diff
same table: mirror + rename (ours A,B,C,D,E,F = cert F,A,B,C,D,E); the cert starts in our B, we start in A (our first step writes the one extra 1)- note
- The cert's rule set = K1-K6 (side_3ary_Pos_inc_rule, QL = QR = our C) + one bell found by the hlin decider (config_T_bsz 745 3). Ours adds a second big bell and wide counter digits. Same config on our flipped table: decider false at T = 746, 1000, 2000, 5000, 20000, and with mnc 3 or 4 at T = 5000 (~2 min each); sibling 707 false at T = 745. On the cert: proved in 4.4 s.
Proof strategy & riskshow the formal proof will go · 3 risks to watch
Finish the small decider grid (mnc 3/4, block size 0, sibling 707). If none proves it, write a hand proof: an invariant of two bells + ternary counter whose low digits are idle fields; prove F, K1-K6, I0-I2 and the two missing rules (I1, E) in Rocq, starting from BellEatsCounter_1RB0RF.v (upstream HEAD) or the _3ary config, then flip to our orientation (Flip.v).
- ▲Bell hand-over (E) and the carry past a digit after a wide 2 (J2) are seen only in traces; their exact case split is not known.
- ▲Field count is only observed bounded (2 big bells + 1 small wide digit up to 5e9); an invariant needs it proved.
- ▲Hand proof is a multi-stage job; the cheap decider route has failed on 8 configs so far.
Stats & provenance1010 steps simulated · 8,464 cells · the status in full · files
- simulated
- 1010 steps
- tape
- 8,464 cells · 5,627 nonzeros
- growth
- span ~ t^0.33 (1,836 cells at 1e8, 8,464 at 1e10); bells 674/630 blocks at 1e9, 1,144/1,071 at 5e9; no halt to 1e10
- status now
- Parked 2026-10-12 by the stop rule of the funded 'invariant' stage (Dennis: 'Invariant stage'): no small invariant closes. Covers W4-7 (line 317) and sibling 707. No property of the digit word excludes the unsupported cases: 237 orbit states at left visits with one number changed and the digit word kept reach case (b) within 30,000 passes (n0 -1/+1: 3/2, a -1/+1: 1/3; unperturbed 0/237); the orbit avoids them by exact sizes (each field-2 bell pushes older waves to the top; counter value near n0 at left visits). Of the 69 distinct hits, 35 are parse artifacts (another 6-encoding parse is supported; all 1,578 such parses match the real TM) and 66 do not halt in 2e9 TM steps, but 3 halt (B> into ready (0,0) followed by ready (2,0) at the top, right after a large width redraw): halting tapes are word-level grammatical, so a proof needs a quantitative invariant. Not a cryptid candidate (long perturbed runs never halt). Line 707: absim2 exact on 226,216/226,216 marker turns from step 117 to 1e9. Restart route in notes.md. (status.json, 2026-10-12)
- observer's note
- Mechanism understood at the component level (bell step, base-3 counter with wide digits; 13 rules validated 200/200); bell hand-over (E) and carry J2 not pinned; the certified sibling's decider config fails on our start.
- files
- observe.json · notes.md · status.json
Proof & checks
- rocq/cal.v · Rocq, not a kill yet
- rocq/g2_707_T5000.v · Rocq, not a kill yet
- rocq/g2_707_T745.v · Rocq, not a kill yet
- rocq/g2_bsz0_T5000.v · Rocq, not a kill yet
- rocq/g2_mnc3_T5000.v · Rocq, not a kill yet
- rocq/g2_mnc4_T5000.v · Rocq, not a kill yet
- rocq/hdr.v · Rocq, not a kill yet
- rocq/try_T1000.v · Rocq, not a kill yet
- rocq/try_T2000.v · Rocq, not a kill yet
- rocq/try_T20000.v · Rocq, not a kill yet
- rocq/try_T5000.v · Rocq, not a kill yet
- rocq/try_T746.v · Rocq, not a kill yet
Files
machines/<tm>/: 9 entries · raw notes, status, scripts, images
| name | size | changed |
|---|---|---|
| notes.md ↓ | 38 KB | 2026-10-12 21:37 |
| status.json ↓ | 1.5 KB | 2026-10-12 21:37 |
| observe.json ↓ | 16 KB | 2026-10-12 18:19 |
| deepen.json ↓ | 15 KB | 2026-10-12 21:37 |
| data/ | 20 items | 2026-10-12 21:37 |
| decisions/ | 5 items | 2026-10-12 21:33 |
| img/ | 5 items | 2026-10-11 00:27 |
| rocq/ | 39 items | 2026-10-11 00:26 |
| scripts/ | 7 items | 2026-10-12 20:54 |
status.json in full
{
"tm": "1RB0RA_1RC0RD_1RD0LC_1LE1RA_---1LF_1RB0LC",
"status": "STUCK",
"stage": "invariant",
"updated": "2026-10-12",
"label": "W4-7",
"confidence": "med",
"reason": "Parked 2026-10-12 by the stop rule of the funded 'invariant' stage (Dennis: 'Invariant stage'): no small invariant closes. Covers W4-7 (line 317) and sibling 707. No property of the digit word excludes the unsupported cases: 237 orbit states at left visits with one number changed and the digit word kept reach case (b) within 30,000 passes (n0 -1/+1: 3/2, a -1/+1: 1/3; unperturbed 0/237); the orbit avoids them by exact sizes (each field-2 bell pushes older waves to the top; counter value near n0 at left visits). Of the 69 distinct hits, 35 are parse artifacts (another 6-encoding parse is supported; all 1,578 such parses match the real TM) and 66 do not halt in 2e9 TM steps, but 3 halt (B> into ready (0,0) followed by ready (2,0) at the top, right after a large width redraw): halting tapes are word-level grammatical, so a proof needs a quantitative invariant. Not a cryptid candidate (long perturbed runs never halt). Line 707: absim2 exact on 226,216/226,216 marker turns from step 117 to 1e9. Restart route in notes.md.",
"siblings": [
"1RB0LA_1LC1RF_---1LD_1RE0LA_1RA0RB_1RE0RF",
"1RB0LC_1RC0RD_1RD0LC_1LE1RF_---1LA_1RB0RF"
],
"solved_relative": "1LB0LC_1LC0RB_1RD1LF_---1RE_1LA0RB_1LA0LF (IndBECv1.v:258, start B of this table)",
"funded": {
"option": "invariant",
"date": "2026-10-12"
}
}