1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): Skelet 1-like Class 2. It is kill #33's table 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA--- renamed by σ = (A,B,C,D,E,F) ↦ (B,C,D,A,E,F), no mirror, started in #33's state D. Equivalently kill #11's table mirrored, started in #11's C. / pending Spreadsheet notes / Discord thread: - Sheet: Results row 1282 and the Classifications tab, "Skelet 1-like Class 2", class only (no status, notes, sources or done-by). - Line 388 of data/holdouts/2026-10-07_778.txt, byte for byte; on all 26 snapshots. - eqv_1590 group {this, 1RB1RF_1RC0RA_1LD0RA_1LE0LE_1RB0LD_1RB---, 1RB---_1RC0RF_1LD0RF_1LE0LE_1RB0LD_1RB1RA}: #33's table started in E and in F (busycoq Eqv_v2.v TM688/TM2137, tm' mentions only, nothing proved for this string). - Not in data/discord/*. Named only in the unposted reports/discord-drafts.md (Message 2, group 2). Unclaimed, so not SKIPPED. Discord #bb6 itself was not searched. Viewer: https://bbchallenge.org/1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---

Observation

• Relation (by simulation and table matching, check_proof.py §S, §R). σ is the only one of 720 × 2 relabelings taking #33's table to this string (12/12 cells); this machine's A is #33's D. The run from blank equals σ(#33 run from 0^inf D> 0^inf) at every step (lockstep to 2·10⁷ steps). From #11: CDABEF + mirror, start C (unique).
• Changed low-level rules: none. #33's 20 window lemmas S1–S6, T1–T14 hold on this table with states renamed by σ (same windows, same step counts, transitions = σ of #33's; §L). F is entered only by E1 and reads 0 every time.
• Macro rules: the same. M and O with #33's formulas, head state <D instead of <C (§A random instances, §H every link of #33's chains on this table).
• Invariant: unchanged. INV is stated on triples; the base is in class A.
• Init (new). K-configurations from blank: 101 K((1,1,1);2,1), 234 K((0,0,1),(1,1,2);4,1), 326 K((2,0,1);5,3), 426 K(;9,5) (none in INV), then 687 K((1,1,9);8,1), class A (S = 6, T = 0). #33 has 82 and 215.
• 1e9 steps from blank: no halt; span −77,517..173 (77,691 cells), 38,839 nonzeros (scripts/sim_1e9_end.jsonl). Trajectory twin of #11 (77,685 / 38,836): from macro step 54 on, the macro state is #11's with one top-digit exponent +3, same rule every step (§X, 3·10⁵ macro steps; explanation only).
• Images: img/default_site.png (site view), img/records_L_3e5.png (left records), img/parent33_records_L_3e5.png (#33, same view), img/viewer.html. #33 started in D renders to the same site PNG byte for byte (scripts/parent33_fromD_site.png).

Candidate rules

33's rules, verbatim, with K head state D (proof.md §1). Tested on this table: M 700/700, O 350/350, random INV states 2,836/2,836 one macro step (§A); 37,220 M chains and 9,996 O chains link by link (§H). Real run from blank = rules at every macro boundary from step 687: 3,384/3,384 to 3·10⁷ (default) and to 10⁹ in check_proof_long.out (§D).

Checkpoint A (Dennis)

Not blocking (confidence high, same mechanism as #33/#11, whose checkpoints passed). Card: card.html, 2 questions (one figure check, one decision on the delta-proof format).

Informal proof

proof.md, a delta proof from #33's proof.md: Lemma R (renaming), what carries over (rules, INV, closure, progress), what changes (init and base, §2), the complete argument (§3), the coupling with #11 (§4, explanation), the .v delta (§5). - check_proof.py (imports #33's check_proof.py read-only): SUMMARY PASS, sections S, R, L, A, H, C, D, B, G, X, V. Default about 20 s (check_proof.out); long run --seed 2026 --tm-steps 1e9 --orbit 1.2e6 --induct 6e5 --lockstep 2e7 (check_proof_long.out).

Formalization log

• 2026-10-10, scratch check only (stage informal_proof). rocq/make_delta.py applies proof.md §5 to #33's passing .v (sha256 37cb1802…2053): the TM string, σ on every {{X}} (A 5 → B, C 22 → D, D 18 → A), init : c0 -->* K [d1 1 9] 8 1 (687 steps, same solve_init), the base in nonhalt, comments. Result rocq/delta_check.v (670 lines). rocq/compile.sh: Coq 8.20.1, 8.8 s, exit 0, Print Assumptions nonhalt: Closed under the global context (rocq/delta_check.out). Compiled on the first try; no tactic changes.
• Not done: copy to machines/<tm>/<tm>.v and run tools/check_kill.sh (the kill stage). Done later the same day: see ## Kill.

Outcome

KILLED_NONHALT (2026-10-10, ## Kill below). Before the kill it read: Open (CHECKPOINT_B). Next: kill stage, i.e. copy rocq/delta_check.v to the kill path, run tools/check_kill.sh, independent audit, submission package. Post together with #11 and #33 (their twins paragraphs list this machine as not formalized).

Kill

• 2026-10-10: KILLED_NONHALT. Kill file 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---.v (673 lines, sha256 6238e25c639d96b40bb55542a76c3d11972053ef3280d039b629a8bf9d7151bd) proves top-level Lemma nonhalt: ~halts tm c0..
• tools/check_kill.sh: PASS 3 times on the same sha256, 17/17 checks each time, 0 assumptions (closed), coqchk -norec pass (no timeout).
• Formalizer: compile 9.2 s (native on), coqchk 1.8 s (rocq/check_kill.out, rocq/log.md).
• Independent audit, --json, 19:21:01Z: compile 9.07 s, coqchk 1.86 s. The audit also:
  • confirmed the string is line 388 of data/holdouts/2026-10-07_778.txt (holdouts.py contains, grep -x -F, od -c on both the list and the literal; the .v is all ASCII);
  • read the file end to end: Individual62 plus ZifyNat/Lia/String/List/Arith, no Set/Unset/Opaque/Section/Variable/Context/Module/Axiom/Admitted/Hint/Instance, only the three local --> notations, no rebinding of halts/c0, two proof-only Ltacs (fin, pw);
  • compiled its own copy with extra checks: tm = TM_from_str "<string>" by eq_refl, nonhalt against the fully qualified halts/TM_from_str/c0, Print Assumptions nonhalt closed;
  • delta audit: σ applied to #33's .v (sha256 37cb1802…2053) and diffed against the kill file. Only the header, the TM string, init's target, the base in nonhalt and comments differ; every proof script is identical.
• Fresh human-readable run for the submission, 19:23:38Z: compile 9.1 s (native on), coqchk pass 1.8 s, 0 assumptions (submission/check_kill.txt, copy in rocq/check_kill_fresh.out).
• The proof is proof.md §5's delta of kill #33's .v, applied by script (rocq/make_delta.py → rocq/delta_check.v); the kill file is that output with only the header comment rewritten to house style (code byte-identical, checked by diff). σ counts {{B}} 5, {{D}} 22, {{A}} 18, {{E}} 18; new init : c0 -->* K [d1 1 9] 8 1 (687 steps, solve_init) and base. Compiled on the first try; no tactic changes, so nothing new for atlas/rocq-notes.md.
• Submission package: submission/.
• The .v, unchanged (same sha256).
• proof.md, a copy built by asserted single-match edits from the working copy (source sha256 3485c697…74d6): title, a submission note, header (holdout-list wording, parent pointer, evidence, status, AI line), §5 heading and closing paragraph (how the delta was carried out, plus a table of where each item lives in the .v), two §6 table cells (repo paths removed) and §7. The working proof.md is untouched.
• parent-proof.md: #33's submission proof.md, verbatim (sha256 17b5fff9…6d15), cited as P§n. Its "D-start row not formalized" remark predates this kill.
• check_kill.txt (the 19:23:38Z run), README.md.
• discord.md, a draft of 1,596 characters plus <LINK>. Not posted.
• Before posting:
• Post #11's message, then #33's, then this one (or all three together). Fix their twins paragraphs, which list this machine as not formalized (#11's also misses #33).
• Discord #bb6 was never searched for this string; search first. If reports/discord-drafts.md Message 2 is still unsent, its group 2 is now down to hipparcos's machine.
• No Checkpoint A or 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.
• Table status: of the four holdouts with this table, #11, #33 and this machine are killed. hipparcos's 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- (Level 1 tab, init 732 steps to K((1,1,10); 8, 1) in simulation) is the last one; the same delta (σ + new init) should apply, but it needs its own .v.