tools/rebuild_pages.sh rebuilds the site within 5 minutes of a change; by hand: python3 -B tools/site.py.1RB0LF_1RC1RB_0RD0RC_1LE1LF_1LD---_0LB1LA
Where it stands
Parked at the deeper analysis
Twin port refuted (different halting event). 500 follows TM2's macro run exactly: 220/220 recorded counter words equal to the follow-stage simulator, to phase 370, and TM2's b = n-1 per phase.
Read the full status
TM2 exits 16 macro steps after its 374th overflow (early in 500's phase 375) and halts at step 13,297 when B reads 1. On the same configuration, with a and b kept symbolic, 500 makes the A0 turn, runs 72,652 steps without halting and re-enters TM2's own cfgL' a b r'' (next rule LIncs). TM2's left lemmas (LInc, LRst_101, LRst_11) hold for 500 iff a is odd, and a = 3 mod 4 throughout the orbit, so 500 can only halt on the counter side. It was already followed to phase 1,857 with no halt. Machine stays parked.

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.
Overview
In one sentence
Left binary counter +1 per visit; right 1-block loses 2 cells/visit, pad gains 4; reset doubles it. Digit grammar open
- Status
- Parkedtwin port refuted · updated 2026-10-14Not blocking · Stuck at the twin port refuted stage. Answer Q1–Q3 whenever; a “no” redirects the work.idle since Oct 14 16:54 (44 h ago) · status.json 2026-10-14
- Class
- Sync bouncer counterours: Sync bouncer counter (sheet) · ours adds: binary counter on the left, eroding 1-block timer on the right, doubling reset · med confidence
- On the list
- line 453 of
BB6_holdouts_663.txt· historical 740 line 500
Your calls on file 7
- parked
- Parked 2026-10-11 (Dennis: go with recommendations): Park #37 behind the other machines.
- funded
- option: follow · date: 2026-10-10 · auto: true
- next
- No port. #37 stays parked (Dennis 2026-10-11). Asset: TM2's representation (cfgL'/cfgR', rest/RIncs, LInc/LIncs/LOv/LRst) is an exact accelerator for #37 under 'a odd'; a nonhalt proof still needs the counter-side invariant (lemma B'/rule M of the follow stage).
- 2026-10-10 · deepen
- #37's visit, reset and halt rules are exact. What is open is the counter-word grammar K (its closure under inc and reset) and the reason every reset lands on bit 0 = 0. Spend one deepen stage pinning K, or park #37? (Dennis: go with all recommendations (2026-10-10))
- 2026-10-10 · deepen2
- #37's sync now rests on one open lemma B (its bottom counter run never again becomes an erasable 11 digit): fund a second deepen round on B, or park #37? (auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was at lunch). Override any time.)
- 2026-10-10 · follow
- #37's sync now hinges on whether a short run ever reaches the bottom during an excursion: port the jump simulator to C and follow the real orbit through the next excursions, or park #37? (auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.)
- decision.json · answered 2026-10-11: park
- #37 stays in sync to phase 1,857, and its next excursion (phase 3,321) is predicted benign: park it, spend one round deriving the merge-wave rule, or first confirm phase 3,321 on the real orbit? Decisions →
Mechanism
How it works: 3 notes
- Each visit (right record in C) maps
0^inf L 1^n 0^g C> 0^infto0^inf inc(L) 1^(n-2) 0^(g+4) C> 0^inf: the head stripes the block going left, adds 1 to the counter L, zigzags back and erases the block's last 2 cells (early in a phase, filler cells of L can merge into the block). - inc is a binary +1: the carry depth follows the ruler sequence (27,084/27,124 visits). Digits are 1 or 2 cells, separated by
00gaps or 1-runs the carry passes; the layout is rebuilt at each reset and migrates early in a phase (the open part). - Reset at n=2:
L0 0 1^2 0^g C>->L0 1^(g+6) C>with g = 4(visits-1), so the block about doubles. All 12 resets to 2.5e9 hit a bit-0 = 0 visit; 35/36 off-sync variants leave an odd pad and halt next visit. Not a cryptid: plain +1, linear timer.
Figures for Checkpoint A
One row per new edge cell. Follow each white triangle down to the full-width white row that ends it.
Each row is the tape at a visit start. Read right to left from the white block; compare flip rates.
Every step of one visit's counter part. Top: sweep left; middle: turn at the carry; bottom: zigzag back.
More figures (2)Fig 4–5: bbchallenge default view, 10,000 steps · Lowest 48 runs per phase, real orbit
The site's own view: the first four phases as growing bands.
Columns are runs above the block. Vertical stripes are frozen runs; diagonal bands are the waves after excursions.
Rules (9/10 validated)1 failing · exact tape rewrites the proof will formalize, each re-checked by simulation
| rule | from ⟶ to | cases | steps | checked |
|---|---|---|---|---|
| V visit | 0∞ L 1m 0g C> 0∞ ⟶ 0∞ inc(L) 1m+d 0g+4 C> 0∞ | m >= 4; g even; (inc(L), d) depend on L only (d = -2 except when bit 0 flips or filler merges); tested on every visit to 2.5e9 with random m' (same parity) and g' (both residues mod 4) | 6m+2g+c(L) | ✓54248/54248 |
| Inc binary +1 | carry depth of visit k in a phase ⟶ v2(k+c)+1 digits flipped | one offset c per phase; 40 misses are early-phase digit migrations (a filler zero joins a digit) | — | ✗27084/27124 |
| R0 bit-0 visit | 0∞ L0 0 1n 0g C> 0∞ ⟶ 0∞ L0 1n-1 0g+4 C> 0∞ | n even >= 4, g even, any word L0 | 6n+2g-10 | ✓600/600 |
| R1s bit-1 carry (1 cell) | 0∞ L0 1 0 00 1 1n 0g C> 0∞ ⟶ 0∞ L0 1 1 00 0 1n-2 0g+4 C> 0∞ | n even >= 4, g even, any L0 (phase-10 layout) | 6n+2g+10 | ✓600/600 |
| R1d bit-1 carry (2 cells) | 0∞ L0 1 0 00 00 00 1 1n 0g C> 0∞ ⟶ 0∞ L0 1 0 00 11 00 0 1n-2 0g+4 C> 0∞ | n even >= 4, g even, any L0 (phase-9 layout) | 6n+2g+14 | ✓600/600 |
| R reset | 0∞ L0 0 12 0g C> 0∞ ⟶ 0∞ L0 1g+6 C> 0∞ | g = 0 mod 4 (always: g = 4(visits-1)); any L0; all 12 real resets plus random g | — | ✓636/636 |
| P pad fill | 0∞ X 1n 0g C> 0∞ ⟶ 0∞ X 1n-1 <F 1g+3 0∞ | g even, n >= 1 | g+4 | ✓400/400 |
| H odd pad | 0∞ X 1n 0g C> 0∞ ⟶ halt | g odd: E reads the last block cell | g+4 | ✓5825/5825 |
| S stripe | L 12k+1 <F R ⟶ L <A 1 (01)k R | k >= 0 | 2k+1 | ✓400/400 |
| Z zigzag | 1a C> (01)k 1b 0∞ ⟶ 1a+2k-1 C> 1b+1 0∞ | a, k, b >= 1 | 10k-5 | ✓400/400 |
Compressed historythe tape as 0∞ L 1m 0g C> 0∞ at 36 moments: where the rules are read off
| step | phase | m | g | visit | span |
|---|---|---|---|---|---|
| 13 | 1 | 6 | 0 | 2 | 7 |
| 112 | 2 | 14 | 0 | 5 | 19 |
| 472 | 2 | 10 | 16 | 9 | 32 |
| 836 | 2 | 2 | 32 | 13 | 44 |
| 911 | 3 | 38 | 0 | 14 | 47 |
| 3,589 | 3 | 25 | 44 | 25 | 78 |
| 6,027 | 3 | 2 | 88 | 36 | 108 |
| 6,214 | 4 | 94 | 0 | 37 | 111 |
| 19,282 | 4 | 50 | 96 | 61 | 160 |
| 30,190 | 4 | 2 | 192 | 85 | 216 |
| 30,585 | 5 | 198 | 0 | 86 | 219 |
| 90,277 | 5 | 105 | 208 | 138 | 332 |
| 138,567 | 5 | 2 | 412 | 189 | 438 |
| 139,402 | 6 | 418 | 0 | 190 | 441 |
| 379,634 | 6 | 210 | 416 | 294 | 650 |
| 576,706 | 6 | 2 | 832 | 398 | 866 |
| 578,381 | 7 | 838 | 0 | 399 | 869 |
| 1,543,463 | 7 | 421 | 836 | 608 | 1,287 |
| 2,333,933 | 7 | 2 | 1,672 | 817 | 1,706 |
| 2,337,288 | 8 | 1,678 | 0 | 818 | 1,709 |
| 6,208,302 | 8 | 841 | 1,676 | 1,237 | 2,548 |
| 9,377,196 | 8 | 2 | 3,352 | 1,656 | 3,394 |
| 9,383,911 | 9 | 3,358 | 0 | 1,657 | 3,397 |
| 24,898,377 | 9 | 1,681 | 3,356 | 2,496 | 5,088 |
| 37,597,555 | 9 | 2 | 6,712 | 3,335 | 6,770 |
| 37,610,990 | 10 | 6,718 | 0 | 3,336 | 6,773 |
| 99,808,022 | 10 | 3,362 | 6,720 | 5,016 | 10,154 |
| 150,715,866 | 10 | 2 | 13,440 | 6,696 | 13,518 |
| 150,742,757 | 11 | 13,446 | 0 | 6,697 | 13,521 |
| 399,462,331 | 11 | 6,725 | 13,444 | 10,058 | 20,243 |
| 602,996,957 | 11 | 2 | 26,888 | 13,419 | 26,970 |
| 603,050,744 | 12 | 26,894 | 0 | 13,420 | 26,973 |
| 1,597,795,614 | 12 | 13,449 | 26,892 | 20,143 | 40,428 |
| 2,411,745,732 | 12 | 2 | 53,784 | 26,866 | 53,878 |
| 2,411,853,311 | 13 | 53,790 | 0 | 26,867 | 53,881 |
| 9,646,815,518 | 14 | 107,582 | 0 | - | 107,697 |
phaselast 14mlast 107,582glast 0visitlast -spanlast 107,697Template comparisonSBCv7.v TM4: partly applies · the nearest solved proof, what carries over, and the transitions that differ
| 0 | 1 | |
|---|---|---|
| A | 1RB | 0LF |
| B | 1RC | 1RB |
| C | 0RD | 0RC |
| D | 1LE | 1LF |
| E | 1LD | --- |
| F | 0LB | 1LA |
- file
SBCv7.v:610- module
TM4 (line 610); also SBCv11.v GenericNonhalt- machine
1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_0RA---(11 transitions apart)- diff
11 of 12 transitions differ: a class-level match, not a delta- note
- Same macro shape (left binary counter, right side reset in sync, progress_nonhalt_cond). TM4's fixed digit words d0/d1 and BC.Mul2 do not fit: here digits are 1 or 2 cells with phase-dependent fillers. No solved machine within 3 transitions (nearest: CTLv1, RWL_mod, CPS_LRU deciders at 4).
Proof strategy & riskshow the formal proof will go · 3 risks to watch
Visit-level proof: invariant = L in a counter language K (with bit-0 alignment to the block), g = 0 mod 4. Prove V for L in K from S, P, Z and per-digit carry lemmas; R for the reset (plus the absorption visits); then progress_nonhalt_cond. Open: write down K (digit/filler grammar) and prove it closed under inc and the reset, including the sync.
- ▲The counter's digits (1 or 2 cells) and fillers change layout at each reset and migrate early in a phase; the grammar K is not pinned, and its closure is the proof.
- ▲Sync: all 12 resets landed on a bit-0 = 0 visit, but visits per phase are not always odd (phase 5: 104, after 10 absorbed cells). 35/36 off-sync resets halt on the next visit (tested), so the sync must come out of the grammar.
- ▲No close template (SBCv7/SBCv11 are class-level only): expect a long custom .v, kill #4-sized or larger.
Stats & provenance1.2·1010 steps simulated · 115,087 cells · the status in full · files
- simulated
- 1.2·1010 steps
- tape
- 115,087 cells · 114,968 nonzeros
- growth
- span ~ t^0.5: the block about doubles each phase and a phase costs ~2.5 n^2 steps (~4x the last); left edge -175 at 1.2e10
- status now
- Twin port refuted (different halting event). 500 follows TM2's macro run exactly: 220/220 recorded counter words equal to the follow-stage simulator, to phase 370, and TM2's b = n-1 per phase. TM2 exits 16 macro steps after its 374th overflow (early in 500's phase 375) and halts at step 13,297 when B reads 1. On the same configuration, with a and b kept symbolic, 500 makes the A0 turn, runs 72,652 steps without halting and re-enters TM2's own cfgL' a b r'' (next rule LIncs). TM2's left lemmas (LInc, LRst_101, LRst_11) hold for 500 iff a is odd, and a = 3 mod 4 throughout the orbit, so 500 can only halt on the counter side. It was already followed to phase 1,857 with no halt. Machine stays parked. (status.json, 2026-10-14)
- observer's note
- Mechanism found (binary counter + eroding block + doubling reset); 10 rules validated (V on every visit to 2.5e9, 54,248/54,248; reset 636/636); confidence med because the counter's digit grammar and its closure under resets are open.
- files
- observe.json · notes.md · status.json
Proof & checks
No proof work yet.
Files
machines/<tm>/: 9 entries · raw notes, status, scripts, images
| name | size | changed |
|---|---|---|
| notes.md ↓ | 31 KB | 2026-10-14 16:54 |
| status.json ↓ | 3.3 KB | 2026-10-14 16:54 |
| observe.json ↓ | 14 KB | 2026-10-10 15:11 |
| deepen.json ↓ | 12 KB | 2026-10-10 15:13 |
| decision.json ↓ | 3.1 KB | 2026-10-11 08:19 |
| decisions/ | 3 items | 2026-10-10 15:14 |
| img/ | 6 items | 2026-10-10 15:11 |
| scripts/ | 24 items | 2026-10-14 16:29 |
| work/ | 21 items | 2026-10-14 16:29 |
status.json in full
{
"tm": "1RB0LF_1RC1RB_0RD0RC_1LE1LF_1LD---_0LB1LA",
"label": "P-500",
"status": "STUCK",
"stage": "twin_port_refuted",
"updated": "2026-10-14",
"holdout_line_740": 500,
"parent": "SBCv9.v Module TM2 (1RB0RF_0LC---_1LD1LC_0LE0LD_1RE1RF_0RC1RA), HALT",
"relation": "mirror(500) with states A,B,C,D,E,F -> TM2's A,C,D,E,G,F equals TM2 except A0 (TM2: A0 1RB, B0 0LC, C1 1LC = 3 steps, halts if B reads 1; 500: 1 step) and the E self-loop (500 alternates D/E over 0s and halts at E1 after an odd number of 0s); same start, same tape at all times",
"reason": "Twin port refuted (different halting event). 500 follows TM2's macro run exactly: 220/220 recorded counter words equal to the follow-stage simulator, to phase 370, and TM2's b = n-1 per phase. TM2 exits 16 macro steps after its 374th overflow (early in 500's phase 375) and halts at step 13,297 when B reads 1. On the same configuration, with a and b kept symbolic, 500 makes the A0 turn, runs 72,652 steps without halting and re-enters TM2's own cfgL' a b r'' (next rule LIncs). TM2's left lemmas (LInc, LRst_101, LRst_11) hold for 500 iff a is odd, and a = 3 mod 4 throughout the orbit, so 500 can only halt on the counter side. It was already followed to phase 1,857 with no halt. Machine stays parked.",
"checks": {
"check_twin": "scripts/port/check_twin.py (T1-T6, ~6 min; work/port/check_twin.log)",
"layouts": "work/port/cmp_tm2_vs_500_layouts.log (202/202 with b = n-1; check_twin T4: 220/220 words)",
"exit_window": "work/port/exit_window.log"
},
"confidence": "high",
"funded": {
"option": "follow",
"date": "2026-10-10",
"auto": true
},
"parked": "Parked 2026-10-11 (Dennis: go with recommendations): Park #37 behind the other machines.",
"prior_reason": "Parked 2026-10-11 (Dennis: go with recommendations): Park #37 behind the other machines. Follow (funded 2026-10-10, auto-applied recommendation) done; new priority call in decision.json (recommended: park). A C port of the jump simulator (exact: 160/160 phases equal to Python, random instances 90/90 vs Python and 90/90 vs exact fastphase) followed the real orbit to the start of phase 1,857 (n ~ 2^1860): no off-sync, no halt. Excursions at phases 91, 119, 215, 487 were all benign, with 14, 77, 93 and 700 cells in the run that became the bottom; the 3-run that sat 16 runs up at phase 171 was absorbed by a merge wave at phases 231-233. Between excursions the bottom run loses 1 cell per phase (1,777/1,779 steady phase pairs) and the runs below the wave front are frozen; after each excursion a merge wave climbs at ~0.5 runs per phase. A fast-forward check (bottom run cut short) reproduces the real excursion at phase 487 and its cascade exactly (45/45 phases) and predicts the next excursions at phases 3,321, 4,866 and 5,172 as benign. Candidate maturation rule M (the new bottom and the new a1 are merge products after every cascade, so a1 >= 6 at each excursion) holds in 4 real + 3 predicted cascades but is not derived; a proof would need a wave grammar on unbounded run words, with no busycoq template near. Not a cryptid as tested.",
"next": "No port. #37 stays parked (Dennis 2026-10-11). Asset: TM2's representation (cfgL'/cfgR', rest/RIncs, LInc/LIncs/LOv/LRst) is an exact accelerator for #37 under 'a odd'; a nonhalt proof still needs the counter-side invariant (lemma B'/rule M of the follow stage)."
}1 contract warning
- diagrams[4].window: not "cells A..B, 1 px = k cells"




