1RB1LA_1RC1RE_1RD0RD_1LA1RC_1RF0LE_1RA---
Status: CHECKPOINT_A (2026-10-10). Confidence low, so proof work waits for Dennis (priority call: Q3 on the card).
Class guess (agent / Dennis): SO structural counter. A binary counter stored between segments of 6-cell blocks, which widens by eating a finite reservoir / _
Spreadsheet notes / Discord thread: Results row 613, "Shift-overflow structural counter", with no status, notes or done-by. Not in dyuan01's Oct 1 longitudinal list. It is in mxdys's UBRRBA_TODO (Aug 24), which Dennis ruled fair game on 2026-10-10. No thread is linked and nobody has claimed it, so it is not SKIPPED. Pool: targeting.md reserve R5; rank 45 in observe.json = 40 + 5.
Viewer: https://bbchallenge.org/1RB1LA_1RC1RE_1RD0RD_1LA1RC_1RF0LE_1RA---
Observation
- Diagrams (every label field is in observe.json).
TM= this machine; all were made withtools/diagram.py "$TM"unless noted. img/records_4e5.png:--mode records --steps 4e5. Blank start, 1,162 rows, cells -59..1102.img/cycle_depth_256.png: custom pixel art fromwork/scripts/depthpng.py ../long_cycles.txt ../../img/cycle_depth_256.png 9.4e6 1.43e7 -60 1539 2 2. There is one row per cycle (272 cycles, steps 9,406,481..14,286,019). Orange marks the cells swept in that cycle.img/zigzag_closeup.png:--mode every:1 --style explore --steps 120 --from-config @work/cfg_9848484.txt --width 56 --ox 0.8. This is the real tape at step 9,848,484.img/blaze_1e7.png:--mode blaze --steps 1e7 --as-site --blaze-engine wasm.img/every400_16cycles.png:--mode every:400 --steps 265000 --from-config @work/cfg_9817765.txt --max-width 1300.img/viewer.htmlholds all views.- Direct simulation (C core): 1e10 steps, no halt. The span is cells -59..152,094 (152,154 cells) with 107,017 nonzeros, and grows like t^0.5. The left edge has been fixed at -59 since step 35,809.
- Quick_Sim:
- The default block finder picks 6, and that run proves 0 rules.
- Block size 12 with
-raccelerates well: no halt to 8.26e13 steps (steps exact, still running at that point;work/qlong.txt,work/qleft.txt; drivers inwork/scripts/qlong.pyandwork/scripts/qleft.py). - Block sizes 1, 2 and 3 died early ("lost sys.stderr").
- Tape structure (main epoch, after ~5e4 steps):
- Frozen prefix:
0^inf 1^4 (01)^11 1 (10)^4 1^7 0 1^6 (10)^3 1^6 (10)^4 1^6 (10)^3 1^6 (10)^7 1^6, then the reservoir(10)^m. - After the reservoir comes a list of segments
(101110)^n_jin either of two block phases, separated by short boundary gadgets of about 14 cells. - At the right end:
G S (110101)^n 01 C> 0^inf, with G =1^7 (01)^3 110 1^9 (01)^2 110 1^7 0and S one of four states S0..S3. - Example at 1e9: segment sizes 5, 23, 93, 374, 1496, ~6000 blocks.
- Cycle:
- From the right edge the head zigzags left: rule Z, 20 steps per block,
101110 -> 111110, carrying the 8-cell packet1^7 0leftwards. - It turns at the first boundary gadget that does not carry, then runs right through C/D: rule RS, 6 steps per block,
111110 -> 101011. - The right edge gains 4 cells per cycle.
- Counter:
- The cycle depths follow the binary ruler sequence. Levels are nested local minima of each cycle's leftmost cell, and every level is exactly every 2nd member of the level below: 37,885 of 37,885 spacings, steps 5e4..1e10, 13 levels (
work/scripts/ruler2.py,work/allcyc_1e10.txt). - Each boundary gadget holds 2 bits (4 visible states, e.g.
(10)^7 -> (10)^6 1^4 -> 10 1^6 (10)^4 -> 10 1^6 (10)^3 1^4, plus a second block phase). - Every segment grows by 1 block per 2 traversals, so the sizes go x4 per segment (x2 per bit).
- Reservoir, from the direct run to 1e10:
| step | m | right edge |
|---|---|---|
| 37,397 | 66 | 246 |
| 45,549 | 58 | 342 |
| 220,745 | 39 | 838 |
| 2,115,721 | 32 | 2,374 |
| 30,142,857 | 25 | 8,518 |
| 469,407,113 | 18 | 33,094 |
| 7,460,955,529 | 11 | 131,398 |
- From 58 on, m drops by 5 then 2 alternately, once per new top bit. Each drop comes about x4 later in time.
- qsim (block 12):
- At 3.39e12 the reservoir is gone and the gadget
(10)^7to its left is down to(10)^2. - By 7.69e12 the prefix has been eaten down to
1^4 (01)^11 1 (10)^4, with a new top gadget(11111110)^2 (10101111111010)^2 (1011111110)^3 1^12. - At 3.6e13 the counter is still running and
1^4 (01)^11 1 (10)^4is intact. No halt to 8.26e13.
- At 3.39e12 the reservoir is gone and the gadget
- Early phase: steps 0..~3.6e4 are a separate left-growing counter. Its left edge moves -10, -24, -38, -52 at steps 290, 1,358, 2,954 and 5,282, then -54 and -59. It ends by writing
1^120, which becomes the reservoir(01)^66at step 37,397. This part is finite and would be covered byinit.
Candidate rules
All checked by work/scripts/validate.py, validate_rc.py and validate_all.py (seeds 1, 2, 7). Each check builds the configuration for random n (and random context words), runs the exact step count (Z, RS, H) or runs to the cycle end (RC*), and compares the trimmed tapes exactly.
| rule | from → to | steps | sims |
|---|---|---|---|
| Z | (101110)^n <A 1^7 0 → <A 1^7 0 (111110)^n |
20n | 90/90 |
| RS | D> (111110)^n → (101011)^n D> |
6n | 90/90 |
| H | 0 <A 101 → halt (the only route: F1 is the sole undefined transition, and F is entered only from E0) |
4 | 50/50 |
| RC0 | X G S0 (110101)^n 01 C> → X G S1 (110101)^n 01 C> |
26n+108 | 100/100 |
| RC1 | X G S1 (110101)^n 01 C> → X G S2 (110101)^(n+1) 01 C> |
26n+44 | 100/100 |
| RC3 | X G S3 (110101)^n 01 C> → X G S0 (110101)^(n+1) 01 C> |
26n+44 | 100/100 |
| RC2 | X G S2 … → X' G S3 … (carry into the bits on the left) |
– | not yet an exact rule |
| D | cycle depths = binary ruler | – | 37,885/37,885 spacings (orbit, 5e4..1e10) |
| M | reservoir: m -> m-5 -> m-7 per two new top bits | – | 11/11 changes (orbit) |
S0..S3 and G are spelled out in observe.json.
The step counts were fitted as linear in n from random instances and match every instance exactly.
Not covered by any rule: - the inner boundary-gadget bit flips (the states are read off the orbit only); - the top gadget; - the early phase; - the post-reservoir regime (only seen through qsim snapshots).
Template check:
- The nearest proved machine is verify/SOC_2_4_v4.v TM204 (1RB1LA_1LC1RE_1RD0LC_1LA1RC_1RF0RB_1RA---), 3 cells away (B0, C1, E1). It is a BinaryCounter_v2 proof with different words, so it does not apply.
- The class templates SBCv6a, SBCv6a2, SBCv10 and SOBLv1-3 are 8-11 cells away.
- The closest framework is Longitudinal.v (segRLs; SOBLv3's RIncs0 k ls: h^^k passes become h^^(k*2^len)), which matches our pass-halving segment list.
Cryptid check (ground rule 6): none so far. - The counter is deterministic: binary increments with carries. - The reservoir drops are periodic (5, 2). - There is no parity- or Collatz-like branching anywhere in the observed regime. - Open: the epoch map, i.e. what an overflow into blank tape creates. If it turned out to depend on the arithmetic of the counter value at overflow, the machine would need re-flagging.
Checkpoint A (Dennis)
Card: machines/1RB1LA_1RC1RE_1RD0RD_1LA1RC_1RF0LE_1RA---/card.html. Q1 and Q2 are checks. Q3 is a priority call: more budget on the epoch map, or park?
Informal proof
Not started. Confidence is low, so the stage stops here until Dennis decides.
Non-halting needs two arguments:
- (a) Inside an epoch, the counter never produces 0 <A 101. This is plausible: within an epoch, the head reads A-on-0 only in rule Z's <A 1^7 0 and at gadget turns.
- (b) Every overflow seeds a structure of the same kind. Not observed.
Formalization log
-
Outcome
Open (CHECKPOINT_A, low confidence).
Decision (2026-10-10)
Question: Before any more agent time on R5, run one niced background qsim (block 12) for up to 24 h to watch the counter reach the left prefix, and park agent work until it reports? Answer: watch (Background qsim to the overflow; park agent work). Dennis: go with all recommendations (2026-10-10). Parked by Dennis 2026-10-10 (watch): agent work waits on a niced 24 h background qsim to the overflow, work/qleft_24h.txt.
Post-overflow follow-up (2026-10-10)
Dennis approved the follow-up after the watch run died at loop 304M (MemoryError at 6 GB). Full write-up: work/r5_followup.md.
- The overflow is now located exactly. A re-run of the same qsim configuration reproduced the 24 h run step for step (150/150 checkpoints to loop 300M).
- The old left end, with the 1^4 at absolute cells -59..-56, holds up to loop 288,010,300 (step 4,391,021,972,196,788).
- By loop 288,010,400 (step 4,391,022,056,149,912) the tape has grown to the left for the first time since step 35,809.
- After that qsim covers only about 1e4 steps per 100 loops.
- The direct run starts at loop 288M, not 286M. The dump is work/r5_pre_overflow.json: step 4,390,707,259,988,964, 100,660,080 cells, every block plus a directed-head string. Loop 286M lies 6.1e13 steps before the overflow, out of reach of a 2e13 run; that dump is kept as work/r5_loop286M.json.
- Checks:
- The expansion matches tools/sim.py run from blank at three loops.
- The C driver work/scripts/r5run matches qsim exactly on every reference tested: 19/19 early, and 3/3 over the first 1e10 steps from the dump.
- The long run itself verifies all 597 qsim dumps up to loop 300M, which includes the overflow.
- Running (detached, niced, 1 core):
- 2e13 steps from the dump, logging every 1e10 steps to work/r5_post.log: step, head, span, nonzeros, leftmost 300 and rightmost 200 cells, and a HALT line with the exact step if it halts.
- Checkpoint every 1e12 steps: work/r5_post_ckpt.bin, resume with work/scripts/r5_post_launch.sh resume.
- ETA about 22 h: around 2026-10-11 21:30 PDT.
- First result (23:45 PDT, rel step 4.8e11):
- All 597 qsim references matched exactly, across the overflow.
- The overflow erased the old tape. Nonzeros fell from 8.4e7 to 1,681 within 3.7e8 steps.
- What is left: an island near cell 2.5e7, 1^7 at the old right end (about 1.0066e8), and a new structure growing from a new left edge at absolute -62, then -67.
- It has 4.0e5 nonzeros by rel 4.7e11. Its left edge is still moving, as in the first epoch's early phase.
- Preliminary reading: a reset into a fresh epoch. This run probably shows how the new epoch is built, but not its overflow (see work/r5_followup.md §5).
- Read the log with python3 -B work/scripts/r5_post_view.py. Agent work stays parked until the run reports.
Halting hunt: exact model (2026-10-13)
Pick H-4 of the halting hunt (Dennis's 10-13 hunt approval). Dennis, one line: the epoch-map stage (the 10-10 option you did not pick, "for Dennis to decide" in work/r5_followup.md) was launched tonight as simulation of our own STUCK machine; nothing beyond simulation was started.
Outcome: no halt up to step 5.636e76 (10^76.75) (exact model, validated against direct simulation on every anchor reached). Not a kill and not a halt.
What was built (work/exact/)
xm.py: an exact accelerated simulator. Nothing is fitted; every rule comes from the transition table.- Tape = tokens: literal cells, or runs
w^n(word of period 1..16, exact big-integer count). - Literal cells: plain TM steps.
- Shift rules: when the head enters
w^nin state q, the TM is run on one copy of w plus k context cells (k = 0..24). If the head leaves on the far side in state q and the region now readsC w'(resp.w' C), induction givesw^n C -> C w'^nin n*s steps. Constant runs with no rule for w also try w^2..w^4. - Peeling one copy when no rule exists.
- Memos: a symbolic run of the same engine over a suffix region
[b, E)of the tape. Counts >= 16 become symbols, the right of the region is treated as blank (E = the first long 0-run), the run starts with the head about to enter run r leftwards and ends the first time it is about to enter run b leftwards. Every peel and every nested memo adds an affine constraint. A memo stores the result tokens (affine counts), the step count (affine), the blank cells it uses and its constraints. It is applied only when the region shape matches exactly and every constraint holds; a memo whose symbolic run reaches a halting transition is discarded, so halts are always met concretely. - The recursion (memo for b uses the memo for the next run right of b) is what batches the binary counter: each level costs about 4 applications of the level below.
- Drivers:
far2.py(far run with JSON log + state pickle every 5 min;--tm,--ckpt,--resume),anchors.py(exact comparison with R5CFG references),postcheck.py(comparison with an r5run continuation),loadcfg.py(tokenises a 1e8-cell checkpoint exactly),test_blank.py.
Validation (all exact: state, head, the whole nonzero tape, step count)
- From the blank tape vs
tools/sim.py(C core): 1e2 .. 1e10 steps, with and without memos. - From the blank tape to the qsim pre-overflow dump (
work/r5_pre_overflow.cfg, step 4,390,707,259,988,964): the full 100,660,080-cell tape. The model gets there in about 15 s. - Across the first overflow: 99/99 qsim references (
work/r5_refs.cfg, every 6th, loops 288,000,100 .. 298,600,000, steps up to 4,391,173,976,288,409; anchors2.jsonl) and 97/97 in an earlier pass (every 4th; anchors1.jsonl). These references were themselves verified by the direct C run (597/597). - After the epoch-2 checkpoint (
work/r5_post_ckpt.bin, rel 2e13, step 4,410,707,259,988,964): a fresh direct C continuation (scripts/r5run, 3e11 steps,exact/r5run_post.jsonl) vs the model started from the checkpoint: 30/30 log points (state, head, nonzeros, outermost 1s, every 1e10 steps) and the full tape at step 4,411,007,259,988,964 (exact/r5_post_2p03e13.bin). Both engine versions (the one used by the long runs,xm_v1_snapshot.py, and the currentxm.py) pass (postcheck_v1/v2). - Blank tape to the epoch-2 checkpoint in one run: the model from the blank tape reaches step 4,410,707,259,988,964 (rel 2e13, past the overflow) in 84 s and matches the whole 100,663,701-cell checkpoint tape, head and state (
exact/anchors4.jsonl; current engine). An earlier pass (anchors3) matched the tape and state but failed the head check because anchors.py read the packed checkpoint's head as an index instead of a position (head minus pos0); fixed, then anchors4 passed.
The old runs, closed
- Direct C run from loop 288M (work/r5_post.log): finished its 2e13 steps (2026-10-11), no halt, 597/597 references.
- Seeded qsim
reports/halting-hunt/parked/r5/r5q.py(block 24): hit its 4 h cap at 21:36 at loop 194.4M, step 4,969,937,411,350,948, no halt, 0 prover rules.
Epoch 2, as the model sees it
- At the checkpoint (rel 2e13) the tape is a static left part, several finished sub-counters separated by period-8 runs (
(11101010)^n/(11010101)^n), the active counter, and the epoch-1 debris: short blocks at x4-spaced positions (zero gaps 12,819 / 73,715 / 294,899 / 1,179,635 / 4,718,579 / 18,874,355 cells) and1^7at the old right end. - Each sub-counter is the epoch-1 kind of binary counter (segments
(110101)^n, x4 per segment, gadgets of about 100 cells). The finished ones end with a big segment S followed by(11010101)^~2S: S = 196,607 / 786,421 / 3,145,733 with runs 393,167 / 1,572,810 / 6,291,263. Reading: a sub-counter runs until its right end meets the next debris block, then its last segment is converted and a new sub-counter, one level bigger, starts to its right. - Past the last debris the active counter grows freely. Its fuel is the run
(11010101)^6,291,263to its left, eaten as new top bits are made (as epoch 1 ate(10)^66): it went 6,291,263 -> 6,291,195 -> 6,291,133 -> 6,291,121 -> 6,291,118 at steps 10^44.95, 10^59.70, 10^73.14, 10^75.84, 10^76.61: steadily about 4.6 copies per decade of steps. - The finished sub-counter to its left (segments 9 .. 3,145,739) is incremented while this happens: its low gadgets flip
(10)^9 <-> (10)^1and its last segment grows 3,145,733 -> 736 -> 739 over the same span. So epoch 2 is a counter of counters. - No overflow of the active counter happened in the run. At the measured rate its fuel lasts about 6.29e6 / 4.6 ~ 1.4e6 decades: the next decision point (the active counter's overflow) is projected near 10^(1.4e6) steps (an extrapolation, not a model result). The left counter's own overflow is also far off (ten levels; its lowest segment grows by 3 per ~14 decades).
- Cryptid check: none. Everything seen is binary counting with periodic fuel use; no parity- or Collatz-like branching.
Far runs
far3.jsonl(from the rel-2e13 checkpoint): 3600 s, reached step 5.636e76 = 10^76.75 exactly (77 digits, first digits 563690473834), no halt; 546 tokens at the end. Engine as of 22:13 (the current one minus LRU memo eviction; caching only). State pickles in far3_s*.pkl and far3.jsonl.state.pkl (resume: far2.py --resume). The run was left going to its 90-min cap (23:43), so its log may end a little further than this.farc1.jsonl(first engine version, same start): 2.29e45 steps in 945 s, no halt (stopped and replaced by far3).- Speed limit: each new top bit of the active counter costs a few dozen driver events and adds ~2 tokens, so the run gained about 0.05 decades per second at first and only ~0.02 decades per minute past 10^75 (500+ tokens; the memo cache is flushed every ~30k memos). Reaching 10^(1.4e6) needs a further level: a closed form for "one more top bit" (counter with k bits -> k+1 bits, fuel -c), which the memo framework cannot express because the token count changes.
Line 43 (1RB1LF_1LC1RB_1LF1LD_1LE0RD_1LB---_1LA0LA, claimed 2026-10-13)
- Same table as R5 started from D, mirrored; it has its own orbit from the blank tape. The model is generic in the table.
- Validation: model from blank vs
tools/sim.pyat 1e5, 1e7 and 1e9 steps: exact (test_blank.pywithTMX=<43>). exact/far43.jsonl(35 min from blank): step 4,689,505,113,775 (4.7e12), no halt.- The tape is the mirror image of R5's epoch-1 counter:
(101011)segments, x4 per level, growing to the left (left edge at -3.3e6), with long runs(1)^1830and(1)^439in the prefix on its right, where R5 had its(10)^66reservoir. Its first overflow was not reached. The model is slower on 43 (a messy start with many failed memo builds), so it needs a longer run.
Certification
None possible at this depth. No halt was found, so there is nothing to certify; a nonhalting proof would need the epoch-2 counter-of-counters structure formalised, which is far beyond the current templates. The model's rules (shift rules + memos) are exact rewrites, so a found halt could be certified W5-5 style by replaying the real TM from a configuration the model reaches shortly before it (expand a window of +-N cells around the head).