/machines/1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---/notes.md · raw

1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): binary counter with a re-pairing overflow. It is kill #11's table, mirrored and started in #11's state D (Skelet 1-like Class 2) / _ Spreadsheet notes / Discord thread: - Sheet: Results tab, class only, with the note "Machine with the most common transitions". Level 0 tab ("not individually worked on"): "Fun fact: machine with the most common transitions". No status, no links, no strikethrough. - On every snapshot from 2024-06-14 to 2026-10-07_778. A singleton group in 2026-10-07_eqv_1590.txt. - Not on the UBRRBA (mxdys) or longitudinal (dyuan01) lists in data/discord/, and not in reports/discord-drafts.md. Not claimed, so not SKIPPED. Viewer: https://bbchallenge.org/1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---

Observation

#11's notes listed the B and C starts but missed this one. The eqv_1590 file keeps all four in separate groups, so a kill of one does not cover the others. - 1e9 steps from blank: no halt. Span −76,078..166 (76,245 cells), 38,119 nonzeros. - Left edge ~2.4·t^0.5. Left records come 2 per left-edge visit and 4 per counter increment (76,078 by 1e9). - The right edge grows +3 cells per overflow (166 right records, in triples, 52 overflows by 1e9). - qsim (qsim.jsonl): block size 2, 0 prover rules, 2,180 failed proofs, so there is no acceleration. Same as #11. - compress (scripts/compress_track_1e7.txt, aligned at left records) gives the head-local skeleton 0^inf <C (01)^a 0^3 (01)^b r, with a +2 and b +1 per visit. That is the K block below, with the roles a↔b swapped. - Images (labels in observe.json → diagrams): - img/default_site.png: the site view; - img/cycle_10050.png: one counter cycle from the natural K at step 10,050, every 20 steps. Its start config is in img/cycle_from_10050_start.txt, which equals the run's tape at that step (checked); - img/records_L_3e5.png: left records to 3e5; - img/blaze_1e7.png; - img/viewer.html. - K-config (head at the left edge, state C, reading blank; it occurs at every 4th left record): K(d_1..d_m; a, b) = 0^inf <C (01)^b 000 (01)^a d~_m .. d~_1 1001 0^inf, with d~ = (10)^v J (01)^u. - J = 00 is bit 0; J empty is bit 1. - d_1 sits next to the fixed 1001 (MSB) and d_m next to the block (LSB). - This is exactly #11's K(d; a, b) = 0^inf 10 01 d_1..d_m (10)^a 0^3 (10)^b B> 0^inf, mirrored, with #11's B = our C. Digit (u, β, v) means the same thing in both. - Between two K-configs there is one intermediate visit, <C (01)^(b+1) 0 (01)^(a+1), in the Y form.

Candidate rules

All in this machine's orientation. The scripts are in scripts/.

init:  0^inf A> 0^inf --82--> K(; 3, 1) --133--> K((1,1,3); 4, 1)  (step 215, INV class A)        [exact, direct sim]
M_k (carry; j* = last bit-0 digit, k = m - j*):
  <C (01)^b 000 (01)^a [(10)^vj (01)^uj]_{j=m..j*+1} (10)^v 00 (01)^u  P  1001
  --> <C (01)^(b+2) 000 (01)^(a+1) [(10)^(vj-1) 00 (01)^uj]_{j=m..j*+1} (10)^(v-1) (01)^(u+1)  P  1001
  steps 32 + 8a + 8b + 4v + sum_{j>j*}(8 uj + 4 vj); needs v >= 1, uj, vj >= 1 (j > j*), a, b >= 0
  v = 1: the digit (u+1,1,0) drops, i.e. the same string is re-read as fused with the next digit / the block   [240/240]
O (overflow; all bits 1; m >= 1, all u, v >= 1, a >= 1):
  <C (01)^b 000 (01)^a [(10)^vj (01)^uj]_{j=m..1} 1001
  --> <C 01 000 (01)^(b+3) (10)^a (01)^vm [(10)^uj 00 (01)^(v(j-1)-1)]_{j=m..2} (10)^u1 00 1001
  steps 89 - 4m + 8a + 20b + 4 sum u + 8 sum v                                                                [120/120]

The K at step 215 is class A: top (1,1,3), S ≥ 1, ubar odd, vbar ≥ 1. The earlier K(; 3, 1) at step 82 has no digits, so it is not in INV, which is why the init stops at 215. - scripts/init_from_D.py scans the K-configs for all four start states of #11's table. It reproduces #11's recorded inits (start A: 483, class A; B: 732; C: 687) and finds start D: 215, class A. - Pre-overflow history (observe.json → history, 36 of 52 overflows): structured values such as 2^k−1, 2^k and 3·2^k−2, and the classes alternate A/C at overflows. There are no parity coin-flips.

Template check

Cryptid check (ground rule 6)

Not a cryptid. The dynamics are an exact binary counter with deterministic carries and a deterministic re-pairing. There is no parity-of-growing-number branching that decides halting. Halting would need a carry to reach a bit-0 digit with v = 0, and #11's INV, already proved in Rocq for this table, rules that out. Here INV holds from step 215 on.

Checkpoint A (Dennis)

Informal proof

2026-10-10: proof.md written (stage informal_proof, status OPEN; Checkpoint B pending, non-blocking). - Written in this machine's own orientation: - K = 0^inf <C (01)^b 000 (01)^a d~_m .. d~_1 1001 0^inf, with d~(u,β,v) = (10)^v [00] (01)^u; - M and O derived as chains of the 20 window lemmas (#11's names, mirrored); - #11's §3 INV and closure verbatim (it is stated on triples only); - init: blank -82-> K(;3,1) -133 (O at m=0)-> K((1,1,3);4,1) at step 215, class A (T = 0, tight); - §0 tabulates the four holdouts with this table (starts A/B/C/D, inits 215/483/732/687). - check_proof.py, self-contained, 13 checks. ALL PASS with the default seed (check_proof.out) and with --seed 2026 --tm-steps 1e9 --orbit 1.2e6 --induct 6e5 (check_proof_long.out, about 90 s). The long run includes: - the real-machine closure at all 18,977 macro boundaries to step 999,982,947; - link-by-link M/O chains (37,220 + 9,996, including m = 0); - 600k random-INV inductiveness; - the 4-holdout relabeling search over the 778 list. - rocq/plan_check.v (1.2 s) confirms the mirror dictionary of proof.md §6. These compile: - S1–S6, T1–T14, Lb/Lf/Rb/Ro; - the mirrored K; - init: c0 -->* K [d1 1 3] 4 1 (solve_init). - Correction to "Formal routes (a)" above: list literals are not reversed under the mirror, because busycoq sides are nearest-cell first.

2026-10-10, skeptic revision. Verdict: sound, 2 minor gaps, no fatal or major one. Both are resolved; the Review log is at the end of proof.md. - Gap 1: the three rule specs (and LbS/RbS/RoS/chunkA/chunkC/chunkO/Ozeq) are not yet proved in Rocq on this table, so the carry-over of #11's step/nonhalt was conditional on keeping the spec statements verbatim. - Now Rocq-checked: rocq/abstract_check.v (built by scripts/make_abstract_check.py) puts #11's abstract part, verbatim, over this machine's plan_check.v (tm, K, init), with #11's three spec statements as its only section hypotheses. - Coq 8.20.1, 8.9 s, exit 0. nonhalt : M_spec -> Mdrop_spec -> O_spec -> ~ halts tm c0 for this string, closed under the global context (rocq/abstract_check.out). - New check 14 in check_proof.py (16/16, with 3 negative controls) makes the interface mechanical. #11's abstract part uses exactly tm, dg/d0/d1, K, map0, map1, Oz, Oout, the three specs and init, with no unfold K. proof.md §6 quotes the specs verbatim, and abstract_check.v is the verbatim assembly with a matching compile record. - Oz must also be copied verbatim; the reviewer's list omitted it. - Gap 2: the stale "skeptic review not done" bullet is replaced by a record of the review's independent checks (0 failures). - Re-run: check_proof.py ALL PASS, 14 checks, default and long. plan_check.v recompiles in 1.19 s. - Status: CHECKPOINT_B (stage informal_proof). Not a kill. Next: port the 3 specs and their supports name for name, swap them in for the section hypotheses, and run check_kill.

Formalization log

Outcome

Kill