1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): Skelet 1-like Class 2. It is kill #3's table under the state renaming ρ = DABCEF (A↦D, B↦A, C↦B, D↦C), with no mirror, started in #3's state B. / pending Spreadsheet notes / Discord thread: - Sheet: Results CSV line 1288 and the Classifications tab, "Skelet 1-like Class 2", class only (no status, notes, sources or done-by). Not in data/discord/*. - Holdout list: line 604 of data/holdouts/2026-10-07_778.txt, byte-exact. Not in solved_index.tsv; a singleton equivalence group. Found by reports/family-sweep.md (candidate 2). - Parent: machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (#3, KILLED_NONHALT). Siblings with the same table: #25 (started in #3's C) and #24 (mirrored, started in #3's D), both killed.

Viewer: https://bbchallenge.org/1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---

Observation

• Relation to #3. ρ is the only one of the 720 renamings (each with or without a mirror) that maps #3's table to this one. ρ is the 4-cycle (A D C B). The machine starts in A = ρ(B), so its run is #3's machine run from 0^inf B> 0^inf. That is #3's own run without the 1 written in #3's first step.
• Lockstep: the twin from blank equals #3 started from 0^inf B> 0^inf, relabelled by ρ, at every step for 2·10⁶ steps.
• Sibling maps (informational): BCDAEF from #25's D, and the mirror of CDABEF from #24's C.
• Same macro rules, different orbit. The canonical configs (state D on a new left edge) follow #3's abstract map from step 402 on: 5,323 of 5,323 transitions to 3·10⁸ steps. Unlike #25 and #24, this orbit is not coupled to #3's.
• The first 120 E-starts of the two orbits have none in common.
• The base has 3 pairs, where #3's has 4.
• At 10⁹ steps the tape spans 79,454 cells (−79,241..212) with 39,718 nonzeros. #3 has 67,343 cells and 33,665 nonzeros, so this tape is 18% wider.
• Diagrams in img/ (labels in observe.json):
• every1e6_1e9.png and parent3_every1e6_1e9.png: this machine and #3, drawn identically (every 10⁶ steps, every 32nd cell, same window);
• init_recL_4e4.png: left records up to the base;
• zoom_cycles_annotated.png (+ .html, zoom_cycles_raw.png; scripts/diagram_zoom.py, adapted from #3's): every cell, one row per decrement, steps 3,520..21,790, around re-pairings 3 and 4, tinted by role like #3's card Fig 3; the script checks the card's Q2 claims;
• default_site.png, viewer.html.

Candidate rules

3's 9 rules, verbatim, with head state D instead of A. Checks:

• 405/405 random instances on this machine's own table;
• blank tape → K0′ = K(2; (7,4,0); −) at step 402 (step 121 has L = 0, outside D);
• re-pairings at 1,083, 3,520, 6,965, 17,738, 23,871 and 38,732, then every transition rule-predicted.

Checkpoint A (Dennis)

Card: card.html. Not blocking. The mechanism is #3's, which passed Checkpoint A there.

Informal proof

proof.md, a delta proof. - Unchanged: the rules, the outside cases, INV+(e), the period theorem, and the Rocq Jstep. There is no adjusted invariant. - Changed: only the initial segment and the base, B′ = K(2; (47,32,0),(40,33,1),(13,34,1); −), at step 38,732 after re-pairing 6. - B′ meets INV+(e) with L* = 3, the lower edge of clause (d). - It also meets the Rocq J clauses. Their one tight clause, 48 ≥ 48, is tight at every regular start. - The E-starts after re-pairings 2 and 4 have L* = 2, so B′ is the first possible base. - The period theorem covers L* = 3: its proof needs only M = L* + 1 ≥ 4 and L* ≥ 2 (proof.md §3). - Checks. check_proof.py, which imports #3's checks read-only, gives SUMMARY PASS on S, A, C, D, B, G and N. Outputs: - check_proof.out: defaults, L* ≤ 300, 34 s; - check_proof_l600.out: G and N to L* ≤ 600; - check_proof_3e8.out: D to 3·10⁸ steps. - Section N runs 5,000 random L* = 3 starts around B′, one cycle pair each.

Formalization log

Not started. The .v delta is in proof.md §5. It is #25's recipe: - take #3's current .v (sha256 cfa603a3…, check_kill PASS in its submission/check_kill.txt); - simultaneous rename {{A}}→{{D}}, {{B}}→{{A}}, {{D}}→{{C}}; - the TM string; - init0 (7,4) at 402 steps; - the 3-pair base with an esx of 38,732 steps; - J_base with the same script.

Outcome

Open (CHECKPOINT_B). Next: formalize, then check_kill. - #3's notes.md quotes its .v as sha256 91861259…, 1,301 lines. The file on disk is now cfa603a3…, 1,303 lines, and a newer check_kill PASS covers it. Use the file on disk.

Kill

• 2026-10-10: KILLED_NONHALT. Kill file 1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---.v (1,309 lines, 1,484 sentences, sha256 a12c060311a6a0b94054174d5882ac2316ec37e22b464ee475b6d30bf877128e) proves top-level Lemma nonhalt : ~ halts tm c0..
• tools/check_kill.sh: PASS 3 times on the same sha256, each with ulimit -s unlimited and ulimit -v 8000000, one coqc/check_kill at a time. The watchdog showed about 20 GB available, and nothing was killed.
• Formalizer: compile 54.4 s (native on), coqchk -norec pass 17.4 s, closed (rocq/check_kill.out).
• Independent audit, --json: 17/17 checks pass, compile 53.3 s, coqchk pass 17.6 s, 0 assumptions. The audit also confirmed the string is line 604 of data/holdouts/2026-10-07_778.txt (holdouts.py contains, grep -x count 1). It read all 1,309 lines and found nothing suspicious: only Individual62 and the stdlib (Arith, Lia, List, String, ZifyNat) are required; local notations only; no Section/Variable/Context/Module/Set/Unset/Arguments/Opaque/Hint/Instance/Fail/Succeed; no framework name redefined; ASCII only. It re-derived the rename by hand (ρ applied to #3's string gives this string). Harmless leftovers inherited from #3: Import Coq.Init.Datatypes., Local Open Scope nat_scope, and the unused lemmas init0 and pc_len.
• Fresh human-readable run for the submission, 2026-10-10T19:26:21Z: 17/17 checks PASS, compile 52.4 s (native on), 0 assumptions (closed), coqchk pass 17.5 s, 73 s wall (submission/check_kill.txt; raw copy rocq/check_kill_submission.out, exit in rocq/check_kill_submission.exit).
• The proof is the proof.md §5 delta applied by a script to #3's passing .v (sha256 cfa603a3…3031, 1,303 lines). It compiled on the first attempt, and the first check_kill passed (rocq/log.md):
• the TM string;
• a simultaneous ρ rename of {{X}} in the 14 sweep lemmas and K ({{A}}→{{D}}, {{B}}→{{A}}, {{D}}→{{C}}; counts D 4, A 12, C 19, as predicted);
• init0 : c0 -->* K 2 [(7,4,false)] TN (402 steps, unused);
• base := [(47,32,false); (40,33,true); (13,34,true)] (L* = 3), and init by one esx over 38,732 steps;
• header and rule-table comments. Every es proof, the 9 macro rules, J/PN/PI/TC, every ob_*/inv_* lemma, Jstep, the J_base script and nonhalt are #3's text: Require Import ZifyNat .. Lemma nonhalt is byte-identical to #3's. After ρ is applied to #3's state names, 16 of #3's lines differ (TM string, init0, base, comments). J_base closes the tight clause h + 4(tv+w) + 6 = 48 >= 12w = 48 with the same lia. Direct proof on the holdout string; no relabelling or equivalence lemma.
• Submission package: submission/.
• The .v, unchanged (same sha256).
• proof.md, a copy built by rocq/make_submission_proof.py (each edit asserts exactly one match; the working proof.md is untouched). Updated: title, header (holdout lists, sheet, parent pointer, status, AI line), §5 heading and a "Done as planned" paragraph with a delta-to-lemma map, a §7 note that no Checkpoint B notes were on file, and every repo-local path replaced by a plain description (the script refuses to write if one is left).
• parent-proof.md, a verbatim copy of #3's submission proof.md, because this proof cites it as P§n.
• check_kill.txt (the 19:26:21Z run), README.md.
• discord.md, a draft of 1,529 characters plus <LINK>. Not posted.
• Before posting:
• Post #3's message first, then the twins, or all four (rows 1278, 1280, 1288, 1289) as one group. #3's look-alikes paragraph and #25's "#24 not formalized" note are stale, and neither names this machine.
• reports/discord-drafts.md Message 2 (not posted): group 1 is now all killed. Drop it if unsent.
• targeting.md §5 Q3 (does the list behind Sk1Machines.v also cover Class 2?) is still open, and Discord #bb6 was never searched for this string. Search before posting.
• proof.md §7 has two open reviewer questions for Checkpoint B (delta form; 3-pair base at L* = 3 versus the 4-pair E-start at step 104,510). No notes from Dennis were on file when this was packaged. If he adds any, fold them into proof.md and the submission copy first.
• Disclosure wording differs across drafts: this package uses "with the help of Claude (Anthropic)"; the older unposted drafts say "with Claude Code (AI-assisted) under my direction". The .v keeps the house-style line "Formalized with Claude Code (AI-assisted)."
• With this kill, all four holdouts with #3's table (the A, B, C and D starts) are killed: #3, this machine, #25, #24.

Card questions (Dennis, 2026-10-10)

Q1 (Fig 1/2: same bands as #3, left edge farther out): yes. Q2: confusing as worded; to be rewritten in plain language (same terms as #3's rewritten Q1/Q2). The card showed "#F2" (a family-sweep working id) instead of #3b; fixed. - 2026-10-10: Q2 rewritten in #3's plain terms (pair / digit block / re-pairing defined; what to look at, what to expect, yes/no) around a new zoomed, annotated Fig 4 (zoom_cycles_annotated.png, primary; Fig 1-3 unchanged, the default view moved to Fig 5). Q3 (3-pair base vs the 4-pair E-start) recorded as settled: the Rocq proof uses the 3-pair base and passed check_kill.