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

1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): Skelet 1-like Class 2. A binary down-counter on a list of pairs, with overflow re-pairing (same family as SBCv6 TM21) / pending Spreadsheet notes / Discord thread: Results row 1278: class only, with no status, notes, source or link. The machine is not on any other tab, not in data/discord/*, not in busycoq at 0940bb9 (or solved_index.tsv), and not in Sk1Machines.v, which covers Class 1 only. Memo Q3 (does the Sk1 list cover Class 2?) is still open; the paste-ready question is in observe.json discord_check. Viewer: https://bbchallenge.org/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---

Observation

At 1e9 steps: 67,343 cells and 33,665 nonzeros. The left edge grows as ~2.1·t^0.5; the right edge barely moves (157 → 181 between 1e8 and 1e9).
Quick_Sim (block size 2) proves 0 rules. rulefit coverage is 1% and its output is unusable (see Outcome).
Diagrams in img/ (exact start/rows/window/colours: observe.json diagrams):
cycles_phase_1e7.png: one row per decrement to 1e7 steps, every 4th (odd) cell; made by scripts/diagram_cycles.py;
blaze_1e8_speed.png: Blaze speed mode (one snapshot per 131,072 steps, one cell per 16);
every1e6_1e9.png: one snapshot per 1e6 steps to 1e9, every 16th (odd) cell;
explore_3dec.png: 3 counter cycles from a constructed config (counter value 12);
default_site.png, viewer.html.
Reading the sampled views: pair blocks always have even length, so every (10) run in a pair list shares one cell parity. Drawing only every 2^k-th odd cell turns each (10) or (01) run into a solid band, and a colour edge is a pair boundary. Between counter-at-0 events the digit blocks stay put (vertical edges) and the (10)|(01) splits move 2 cells per borrow (slanted edges). At most counter-at-0 events the roles swap: the new digit blocks sit where the old splits were (checked at every such event to 3e6 steps; events that lose a pair, merges and EndLast, keep the old blocks). Which colour means (10) flips from epoch to epoch: pairs start on odd cells at steps 1.85e5 and 1.29e6, on even cells at 6.3e5 and 7.9e6.

Canonical config, taken at a left record in state A whose tape starts (10)^h 11001:

K(h; (p_j,q_j,d_j)_{j=1..L}; T) = 0^inf <A (10)^h 11001  Π_j (10)^p_j (01)^q_j s(d_j)  T 0^inf
s(1) = 0001, s(0) = 0010          T ∈ { '' , (10)^t 1 , (101)^2 (01)^k }

Digits d_j form a binary number V; the least significant digit is next to the head.

Epoch starts (Ov events), with h = 2:

step	L	V	p1,q1	last pair
34,137	4	14	47,56	18,2
868,551	6	62	191,236	45,2
11,309,893	8	254	767,956	90,2
145,833,457	10	1022	3071,3836	98,2
466,254,879	11	2046	6143,5628	100,2

Candidate rules

All rules are in K notation; directed-head forms are in observe.json. Each was tested from random concrete configs: small (1–3), medium (≤25) and large (100–400) values, all h mod 4, and every borrow depth.

rule	when	effect	random checks
Dec	first d=1 at pair k	pairs 1..k: p+1, q−1, digit flips; h+4	48/48
DecMerge	q→0 on the 1→0 pair	fuse with next pair: (p+p'+3, q', d'), or into tail	36/36
End	V=0, no tail	all p+1, q−1; digits → 1…10; tail `101`; h+4	36/36
EndLast	as End, q_L=1	last pair → tail (10)^(p+4) 1	36/36
Ov	V=0, tail (10)^t 1	re-pair: (h+5, p1−1, 0), (q_j, p_{j+1}, 1), (q_L, t+1, 1); h=2	36/36
X1	V=0, no tail, last two q=1	Ov-like re-pair, last digit 0, tail (101)^2 (01)^(b+3)	30/30
X2	V=0, tail (101)^2 (01)^k	End-like, plus new pair (3, k, 1); tail ''	30/30

Direct simulation: the abstract map reproduces every canonical transition from step 1,000 to 1e9: 8,374 of 8,374 (Dec 8,328, End 22, Ov 22, X1 1, X2 1).
Abstract run: from the 1e9 state, the accelerated abstract map runs ~2^48 cycles (L up to 45) with no unknown case: 125 Ov, 124 End, 26 merges.
Known bad case: q→0 on a 0→1 digit gives a different, uncharacterized orbit. It failed 6/6 from random configs. Of these cases only the X1 pattern has occurred so far.
Scripts: scripts/ (absm2.py = abstract map, vfinal.py = validators, vf_.json = results, diagram_cycles.py = img/cycles_phase_1e7.png).

Checkpoint A (Dennis)

pending. Questions are in observe.json. The proof would follow TM21's structure plus a 3-state tail automaton; the hard part is the invariant that excludes bad merges.

Informal proof

2026-10-10: proof.md written, STUCK. Rules, initial segment (956 steps) and parity lemmas are done and validated by check_proof.py (405/405 rule instances, 1,534/1,534 transitions from blank to 3e7 steps, abstract run to L=300 inside the domain). Non-halting is reduced to two open lemmas: - O1: an interior q-defect (q+d odd) never runs out before the next overflow; observed minimum margin is 24·2^(L−j). - O2: the far-end eras stay in the tail automaton; the endgame is safe for every residue of the eroding segment.

Merges (DecMerge*, EndLast) are routine here, unlike TM21; a merge of two good segments creates a persistent parity defect. Two of the outside cases halt within 1,700 steps, so O1 is essential. Priority call for Dennis: a research stage on O1, or park.

2026-10-10, revision 2 (after the skeptic review): CHECKPOINT_B. The two open lemmas are replaced by one invariant, INV (proof.md 3.3-3.5): - Each block keeps its role in all E-cycles (the cycles containing End). Eq blocks (q-role in E-cycles) are exactly neutral in scaled terms. All parity defects are Eq blocks, and they never run out. - Ep blocks erode by 3·2^e per cycle pair, but all interior ones are born at the head with good parity. So every merge is legal. - Far end: x = p_L + 2 ≥ 3 always, so the fatal x = 2 case cannot occur, and the endgame is a 4-way case split. - check_proof.py has a new section F (INV checked at every cycle; PASS to L=600). E2 now really checks, and B is labelled informational. The review log is in proof.md §6.

Formalization log

Round 1 (2026-10-10): the kill file 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v compiles (35 s). It proves every §2 macro rule as a Rocq lemma K h P T -->+ K h' P' T', using 14 sweep lemmas, each by plain es. It also proves init : c0 -->* base E-start (78,710 steps, esx). nonhalt is not proved yet, so check_kill FAILs on theorem_text only.
High-level route changed: a per-step invariant J (ghost phase, projected p+Rt / q−Rt) instead of a per-cycle period lemma. J includes INV+(e) in projected form, plus a "no run-out while the last digit is 1" clause. That clause replaces the reviewer's missing touch-count lemma. J was checked in rocq/jcheck.py (base orbit, 26 overflows) and rocq/jrand.py (1,900 random threshold starts): 0 failures. Details: rocq/log.md.

Outcome

Open. Tool issues found: - tools/rulefit.py: the RULEFIT_FAST suite fails 3 Antihydra tests. - On this machine rulefit prints D2(2n+8, b) --> D3(2n+6, 5n+2) [1/1 sims], but the right-hand exponent follows b (checked with b = 2, 3, 9), so a relation was dropped.

Card data pass (2026-10-10)

Figures on the card: Fig 1 = img/cycles_phase_1e7.png, Fig 2 = img/explore_3dec.png, Fig 3 = img/zoom_cycles_annotated.png (added 2026-10-10 for Q1/Q2), Fig 4 = img/blaze_1e8_speed.png, Fig 5 = img/every1e6_1e9.png, Fig 6 = img/default_site.png. Figs 1-3 are the primary figures, shown beside the checkpoint.
The card's mechanism is cut to 3 bullets. The full list before the cut:
Tape: (10)^h, marker 11001, then pairs (10)^p (01)^q, each ending in a digit block 0001 (=1) or 0010 (=0).
Each cycle (3 short bounces + 1 long sweep) subtracts 1 from that binary number; pairs the borrow passes get p+1, q-1.
Counter hits 0: End sweep adds tail 101; next 0: Overflow re-pairs (q_j, p_j+1), adds a pair, h back to 2.
A q that reaches 0 on a 1->0 digit fuses two pairs. About 1 new pair per 2 epochs, so width ~ t^0.5.
Far end: one double-merge detour (X1/X2) at 2.5e8; after it, 2^48 abstract cycles show no new case.
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 aim for a TM21-style invariant proof (tail automaton), not a Sk1like_TC native_compute run?"

Overnight skeptic of the invariant

2026-10-10 FATAL (repairable), see review-invariant.md: INV is not inductive. The §3.3 Theorem is false: K(2;(7,19,0),(2,10,1),(1,6,1);−) satisfies INV, yet one cycle pair later it is at L=0 (o7); other counterexamples hit (o4) or break INV(d). The INV(d) argument and the "k>=3" premise use p_1/p_2 bounds from earlier cycles that INV does not carry. Fix: add (e) p_1>=2^(L+2)-1 and p_2>=2^L. INV+(e) passed 1.03M exhaustive + 70k random cycle pairs, but (e) still needs a lemma that pair 1 gets at least 2^(L*')-2 touches per L-slot. The Rocq period lemma must use INV+(e).

Kill

2026-10-10: KILLED_NONHALT. Kill file 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v (1,301 lines, sha256 91861259c71ce3338425a86a465c4af5b854f63f071737b8cd7feaa36713fcbf) proves top-level Lemma nonhalt : ~ halts tm c0..
tools/check_kill.sh: PASS 3 times on the same sha256, each time with ulimit -s unlimited and -v 8000000, one coqc at a time.
Formalizer, 13:52:55Z: compile 67.4 s (native on), coqchk pass 24.1 s, closed (rocq/kill.out).
Independent audit, --json, 14:04:09Z: 17/17 checks pass, compile 69.4 s, coqchk pass 24.4 s, 0 assumptions. The audit also confirmed the string is line 53 of data/holdouts/2026-10-07_778.txt (holdouts.py contains, plus a byte comparison). It read the file end to end and found nothing suspicious. Harmless oddities it noted: local notations -->*/-->+, Notation tri, Import Coq.Init.Datatypes. (undoes String's shadowing of length), Local Open Scope nat_scope, an unused lemma pc_len. None touches tm, c0, halts, TM_from_str or the theorem name.
Fresh human-readable run for the submission, 14:06:34Z: compile 69.3 s (native on), 0 assumptions (closed), coqchk pass 24.3 s (submission/check_kill.txt).
The proof:
14 sweep lemmas (es) and list sweeps PassesR/PassesL/OvPasses give the 9 macro rules (Dec, DecMerge, DecMergeTail, DecMergeEmpty, EndR, EndLast, X2, Ov, X1), each K h P T -->+ K h' P' T';
init : c0 -->* K 2 base TN (78,710 steps, one esx, about 30 s);
per-step invariant J on (h, P, T, phase, c4), with per-pair clauses PN/PI on the projected values p + Rt and q - Rt; per-rule obligations ob_* and list lemmas inv_*;
Jstep, J_base, and nonhalt = multistep_nonhalt + progress_nonhalt_cond with P := J. It imports only Individual62 from busycoq. Details: rocq/log.md (rounds 1-2), atlas/rocq-notes.md.
Relation to proof.md: the .v proves J, not proof.md's per-cycle period lemma. J contains INV+(e) in projected form at E-starts, and it replaces L6 and L5' with a projected-h clause, the L1 first-half clause and p + Rt >= c*2^f bounds. So the kill does not depend on the prose of proof.md §3.3-3.8. Formalization found no flaw in that prose; the second skeptic review (review-invariant-2.md) had found no fatal or major gap.
Submission package: submission/.
The .v, unchanged (same sha256).
proof.md: a copy with the title and status lines updated to "fully formalized", an AI line, §3.7's init paragraph matched to the .v, and a new §4 subsection mapping sections to lemma names and listing where the .v departs from the plan. The working proof.md is untouched.
check_kill.txt (the 14:06:34Z run), README.md.
discord.md: a draft of 1,752 characters plus <LINK>. Not posted.
Before posting:
reports/discord-drafts.md Message 2 (duplicate-work question) lists this machine in group 1. If it is still unsent, cut group 1 down to the two look-alikes, or drop it.
targeting.md §5 Q3 (does the list behind Sk1Machines.v also cover Class 2?) is still open.
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.
Look-alikes not killed: 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC--- (#24) and 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD--- (#25). At 1e9 their tapes are within 4 cells of ours (targeting.md), so the same argument likely applies, but each needs its own .v.

Card questions (Dennis, 2026-10-10)

Q3 (Fig 2, sweep depth = borrow chain of a binary down-counter): yes. Q1 and Q2: unclear as worded, and Fig 1 lacks the detail to answer them; to be rewritten in plain language with a zoomed, annotated figure. - 2026-10-10, Q1/Q2 rewritten (same claims, now answerable at cell level). New primary Fig 3 = img/zoom_cycles_annotated.png (+ img/zoom_cycles_annotated.html, vector, with a tints on/off switch; raw render img/zoom_cycles_raw.png), made by scripts/diagram_zoom.py: every cell (3 px) of the 22 canonical rows at steps 4,610..24,668 (rows 11-32 of Fig 1), cells -152..47, from a blank start. Cells come from tools/diagram.py render_rows (bbchallenge-default colours); translucent tints come from parsing each row ((10)^h, 11001, pairs (10)^p (01)^q 0001|0010, tail), and every row parses. Margins give the step, the counter value (0 highlighted) and the macro step (Dec/End/EndLast/re-pair); yellow bands mark the two re-pairs (Ov at 8,319 and 19,436); dashed/dotted guides carry the old borders / digit blocks through each re-pair; an inset magnifies cells -23..6 of rows 9,515 and 10,419 (one Dec touching pair 2). What it shows (and Q1/Q2 ask): digit blocks keep their columns between re-pairs while pair j's border moves 2 cells every 2^(j-1) rows; at a re-pair each new digit block sits on an old border (within 1-2 cells) and each new border at an old digit block (pair 1's next to the old 11001 marker). The old Q1/Q2 texts asked the same about Fig 1's edges and kinks.

Checkpoint B (Dennis, 2026-10-10)

Dennis read through proof.md: "too complex for me but it looks fine I guess - I trust you." (Read-through, not a line-by-line check; the kill rests on the Rocq proof.) Card Q1 and Q2: both yes; Q1's wording 'each purple block keeps its columns' is not literally true (internal light/dark shift, a one-cell translation partway down) -> reword.