1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): Skelet 1-like Class 2. It is kill #3 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- mirrored, renamed and started in the parent's state D. / pending Spreadsheet notes / Discord thread: Results CSV line 1289 gives the class only (status, notes, sources and done-by are empty). The Classifications tab lists it under Skelet 1-like Class 2 with no note. It is not in data/discord/*.txt, not in busycoq at the pin and not in solved_index.tsv. On the 778 list: line 622, byte for byte. Unclaimed. Viewer: https://bbchallenge.org/1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---

Observation

• At 1e9 steps there is no halt; the tape has 33,665 nonzeros and spans 67,345 cells (−182..67,162). The parent has 33,665 nonzeros on 67,343 cells (−67,161..181). The twin grows to the right.
• The tables are equal up to mirror + renaming φ: A↦D, B↦A, C↦B, D↦C, E↦E, F↦F (12/12 entries). This is the only map among 2 × 720 candidates. The start state goes to D, so the twin is the parent run from (D, tape0), not a copy of the parent's run.

Candidate rules

• The parent's 9 macro rules, transported to K′ := the mirror of K (state B on the blank cell right of the reversed word).
• check_proof.py §A ran 405/405 random instances on the twin's own table. 1,534/1,534 canonical transitions to 3e7 steps are predicted by the abstract map, with the same rule counts as the parent.
• Informational lockstep: same rule at every macro step to L = 120. The states differ only by +1 on one far/tail block.

Checkpoint A (Dennis)

Not separately needed: same mechanism as #3 (Checkpoint A passed there). Not blocking.

Informal proof

See proof.md, a delta proof. Rules, outside cases, INV+(e), the Theorem (period) and the Rocq Jstep are unchanged. What changes: - K0′ = K′(2;(11,12,0);−) at step 1021; - the base E-start after overflow 6 is K′(2;(95,68,0),(34,33,1),(10,15,1),(1,25,1);−) at step 78,911.

The base differs from the parent's only in the far q (25 vs 24). It satisfies INV+(e) and J.

check_proof.py gives SUMMARY PASS (M, S, A, C+D, B, G, J; --selftest adds 7 negative controls, all FAIL as they should; about 21 s). Log: logs/check_proof_full.log.

Formalization log

• Not started in machines/. The route is in proof.md §4: the parent's file plus a mirror conjugacy lemma mu, init' from (D, tape0), and J_base'.
• Rocq sanity check, rocq/parent_from_D.v (the parent's .v plus 4 small edits, rocq/parent_from_D.diff): it proves nonhalt_D : ~ halts tm (D, tape0) for the PARENT's tm. Result: rc=0, 39.7 s, closed under the global context (rocq/parent_from_D.out). It is not a kill file.
• Tactic note: esx from (D, tape0) falls back to symbolic es; it did not finish in 14 minutes and reached 2.5 GB before it was killed. Its fast path solve_init only matches goals that start at c0. Fix: solve_initD, which is change (D, tape0) with (cconfig_to_config (nil,nil,0,D)) followed by the rest of solve_init. It works in seconds.
• Left for the kill: Lemma C (mirror conjugacy mu, about 40-60 lines), tm3 naming, and nonhalt for the twin string.

Outcome

Open (CHECKPOINT_B). Next: formalize per proof.md §4. Look-alike #25 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD--- is a plain renaming of the parent (no mirror), started in the parent's state C. Another agent has already killed it (σ-renamed .v by script). A mirror cannot be done by text substitution, so #24 uses the conjugacy route of proof.md §4.

Kill

• 2026-10-10: KILLED_NONHALT. Kill file 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---.v (1,361 lines, 1,500 sentences, sha256 5dadb08f7130e5942620c4e2cbf9f455e40633327c3432e872fc163b0d297240) 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.
• Formalizer: compile 38.5 s (native on), coqchk pass 11.6 s, closed (rocq/kill.out, 17:17:36Z).
• Independent audit, --json: all checks pass, compile 38.3 s, coqchk pass 11.5 s, 0 assumptions, 52 s wall. The audit also confirmed the string is line 622 of data/holdouts/2026-10-07_778.txt (holdouts.py contains; grep -x one match; cat -A: no stray characters). It read the whole file and found nothing suspicious: allowed Requires only (Individual62, Arith, Lia, List, String, ZifyNat), no Set/Unset, Axiom/Parameter/Admitted, Variable/Context/Section/Module, Opaque/Strategy/Extract/Register, *_no_check, Hint/Instance/Coercion or Fail/Succeed, and nothing redefines tm, c0, halts, TM_from_str, flip, Perm or the state names. It hand-checked the conjugacy (12/12 entries under φ, start A ↦ D). The only warning is the expected second TM_from_str literal (line 34, the parent's table as tm3).
• Fresh human-readable run for the submission, 17:21:14Z: 17/17 checks PASS, compile 38.2 s (native on), 0 assumptions (closed), coqchk pass 11.5 s, 52 s wall (submission/check_kill.txt; raw copy rocq/check_kill_submission.out). The watchdog showed about 21 GB available, and nothing was killed.
• The proof is proof.md §4's route, generated by rocq/assemble.py from #3's passing .v (sha256 91861259…) with no hand edits afterwards (rocq/log.md):
• tm is the twin; #3's table is tm3, and the local -->*/-->+ notations are bound to it;
• the start: solve_initD, init0 : D;; tape0 -->* K 2 [(11,12,false)] TN (1,021 steps), base with far pair (1,25,true), init (78,911 steps);

• 3's nonhalt becomes nonhalt_D : ~ halts tm3 (D;; tape0);

• the conjugacy (Lemma C) is phi, perm_twin : Perm (flip tm) tm3 phi (12 cases) and busycoq's Flip.flip_halts + Permute.perm_halts. This takes about 15 lines instead of the planned 40–60-line mu induction. Every sweep, macro rule, J, Jstep and J_base is #3's text. Compared with #3's .v, 22 lines were replaced and 82 added. It imports only Individual62 from busycoq. Direct proof on the holdout string.
• Submission package: submission/.
• The .v, unchanged (same sha256).
• proof.md, a copy with updated title, header (holdout lists, parent pointer, status), a pointer after Lemma C, the §4 heading, a §4 "Done" paragraph with a delta-to-lemma map, §6 open items and the AI line. The working proof.md is untouched. Built by rocq/make_submission_proof.py, which checks the working copy's sha256.
• parent-proof.md, a verbatim copy of #3's submission proof.md, because this proof cites the parent's sections.
• check_kill.txt (the 17:21:14Z run), README.md.
• discord.md, a draft of 1,641 characters plus <LINK>. Not posted.
• Before posting:
• Post #3's message first, or post #3, #25 and this one together. #3's look-alikes paragraph says #24 and #25 are not covered, and #25's draft notes say #24 is not formalized. Both are now out of date.
• reports/discord-drafts.md Message 2 (not posted): its group 1 (#3, #24, #25) is now all killed. If it is still unsent, drop group 1.
• 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.