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

1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): binary counter over a list of blocks with a re-pairing overflow (TM21-like Skelet 1-like Class 2) / _ Spreadsheet notes / Discord thread: Results tab: class only, no status/notes/links. Not on any tab or Discord list. Same transition table as two other holdouts (only the start state differs): - 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- = this table started in our B (rename A..F → E,A,B,C,D,F). Level 1 tab, hipparcos, Discord thread https://discord.com/channels/960643023006490684/1432566675533992019 (2025-10-28). Identical trajectory to 1e9 (checked). - 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- = mirror of this table started in our C (Eqv_v2.v tm' of TM688/TM2137). Viewer: https://bbchallenge.org/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---

Observation

Candidate rules

Digits indexed from the head (0 = next to the near block) for M_k; from the left for O.

M_k (carry, k = # trailing 1-bits):
  l (10)^uk 0^2 (01)^vk [(10)^ui (01)^vi]_{i<k} (10)^a 0^3 (10)^b B> 0^inf
  --> l (10)^(uk+1) (01)^(vk-1) [(10)^ui 0^2 (01)^(vi-1)]_{i<k} (10)^(a+1) 0^3 (10)^(b+2) B> 0^inf
  steps 32 + 8a + 8b + 8·Σ_{i<k} ui + 4·Σ_{i≤k} vi          [84/84 random, exact steps, k=0..5]
O (overflow, all bits 1, n ≥ 1 digits after the leading 10 01):
  0^inf 10 01 [(10)^ui (01)^vi]_{i=1..n} (10)^a 0^3 (10)^b B> 0^inf
  --> 0^inf 10 01 00 (01)^u1 [(10)^(vi-1) 0^2 (01)^u(i+1)]_{i=1..n-1} (10)^vn (01)^a (10)^(b+3) 0^3 10 B> 0^inf
  steps 89 − 4n + 8a + 20b + 4·Σui + 8·Σvi                  [118/118 random (70 exact steps), n=1..7]
init: 0^inf A> 0^inf --142--> K(10 01, (10)^3 01; a=2, b=1)    (from B: 122 steps, (1,2); from C: 101 steps, (1,1))
sweeps: B> (01)^n --2n--> (10)^n B>;  (01)^n <D --2n--> <D (10)^n   [20/20]

Template check

SBCv6.v TM21: 10/12 transitions differ (best rename/mirror); its S' configs do not recur on this machine (0 genuine hits in 2e5 steps from S' in every state). Mechanism matches (LIncs ≈ carries, Ov ≈ re-pairing overflow, BigStep), encoding and invariant do not: here digits run out and merge, so TM21's LWF (2^len ≤ m) fails. Sk1like_TC_v2 TM1: 9/12 differ; usable only if the list dynamics turn periodic.

Checkpoint A (Dennis)

Informal proof

Here ubar = u + R1 and vbar = v − R, the values at the next overflow, with R_j = 2^j − 1 − U_j. The orbit cycles A→B→C→A. - The hand proof of closure uses three exact facts: F1 (touch), F2 (drop algebra) and F3 (overflow). - Init: K((1,1,2);8,5) at step 483, in class A. Twins: start B reaches K((1,1,10);8,1) at step 732; start C reaches K((1,1,9);8,1) at step 687. Both are class A. - check_proof.py: all 10 checks pass. They include 600k random INV states (not just reachable ones), each stepping back into INV, and 2,842 of them stepped on the real machine. - Status: OPEN at informal_proof. Next: Rocq. - 2026-10-10, skeptic revision: the review found the proof sound, with 1 major and 6 minor gaps, all fixed (Review log in proof.md). The major gap: M and O are now derived, not sampled. They are chains of 20 window lemmas (proof.md §2.1–2.3): - shift lemmas S1–S6, including the 2-cell back-bounces S5 C> 11 (01)^n → (10)^n C> 11 and S6 0 B> (10)^n → (10)^n 0 B>; - 14 finite turns T1–T14; - digit lemmas Lb, Lf, Rb, Ro.

M's head path is one dip into the 0^3 gap, one long left sweep to d_{j*}'s 00, then a rightward bounce pass. The "4 right-edge records" above counts right-edge maxima, not excursions. check_proof.py checks 11–13 (lemmas exact; M/O chains link by link on the real machine) all pass. Status: CHECKPOINT_B. Next: Rocq.

Formalization log

Outcome

Card data pass (2026-10-10)

The card now shows at most 3 short mechanism bullets and yes/no questions that point at figures by number (primary figures first). The text they replaced is kept here. - Figure order on the card: Fig 1 = img/counter_from_K.png, Fig 2 = img/records_3e5.png, Fig 3 = img/records_1e7.png, Fig 4 = img/default_site.png, Fig 5 = img/blaze_1e7.png (Figs 1-3 primary). - Mechanism, full observer version: - Tape = list of digits (10)^u J (01)^v (J = 00 is bit 0, empty is bit 1), then a growing (10)^a 000 (10)^b block at the right edge. - Every 4 right-edge records = +1: the head runs left to the first 0-bit (ruler-depth carry), flips bits, each touched v drops by 1. - All bits 1 -> overflow: head runs to the far left (the only left records, 3 cells each); blocks re-pair, new digit i = (v_i-1, u_(i+1)). - A digit whose v runs out fuses with its neighbour (list shrinks); each overflow adds one. Rules alone reproduce all 54 overflows to 1e9 and run to 1e15 without getting stuck. - Same table as 2 other holdouts (hipparcos's Level-1 twin, an Eqv twin) started in states B and C: one proof, 3 inits. - Checkpoint questions before the rewrite (some were decisions, not questions about a figure): - counter_from_K.png: do the excursion depths read as a binary counter (shallow, deeper, shallow, deepest) ending in one full run to the left edge? - records_3e5.png: OK to model the tape as a list of (u, bit, v) blocks (the dashed walls) with an overflow at each band break? - OK to post the Discord question to hipparcos before any proof work on this table?

Kill