1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---

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 σ = (A C)(B D), with no mirror, started in #3's state C / pending Spreadsheet notes / Discord thread: Results row 1280 and the Classifications tab ("Skelet 1-like Class 2"), class only, with no status, notes, sources or done-by. Nothing in data/discord/*. Holdout list: line 293 of data/holdouts/2026-10-07_778.txt, byte-exact. Parent: machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (#3, KILLED_NONHALT). Viewer: https://bbchallenge.org/1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---

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, and σ is an involution. The twin starts in A = σ(C). So its run is #3's machine run from 0^inf C> 0^inf, which is #3's own run without the 11 written in its first two steps.
• Lockstep. The twin from blank equals #3 started from 0^inf C> 0^inf, relabelled by σ, at every step for 2·10⁶ steps.
• Same macro rules, different orbit. At every macro step, the twin's K is #3's K with exactly one exponent larger by +2: the far block (q_L, then the last pair's p, then the tail t or T2's k), with the same rule applied. Checked at every macro step to L = 16 and at every re-pairing to L = 600.
• Not identical trajectories. The twin lags #3 by 132 steps at K0 and by 404 at the base. At 1e9 steps it has 67,347 cells (−67,163..183) and 33,668 nonzeros; #3 has 67,343 and 33,665.

Candidate rules

3's 9 rules, verbatim, with head state C instead of A: 405/405 random instances on the twin's own table. Twin from blank, every canonical transition rule-predicted to 3·10⁷ steps (1,534/1,534).

Checkpoint A (Dennis)

No card. The delta was settled by simulation (§S and §X of check_proof.py).

Informal proof

proof.md, a delta proof. - Unchanged: the rules, the outside cases, INV+(e) and the period theorem; no adjusted invariant. - Changed: only the initial segment and the base. - The twin reaches K0′ = K(2; (11,13,0); −) at step 1,088 (#3: (11,11,0) at step 956). - Its base E-start is B′ = K(2; (95,68,0),(34,33,1),(10,15,1),(1,26,1); −) at step 79,114. It is #3's base with q_4 = 26 in place of 24, and INV+(e) holds there. - Checks. check_proof.py (it imports the parent's checks read-only) gives SUMMARY PASS on S, A, C, D, B, G, X. Output is in check_proof.out (defaults, L ≤ 300) and check_proof_l600.out (G/F/X to L ≤ 600).

Formalization log

Not started. The .v delta is in proof.md §5: - the TM string; - a simultaneous σ-swap of the state names in the sweep lemmas and K: {{A}}→{{C}}, {{B}}↔{{D}}; - init0 with (11,13); - base with (1,26) and an esx of 79,114 steps; - J_base with the same script.

Everything else stays verbatim.

Outcome

Open. Next: formalize, then check_kill.

Kill

• 2026-10-10: KILLED_NONHALT. Kill file 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---.v (1,305 lines, 1,484 sentences, sha256 766d227080425b8550e793e3f13cacf99bae3d7626a6b17b490cce51d7f979fc) 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 check_kill of ours at a time. During the second and third runs another agent's unrelated coqc (M3D.v) was also running; the watchdog showed about 21 GB available, and nothing was killed.
• Formalizer, 16:57:17Z: compile 69.3 s (native on), coqchk pass 24.6 s, closed (rocq/kill.out).
• Independent audit, --json, 17:00:00Z: all checks pass, compile 69.0 s, coqchk pass 24.8 s, 0 assumptions. The audit also confirmed the string is line 293 of data/holdouts/2026-10-07_778.txt (holdouts.py contains; grep -nxF with cat -A: no trailing whitespace or CR). It read all 1,305 lines and found nothing suspicious: no Section/Variable/Context/Module/Include, no ML loading, no kernel flags, no Fail/Succeed; halts, c0 and TM_from_str are never redefined; local notations only. Harmless leftovers it noted, inherited from #3: Import Coq.Init.Datatypes. and the unused lemmas init0 and pc_len. Its diff against #3's .v showed only the changes in rocq/log.md.
• Fresh human-readable run for the submission, 17:02:48Z: 17/17 checks PASS, compile 68.6 s (native on), 0 assumptions (closed), coqchk pass 24.6 s, 97 s wall (submission/check_kill.txt; raw copy rocq/check_kill_submission.out).
• The proof is the proof.md §5 delta applied by a script to #3's passing .v (sha256 91861259…fcbf), and it compiled on the first attempt (rocq/log.md):
• the TM string;
• a simultaneous σ = (A C)(B D) swap of {{X}} in the 14 sweep lemmas and K (counts C 4, D 12, B 19, as predicted);
• init0 : c0 -->* K 2 [(11,13,false)] TN (1,088 steps);
• base with last pair (1,26,true), and init by one esx over 79,114 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, unchanged. Apart from state names, 36 lines differ from #3's .v. It imports only Individual62 from busycoq. Direct proof on the holdout string; no relabelling or equivalence lemma.
• Submission package: submission/.
• The .v, unchanged (same sha256).
• proof.md, a copy with updated title, header (status, AI line, parent pointer), §5 heading and a "Done as planned" paragraph with a delta-to-lemma map, plus a §7 note that no Checkpoint B notes were on file. The working proof.md is untouched. Built by rocq/make_submission_proof.py.
• parent-proof.md, a verbatim copy of #3's submission proof.md, because this proof cites it as P§n (same section numbers).
• check_kill.txt (the 17:02:48Z run), README.md.
• discord.md, a draft of 1,553 characters plus <LINK>. Not posted.
• Before posting:
• Post #3's message first (or as a pair). Its look-alikes paragraph says this machine is not covered; point it at this message instead. #24 is still not formalized.
• reports/discord-drafts.md Message 2 (not posted) lists this machine and #3 in group 1. If it is still unsent, cut group 1 to #24 only, or drop it.
• 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.
• 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.