1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): Counter Class 4, trajectory twin of kill #12 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF (one transition changed, different start state) / (pending) Spreadsheet notes / Discord thread: - Holdout list data/holdouts/2026-10-07_778.txt line 676, byte-exact. - Sheet: Results row 833, status blank, class Counter Class 4, no notes, no links. Level 0 note "-". Direct Simulation lists it only as not simulated to 1e14/1e15. No claim anywhere. - Not in either local Discord file (data/discord/*.txt). - busycoq: only tm' of Eqv.v TM113 (eqv: halts tm c0 <-> halts tm' c0). Not a proof; data/solved_index.tsv has no proof. Viewer: https://bbchallenge.org/1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB

Observation

• It is not #12 up to renaming or mirroring. I searched all 720 relabelings × {as is, mirrored}: none matches. The unique closest is σ (twin A..F = parent B,C,D,E,F,A), which differs in 1 transition (twin F0 = 1RF; the parent's A0 = 1RB renames to 1RA). σ(parent) is exactly Eqv.v TM113.tm. Relabelings that keep the start state differ in at least 6 transitions.
• In the parent's names, the twin is the parent with A0 := 1RA, started in state B.
• Its trajectory is the TM113 trajectory with 4 extra steps at each R3. The twin and TM113 pass through the same left-edge configurations conf([],[2,2]+O_n([])), the twin 4(n+1) steps later. The parent passes through conf([],[3,2]+O_n([])).
• At 10^9 steps: twin 133 cells (87 nonzeros), parent 134 (89), TM113 133 (87). This is the observer's 134/133.

Candidate rules

• R1, R2, R2e, HALT, CW, DW, FW are the parent's exactly: same transitions under σ, same step counts.
• R3' = the parent's R3 with A0 B0 replaced by the detour A0 A0 A1 C1 B1 B0 [twin F0 F0 F1 B1 A1 A0]. The tape effect is the same, and it takes 3k+2m+15 steps instead of 3k+2m+11.
• Init: 48 steps to conf([],[2,2,1]) (the edge frame has a budget of 2).
• All of these are tested in check_proof.py (sections R, A, C, B, T, H, F, G). The full run passes in 52 s (scripts/check_proof_out.txt).

Checkpoint A (Dennis)

No card. This is a delta to an already killed machine, so it went straight to proof.md.

Informal proof

proof.md is a delta proof. It gives the explicit map σ, the one changed rule (R3 to R3', with its 6-step detour trace), the changed init, and the adjusted top-level invariant conf([],[2,2]+O_n([])). The budget-2 edge lemma has zero slack, and the parent's exact costs at M = [] close it. RM, the epoch rules and the Theorem are inherited from P.v, which machine-checks them. §8 is the formal delta plan: about 6 local edits to P.v. It does not depend on Eqv.v.

Formalization log

Not started (next stage). Expected edits: - the TM string; - head state <{{F}} in tR1/tR2/tR3/tR3c/conf; - a new Ep_tm2 from Life_shape (z=3) + push0_ok (h=2) + Life_tm; - init to conf [] [2;2;1]; - nonhalt with C i := conf [] (2::2::snd i).

Outcome

CHECKPOINT_B. The delta argument is complete and validated by simulation. It is not a kill until check_kill passes on its own .v.

Kill

• 2026-10-10: KILLED_NONHALT. Kill file 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.v (894 lines, 980 sentences, sha256 03cda8e9509021e918c20ac00d87da2325d44f6a40ac24f4b4bd33d81ef18940) proves top-level Lemma nonhalt: ~halts tm c0..
• tools/check_kill.sh: PASS 3 times on the same sha256, each with ulimit -s unlimited, ulimit -v 8000000 and no other coqc running.
• Formalizer, 16:49:30Z: compile 4.1 s (native on), coqchk pass 1.3 s (rocq/check_kill.out).
• Independent audit, --json, 16:50:40Z: all 17 checks pass, compile 4.2 s, coqchk pass 1.3 s, 0 assumptions. The audit also confirmed that the string is line 676 of data/holdouts/2026-10-07_778.txt (holdouts.py contains and grep -x). It read all 894 lines and found nothing suspicious: only the Requires Individual62 Lia String List Arith, no Section/Module/Set flags, the three --> notations are the usual abbreviations, nothing re-binds tm/c0/halts/TM_from_str, and the one local c0 intro inside Life_shape does not reach top level. In a separate compile with its own checker file, Print Assumptions printed Closed under the global context, and Print tm matched the string transition by transition.
• Fresh human-readable run for the submission, 16:52:22Z: 17/17 checks PASS, compile 4.2 s (native on), 0 assumptions (closed), coqchk pass 1.3 s (submission/check_kill.txt).
• The proof is the proof.md §8 delta applied to #12's passing .v, and it compiled on the first attempt (rocq/log.md):
• tm string; head state <{{A}} -> <{{F}} in tR1/tR3/tR2/tR3c/conf (9 occurrences); tR3/tR3c (R3', 6-step detour, +4 steps) still close by plain es;
• new Ep_tm2 : Ep W 2 W' -> conf [] (2::2::W) -->+ conf [] (2::2::W') (Life_shape at z = 3, push0_ok at h = 2, Life_tm at L = []), the budget-2 edge lemma of proof.md §5;
• init : c0 -->* conf [] [2;2;1] (48 steps, solve_init); nonhalt with C i := conf [] (2::2::snd i) and cost [] n = 2 by reflexivity (the zero-slack point needs the exact cost);
• everything else (run model, Life, epoch rules, marker words, Inv/Core, main) is #12's text unchanged. Imports Individual62 only from busycoq. Direct proof on the holdout string, not via Eqv.v TM113.eqv.
• Submission package: submission/.
• The .v, unchanged (same sha256).
• proof.md, a copy with updated header, status and AI lines, a "Done as planned" paragraph with a delta-to-lemma map closing §8, and the first §9 gap marked closed. The working proof.md is untouched. Built by rocq/make_submission_proof.py.
• parent-proof.md, a verbatim copy of #12's submission proof.md, because this proof cites it as P§n (same section numbers).
• check_kill.txt (the 16:52:22Z run), README.md.
• discord.md, a draft of 1,825 characters plus <LINK>. Not posted.
• Before posting:
• Post #12's message first. Its twin paragraph says this machine is not formalized; cut it or point it here.
• reports/discord-drafts.md Message 1 (not posted) asks about this machine and #12 as group 3; drop group 3 if it is still unsent.
• Discord #bb6 was never searched for this string; search it first.
• 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.