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-4
1RB0RA_1LC0RE_0LD0LB_1LA1LF_1RA0LF_1LC---
Where it stands
Parked at the deeper analysis
Funded rules_stage done (2026-10-11), and its stop rule applies: no invariant handle, so the family 156/188/450/564 is parked. New exact rules R6, RE (one right-end parity transducer that covers E, the first eat bounces and the one-1 RA records), F, FM (full returns) and LR (run-offs, 2 endings), with L's domain corrected.
Read the full status
Each is 2,000/2,000 on random configs against the TM. Iterating the rules reproduces all four orbits to 1e10 with 0 mismatches, with 63-64 unruled moves per orbit (was 668). Open: no closed record language excluding the halting window 1 1 0 <C, macro hierarchy not probed, 63 moves in ~6 one-off shapes. Resume from scripts/rules (absim.py: 1 s exact record simulator) if a multi-level-counter method appears.
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
1010 tape with 00/11 defects; a carry transducer and an eat rule cover 99.3% of bounces; the macro level is open.
- Status
- Parkedrules stage · updated 2026-10-11Not blocking · Stuck at the rules stage stage. Answer Q1–Q3 whenever; a “no” redirects the work.idle since Oct 11 08:40 · status.json 2026-10-11
- Class
- Unknownours: sheet Unknown ≠ ours defect-list counter: left-end carry transducer + eat phase over a 1010 background (multi-level, no template) · low confidence
- On the list
- line 142 of
BB6_holdouts_663.txt· historical 740 line 156 · observe.json rank #156
Your calls on file 3
- priority call (answered)
- Fund one ~2 h rules stage (rule the 5 remaining event families, build the abstract list machine for all four starts, test the macro hierarchy), or park the family 156/188/450/564 with R4/#32?
- funded
- option: rules_stage · date: 2026-10-11
- 2026-10-11 · rules_stage
- W4-4 and its three sibling starts (188, 450, 564) share one defect-list mechanism: fund one ~2 h rules stage to close the abstract model and probe the macro hierarchy, or park the family with R4/#32? (Dennis: go with recommendations (2026-10-11))
Mechanism
How it works: 3 notes
- The tape is 1010... with isolated extra symbols (00 = extra 0, 11 = extra 1), and every sweep complements what it crosses. So the state is a list (10)^n0 x1 (10)^n1 ... of segment lengths n_i and extra bits x_i. It halts iff it reaches 1 1 0 <C (window W5 with 11 directly left of 00).
- Two exact rules cover 99.3% of record moves to 1e10. L (31%) is a left-end bounce acting as a 4-state carry transducer on (n_i mod 2, x_{i+1}), with deltas 0, +-1, +2, +3, +4 (30,720/30,720 real, 900/900 random). E (68%) is a 000 marker eating the segment to its left, one pair per bounce, and adding 2 pairs at the right end; it is exact iff every segment to its right is even.
- Open: 668 moves (end rules, full sweeps, 3 merges) and the macro level. It has 2-13 separators, recurring tail motifs and left digits growing at power-of-3 rates per pair, so it looks hierarchical. Siblings 188/450/564 (starts D/B/E) show the same coverage, as near-twin orbits that never merge.
Figures for Checkpoint A
Fig 1 · First 10,000 steps (site view)
The site's own picture. Look at the fine vertical stripes (the 1010 background) and where their phase breaks (the defects).
bbchallenge-defaultStart blankRows every step, steps 0..10,000 squeezed into 500 rowsWindow cells -200..199, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Rows: site canvas, bilinear: about 20 steps per row · Window: cell 0 = start cell, at column 200
Rows 495-790: bounces off the left edge, turning points creeping right. Rows 31-55, 456-480: short right-end bounces.
bbchallenge-defaultStart blankRows every 20 steps, steps 0..17,000 (851 rows)Window cells -260..79, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Each zigzag is one bounce from the right end. Compare successive left turning points and the right edge.
bbchallenge-defaultStart constructed: 0∞ (10)3 0 (10)7 0 0 (10)4 0 (10)6 A> 0∞Rows every step, steps 0..639Window cells -56..15, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)
Rows: the right-end returns are at steps 54, 116, 186, 264, 350, 444, 546 · Window: cell 0 = the start head cell, at column 56
More figures (2)Fig 4–5: Records view: defects as lines · Long run to 7.6e8 (sampled)
Fig 4 · Records view: defects as lines
Defects show as lines in the stripe texture: slanted lines are 000 markers walking left during eat phases.
bbchallenge-defaultStart blankRows left/right recordsWindow cells -892..607, 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,500 rows, steps 0..425,442)
Fig 5 · Long run to 7.6e8 (sampled)
Solid bands are alternating segments seen through 64-cell sampling. Rows 800-1260: a long eat phase (frozen left block).
bbchallenge-defaultStart blankRows every 500,000 stepsWindow cells -46,836..18,972, 1 px = 64 cellsColors 1 0 or unvisited head
Rows: steps 0..760,000,000 (1,521 rows; stopped at the image cell cap) · Window: every 64th cell sampled; the head is always drawn · Colors: with 64-cell sampling a 1010 segment shows as solid white or solid black (its phase), so each white/black edge marks a defect
Rules (6/7 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
| rule | from ⟶ to | cases | steps | checked |
|---|---|---|---|---|
| S shifts | A> (10)2n | B> (10)2n | (10)n <B ⟶ (01)2n A> | (01)2n B> | <B (01)n | n >= 1 | 4n, 4n, 2n | ✓120/120 |
| W1-W4 rightward windows | A> 100 | B> 100 | A> 1011 | B> 101 ⟶ <C 101 | 011 B> | <C 1010 | 010 A> | A-mode pair before an extra symbol: turn (W1, W3); B-mode pair: pass (W2, W4) | 5 | 3 | 7 | 3 | ✓4/4 |
| W5-W6 leftward windows | 0100 <B | 110 <B ⟶ <C 1101 | 010 A> | W5: 00 is crossed and lands 2 cells left as 11; with 11 directly left (1100 <B) the same steps halt. W6: turn at 11 | 4 | 5 | ✓2/2 |
| E eat bounce | 0∞ L 0 (10)a+1 0 0 [(10)q_i 0]_(i<=k) (10)c A> 0∞ ⟶ 0∞ L 0 (10)a 0 0 [(10)q_i 0]_(i<=k) (10)c+2 A> 0∞ | a >= 1, every q_i even, c even (any odd q_i or c: fails, 0/n in all 24 parity classes) | 4c + 4 sum q_i + 2k + 12 | ✓200/200 |
| L left-end bounce (carry transducer) | 0∞ <A (10)n0 x1 (10)n1 ... xk (10)nk 1 0∞ ⟶ the same list with deltas from the transducer S/T/Z+/Z-/Q read on (n_i mod 2, x_(i+1)), see notes.md | STOP rows of the transducer; undefined rows (e.g. Z- on (odd, end)) leave for the right end | — | ✓900/900 |
| L on the real run | every LA record to the next LA record, to 1e10 ⟶ transducer prediction | 30,720 moves; 58 parity-signature classes at 1e8, 0 inconsistent | — | ✓30720/30720 |
| unruled moves | end rules, LA>RA, RA>LA, merges ⟶ (no rule yet) | 668 of 98,334 record moves to 1e10 | — | –untested |
Compressed historythe tape as at each eat-phase start (RA record, gap form): d1 |3 d2 |3 ... a |4 q1 |3 ... |3 c A> 0∞ (|3 = 00, |4 = 000) at 40 moments: where the rules are read off
at each eat-phase start (RA record, gap form): d1 |3 d2 |3 ... a |4 q1 |3 ... |3 c A> 0∞ (|3 = 00, |4 = 000)
| step | d1 (leftmost digit) | separators | a (digit left of the 000) | 000 markers |
|---|---|---|---|---|
| 620 | 14 | 2 | 8 | 1 |
| 9,124 | 56 | 4 | 8 | 1 |
| 23,383 | 92 | 5 | 44 | 1 |
| 142,090 | 188 | 2 | 130 | 1 |
| 325,742 | 230 | 4 | 8 | 1 |
| 779,559 | 466 | 7 | 44 | 1 |
| 1,453,639 | 690 | 7 | 54 | 1 |
| 2,400,088 | 886 | 6 | 8 | 1 |
| 4,437,392 | 1,270 | 8 | 8 | 1 |
| 7,684,176 | 1,718 | 8 | 876 | 1 |
| 14,311,149 | 1,908 | 7 | 54 | 1 |
| 19,484,294 | 2,416 | 8 | 8 | 1 |
| 25,385,730 | 2,936 | 9 | 885 | 1 |
| 50,875,119 | 3,942 | 8 | 324 | 1 |
| 50,875,573 | 3,942 | 8 | 324 | 1 |
| 59,950,500 | 4,298 | 7 | 24 | 2 |
| 95,752,744 | 5,846 | 10 | 8 | 1 |
| 122,228,137 | 6,818 | 11 | 44 | 1 |
| 215,147,510 | 9,446 | 8 | 130 | 1 |
| 265,795,226 | 10,598 | 10 | 8 | 1 |
| 402,388,632 | 13,206 | 11 | 5,386 | 1 |
| 402,451,521 | 13,206 | 11 | 5,383 | 1 |
| 906,280,329 | 17,920 | 12 | 69 | 1 |
| 1,000,142,676 | 19,180 | 10 | 14 | 1 |
| 1,691,110,423 | 22,530 | 11 | 886 | 1 |
| 1,810,671,854 | 22,958 | 10 | 18 | 1 |
| 1,866,253,024 | 23,414 | 8 | 10,782 | 1 |
| 2,437,611,296 | 23,486 | 7 | 11,116 | 1 |
| 2,437,699,472 | 23,486 | 7 | 11,116 | 1 |
| 4,062,847,899 | 24,250 | 9 | 1,920 | 1 |
| 4,497,716,228 | 25,038 | 9 | 52 | 1 |
| 4,556,800,202 | 25,590 | 8 | 56 | 1 |
| 4,663,094,521 | 26,554 | 10 | 4,667 | 1 |
| 5,865,924,971 | 28,076 | 10 | 4,179 | 1 |
| 6,155,413,068 | 28,504 | 8 | 14 | 1 |
| 6,967,957,433 | 29,476 | 9 | 344 | 1 |
| 7,045,484,290 | 29,736 | 8 | 8,462 | 1 |
| 8,212,699,050 | 31,160 | 9 | 16 | 2 |
| 8,399,666,536 | 32,348 | 10 | 8 | 1 |
| 9,510,822,139 | 38,720 | 13 | 44 | 1 |
d1 (leftmost digit)last 38,720separatorslast 13a (digit left of the 000)last 44000 markerslast 1Template comparison1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v: partly applies · the nearest solved proof, what carries over, and the transitions that differ
| 0 | 1 | |
|---|---|---|
| A | 1RB | 0RA |
| B | 1LC | 0RE |
| C | 0LD | 0LB |
| D | 1LA | 1LF |
| E | 1RA | 0LF |
| F | 1LC | --- |
- file
1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v⚠ not at pin- module
- —
- machine
1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---(6 transitions apart)- diff
6 cells differ from #11b (= #11's table renamed); architecture differs- note
- Kill #11's .v: shifts S1-S6, windows T1-T14, K(ds; a, b) over d0/d1 digits, carry M, drop, overflow O, one INV. Reusable: the list-of-digits K-config and the list-sweep induction lemmas. Not reusable: our carry is a parity transducer that changes digit lengths, plus a separate eat phase E and a multi-level macro, so the rules and the invariant are new.
Proof strategy & riskshow the formal proof will go · 3 risks to watch
Rule the 5 unruled event families (0.7% of record moves) to get an exact abstract list machine for all four starts. Then find the macro hierarchy and an invariant that keeps 11 from sitting directly left of 00 when a leftward sweep crosses it. The formal side can reuse #11's list-sweep lemmas.
- ▲The macro level is a hierarchical counter with no template (like the parked R4/#32), so an invariant may be out of reach.
- ▲Every branch is decided by parities of large transferred numbers. A pseudo-random parity sequence would make it cryptid-like (no sign of this so far).
- ▲668 record moves to 1e10 have no validated rule yet, and the observed parity law fails at 17 of 60 eat starts.
Stats & provenance1010 steps simulated · 76,685 cells · the status in full · files
- simulated
- 1010 steps
- tape
- 76,685 cells · 38,338 nonzeros
- growth
- span ~ t^0.48 (25,552 at 1e8, 76,685 at 1e9); no halt to 1e10
- status now
- Funded rules_stage done (2026-10-11), and its stop rule applies: no invariant handle, so the family 156/188/450/564 is parked. New exact rules R6, RE (one right-end parity transducer that covers E, the first eat bounces and the one-1 RA records), F, FM (full returns) and LR (run-offs, 2 endings), with L's domain corrected. Each is 2,000/2,000 on random configs against the TM. Iterating the rules reproduces all four orbits to 1e10 with 0 mismatches, with 63-64 unruled moves per orbit (was 668). Open: no closed record language excluding the halting window 1 1 0 <C, macro hierarchy not probed, 63 moves in ~6 one-off shapes. Resume from scripts/rules (absim.py: 1 s exact record simulator) if a multi-level-counter method appears. (status.json, 2026-10-11)
- observer's note
- Observe done at LOW confidence: exact window, eat and carry rules cover 99.3% of record moves to 1e10; 5 event families unruled; no macro rule or non-halting argument. Priority call in decision.json.
- 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 ↓ | 13 KB | 2026-10-11 08:40 |
| status.json ↓ | 1.6 KB | 2026-10-11 08:40 |
| observe.json ↓ | 13 KB | 2026-10-10 23:41 |
| deepen.json ↓ | 2.9 KB | 2026-10-11 08:40 |
| decisions/ | 1 item | 2026-10-11 08:40 |
| img/ | 5 items | 2026-10-10 23:35 |
| scripts/ | 29 items | 2026-10-11 08:23 |
status.json in full
{
"tm": "1RB0RA_1LC0RE_0LD0LB_1LA1LF_1RA0LF_1LC---",
"label": "W4-4",
"status": "STUCK",
"stage": "rules_stage",
"updated": "2026-10-11",
"confidence": "low",
"reason": "Funded rules_stage done (2026-10-11), and its stop rule applies: no invariant handle, so the family 156/188/450/564 is parked. New exact rules R6, RE (one right-end parity transducer that covers E, the first eat bounces and the one-1 RA records), F, FM (full returns) and LR (run-offs, 2 endings), with L's domain corrected. Each is 2,000/2,000 on random configs against the TM. Iterating the rules reproduces all four orbits to 1e10 with 0 mismatches, with 63-64 unruled moves per orbit (was 668). Open: no closed record language excluding the halting window 1 1 0 <C, macro hierarchy not probed, 63 moves in ~6 one-off shapes. Resume from scripts/rules (absim.py: 1 s exact record simulator) if a multi-level-counter method appears.",
"relation": "one table with 4 holdout starts (A = 156, B = 450, D = 188, E = 564)",
"siblings": [
"1RB1RF_1LC0LB_1RE0LD_1LB0RF_0RA0RC_1RE---",
"1RB0LE_0RC0RA_1RD1RF_1LA0LD_1LD0RF_1RB---",
"1RB0LF_1RC0RB_1LD0RA_0LE0LC_1LB1LF_1LD---"
],
"holdout_line_740": 156,
"existing_work": "none found: sheet Results row 66 is class Unknown only; no Discord hit; upstream busycoq only has Eqv_v3 TM23 (equivalent to its E1=0LB variant).",
"priority_call_answered": "Fund one ~2 h rules stage (rule the 5 remaining event families, build the abstract list machine for all four starts, test the macro hierarchy), or park the family 156/188/450/564 with R4/#32?",
"funded": {
"option": "rules_stage",
"date": "2026-10-11"
}
}observe.json contract (tools/README-card.md):
1 contract warning
- template file not in the pinned tree: 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v