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

1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): Sync bouncer counter: TM4's binary counter + 3-block bouncer with a moving front / _ Spreadsheet notes / Discord thread: Results row 921, "Sync bouncer counter", no status/notes/done-by. Archive: "does not halt in 2e13". No xlsx comment. On dyuan01's Oct 1 longitudinal list (technique filter, not a claim; ask before submitting, message in observe.json) and mxdys's UBRRBA_TODO (fair game per Dennis). Viewer: https://bbchallenge.org/1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---

Observation

Diagrams: img/records_2.7e6.png (most telling), img/every60_Q8_front_conversion.png, img/blaze_1e7.png, img/default_site.png; all views in img/viewer.html.
How each card diagram was made (re-run 2026-10-10: byte-identical PNGs; label fields in observe.json come from these runs). TM = this machine, all via tools/diagram.py "$TM":
records_2.7e6.png: --mode records --steps 2.7e6 --scale 2. Blank start; one row per new left/right record (1,173 rows); cells -21..1151.
every60_Q8_front_conversion.png: --mode every:60 --steps 110000 --scale 2 --from-config "<canon.build('Q',8,129,1,24,29)>" (work/scripts/canon.py). That config equals the real tape at step 74,114 (checked), so this is a mid-run picture of steps 74,114..184,114, one row per 60 steps, cells -17..377.
blaze_1e7.png: --mode blaze --steps 1e7 --as-site (summary work/dg3.json). default_site.png: --as-site (work/dg1.json).
Simulated to 3e9 steps with no halt: span 48,013 cells, 22,929 nonzeros, span ~ t^0.5. qsim: block size 5, 0 rules.
Notation: C_k(n) = n in k bits, MSB first, 1 = 1010, 0 = 0010 (TM4's d1/d0).
Skeleton (every right-edge visit in state C):
P(k,n,X,z) = 0^inf C_k(n) (00111)^X (10111)^z 00 C> 0^inf
Q(k,n,x,y,z) = 0^inf C_k(n) (00111)^x 111 (00111)^y (10111)^z 00 C> 0^inf
Coverage: 4,711 of 4,722 right-edge C records to 1e9 are exactly P or Q. The other 11 are mid-conversion or the start.
Cycle (records view): during P, each bounce adds a B block (10111). On overflow, the front (111) starts at the left and moves right 2 A blocks per edge visit. When the front reaches the B blocks, they all turn into A blocks. Then the next cycle runs at k+1.
Phase boundaries (full list in observe.json history):

step	state
35,105	P(7,99,26,0)
72,213	P(7,127,26,28)
74,114	Q(8,129,1,24,29)
108,318	Q(8,165,25,0,41)
172,672	P(8,208,67,0)
518,654	Q(9,353,65,1,80) (odd)
1,101,764	Q(10,537,17,131,0)
1,093,007,525	Q(15,16502,79,4632,0)
2,318,632,923	P(15,25768,7028,0)

Candidate rules

t(n) = number of trailing 1-bits of n.

rule	from → to	condition	steps	sims
R1	P(k,n,X,z) → P(k,n+1,X,z+1)	n+1 < 2^k	32X+32z+16t(n)+47	65/65
R2	P(k,2^k-1,X,z) → Q(k+1,2^k+1,1,X-2,z+1)	X≥2	–	25/25
R3	Q(k,n,x,y+2,z) → Q(k,n+3,x+2,y,z+1)	n+3 < 2^k	96x+32y+32z+16(t(n)+t(n+1)+t(n+2))+197	65/65
R4	Q(k,n,x,0,z) → P(k,n+z+2,x+z+1,0)	n+z+2 < 2^k	–	25/25
R5	Q(k,n,x,1,z) → P(k,n+2z+7,x+z+4,0)	n+2z+7 < 2^k	–	25/25
R4o	Q(k,n,x,0,z) → Q(k+1,2^k+1+3m,1+2m,x+z-1-2m,0)	m=n+z+2-2^k ≥ 0	–	25/25 in regime
R5o	Q(k,n,x,1,z) → Q(k+1,2^k+1+3m,1+2m,x+z+2-2m,0)	m=n+2z+7-2^k ≥ 0	–	50/50 in regime

How the rules were tested: build the concrete configuration for random parameters (k=2..12, small/medium/large values), run to the next canonical right-edge C configuration, and compare exactly. The step formulas come from exact rational fits on 40 runs each, with residual 0.
Regime: "in regime" means x+z ≤ 2^(k-1). Outside it, R4o/R5o fail on 2/25 and 4/25 random instances: the head breaks through the counter, and Q(4,8,400,0,180) even halts. The invariant must exclude this.
Real orbit: all 4,709 consecutive canonical transitions to 1e9 match the rules. The only exception is the start at step 110 (X=1).
Phase-level map: built from R1-R5o and started at Q(5,17,1,2,2) (step 1,507), it reproduces all 36 phase boundaries in the observe.json history from there to 2.3e9 steps (18 phase starts plus the 18 phase ends between them), including the two beyond 1e9. The 2 earlier history rows come before the map's start. (Re-checked 2026-10-10 with work/scripts/abstract.py.)
Branch = parity of X (X grows ~3X/2 + Z), so the branch sequence is pseudo-random: ABoAABoBAAABo...
Why this is not a cryptid: run to k=3000, and with branches forced all-A, all-B or random to k=600, the map stays in regime:
X/2^k stays in [0.20, 0.29];
overshoot m/2^k ≤ 0.031;
Q-phase counter slack ≥ 0.28·2^k. So halting does not depend on the parities.
Template check (SBCv7 TM4 / TM37, which differ only in F0): partly.
All three machines agree from blank up to step 211.
TM37's overflow form 0^inf 101000 C> (1010)^(k+1) 1010010 r is reached 5/5 from TM37's configurations.
TM4's BigStep holds in only 2/8 cases, exactly those where TM4 never reads F0.
Verdict: the counter carries over; the right-side words are new.
SBCv11 (2 transitions away) uses a column/particle framework (hp=(D,00111)); it may be useful for the right side.

Checkpoint A (Dennis)

Questions in observe.json (front reading; odd-X branch as a case split; fresh Longitudinal proof vs copy-modify).

Informal proof

Done 2026-10-10: proof.md (checker check_proof.py, log work/check_proof.log, ALL CHECKS PASSED in 6 s). - The moving head carries 001 (<A 001 / 001 E>, TM4's hL/hR). Blocks are A = 00111 / A' = 00101 and B = 10111 / B' = 00001 (left / right form). - 21 shift rules, each exact on its window. They give CTR, OV, the front gadget QC (FL, FR1-FR3) and the conversion gadget (even FR1^(z+1); odd FR1, FR2, (FR4, FR2)^z, FE1-FE4), then FE0. R1-R5o are derived from these. - R4o/R5o domain: m >= 0, y_final >= 1, 3m <= 2^k-2. - Cycle map S(k,Y,Z) -> S(k+1, F_N(Y,Z)): even (3j+Z, N-3-4j-Z), odd (3j+3+Z, N-8-5j-2Z). - Invariant: the hexagon 8Y>=N, 8Y<=3N, 3Z<=N, 8Z>=-N, 4Y+2Z>=N, 20Y+16Z<=9N, for N>=64. Both branches preserve it, so this is not a cryptid. - init: c0 -->(17215) S(6,16,0) = Q(7,65,1,16,0). - Rule-only runner from step 1507 reproduces all 36 history rows, configuration and exact step, up to 2.3e9. - 2026-10-10 skeptic revision (7 minor gaps, all accepted; Review log at the end of proof.md): on the invariant 2Y+Z <= 27N/32, so an even conversion never overflows. The cycle lemma gains hypothesis (d), and R4o is now only a remark: R5o is the only overflow-during-conversion lemma to formalize. The R5o domain is split into m = 0 and m >= 1. Template list: SBCv7 TM1/2/3/4/18/37 all differ only in F0. Rocq scratch checks: 21 shift rules (es), ALs/BLs/ARs (manual induction, not ind), init (esx 2.1 s). Status CHECKPOINT_B.

Formalization log

Outcome

Card data pass (2026-10-10)

Figures on the card: Fig 1 = img/records_2.7e6.png, Fig 2 = img/every60_Q8_front_conversion.png, Fig 3 = img/blaze_1e7.png, Fig 4 = img/default_site.png. Figs 1-2 are the primary figures, shown beside the checkpoint.
The card's mechanism is cut to 3 bullets. The full list before the cut:
Left: binary counter C_k(n), k bits MSB first, 1=1010, 0=0010 (TM4's d1/d0); +1 per bounce.
Right: A blocks 00111, one 111 marker (the front) in Q, B blocks 10111 at the right edge.
P phase: every bounce adds one B block until the counter is all 1s.
Overflow: counter gains a bit; front starts at the left and moves 2 A blocks per edge visit.
Front reaches B: all B blocks turn into A blocks (1 bounce each if X even, 2 if odd); next cycle at k+1.
Checkpoint questions are now yes/no questions about the figures. Moved off the card (strategy calls, not figure reading; settle them in proof.md / Checkpoint B):
"OK to build a fresh Longitudinal proof (TM4 counter lemma + new right-side words) rather than copy-modify TM4/TM37?"
Correction: the odd-X event (two fronts back to back, R5o) is about two-thirds down records_2.7e6.png: Q(9,353,65,1,80) at step 518,654 is record row 772 of 1,173, and Q(10,537,17,131,0) at step 1,101,764 is row 786. The old question said ~55% height.

Kill

2026-10-10: KILLED_NONHALT. Kill file 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v (502 lines, sha256 f91548736cf9715968e94b7161d9e707332b09f8a3fd7ebf653ebc8f177000d2) proves top-level Lemma nonhalt: ~halts tm c0..
tools/check_kill.sh: PASS 3 times on the same sha256.
Formalizer, 12:10:08Z: compile 6.4 s, coqchk pass 2.0 s (rocq/check_kill.out).
Independent audit, --json: 17/17 checks pass, compile 6.8 s, coqchk pass 2.0 s. The audit also confirmed the string is line 681 of data/holdouts/2026-10-07_778.txt (holdouts.py contains, grep -nx, and od -c of the literal). It read the file end to end and found nothing suspicious. Its own simulation reaches CfgF 5 0 16 0 = Q(7,65,1,16,0) at exactly step 17,215, with no halt in 2e7 steps.
Fresh human-readable run for the submission, 12:13:36Z: compile 7.2 s (native on), 0 assumptions (closed), coqchk pass 2.2 s.
The proof follows proof.md:
21 shift rules (es) and their repeated forms;
Fixpoint ctr with CTR/OV, plus the round trips RT/OVRT;
QC, R1–R3 and Pfin;
the conversion as one induction over Inductive Gad (ConvNo, PostOV, ConvOV), which gives R4, R5 and R5o;
cycle_step on the index (k,i,y,z) with Inv = the hexagon, then nonhalt = multistep_nonhalt + progress_nonhalt_cond. It imports Individual62 only (no Longitudinal). Details: rocq/log.md, atlas/rocq-notes.md.
Submission package: submission/.
The .v, unchanged.
proof.md, a copy whose status lines are updated to "fully formalized", with a new §6 subsection mapping sections to lemma names. The working proof.md is untouched.
check_kill.txt (the 12:13:36Z run), README.md.
discord.md, a draft of 1,639 characters plus <LINK>. Not posted.
Before posting:
Re-read dyuan01's Oct 1 longitudinal thread. The machine is on that list, which is a technique filter, not a claim (reports/discord-drafts.md).
No Checkpoint B notes from Dennis were on file when this was packaged. If he adds any, fold them into proof.md and the submission copy first.
Neighbours: SBCv7 TM1/TM2/TM3/TM4/TM18/TM37 (same table except F0) were already solved. It is the only machine on the 778 list with this A–E table.