1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA

Status: KILLED_NONHALT (2026-10-10; F3 of reports/family-sweep.md; delta proof of kill #4; see ## Kill at the bottom) Class guess (agent / Dennis): Sync bouncer counter. It is kill #4's table renamed by σ = EDBCFA, with no mirror, started in #4's F / pending Spreadsheet notes / Discord thread: Results row 915, "Sync bouncer counter", no status, notes or done-by. - Holdout list: line 17 of data/holdouts/2026-10-07_778.txt, byte-exact. Eqv member: 1RB0LC_1LC0RB_0LD1LA_0RA1LE_0LA1LF_1LD---, line 24 of the 1590 file. - On mxdys's UBRRBA_TODO (line 45) and dyuan01's Oct 1 longitudinal list (line 7). Both are fair game, and #4 was on both too. - Vendor: only Eqv_v2.v TM7 tm', an equivalence lemma with no nonhalt proof. - Parent: machines/1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC--- (#4, KILLED_NONHALT). Viewer: https://bbchallenge.org/1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA

Observation

• Relation. σ: A→E, B→D, C→B, D→C, E→F, F→A. It is the only one of the 720 renamings (each with or without a mirror) that maps #4's table to this one. The twin's start A = σ(F).
• So the twin's run is #4's machine run from 0^inf F> 0^inf, relabelled: lockstep identical for 2e6 steps.
• That run is not #4's own run. From F the parent has 0^inf 1 C> 0^inf at step 1; from A it has 0^inf 1 0 C> 0^inf at step 2. So the two runs are different orbits of the same macro map, not trajectory twins.
• Words. Same as #4: P/Q families, counter digits 1010/0010, A = 00111, B = 10111, front 111. Right-edge head state B = σ(C); moving head <E 001 / 001 F>.
• Early history. P(3,7,1,2) at step 399 has X = 1, so R2 does not apply there and the start is irregular. From Q(5,20,3,1,0) at step 1,711 every canonical transition is rule-predicted: R5, R1^4, R2, R3^2, R5, R1^3, R2. That reaches S(6,14,4) = Q(7,65,1,14,4) = CfgF 5 0 14 4 at step 16,590. The parent reaches S(6,16,0) at 17,215.
• Orbit. S(k,Y,Z) at k = 6..15: (14,4), (25,29), (68,2), (104,115), (271,186), (594,−31), (860,888), (2178,1485), (4752,2348) at 1,268,929,120 steps, and (9476,4529) at 5,039,089,135. All are in the hexagon.
• Branches: even, odd, even, even, odd, then even for the rest.
• One R5o, with m = 31 (Q(11,1430,271,1,321) → Q(12,2142,63,532,0)).
• All 9 cycle states and all 43 phase boundaries are hit by direct simulation at the exact predicted steps.
• Size. At 1e9: span 29,054 cells (parent 23,607, so +23%). At 3e9: 47,451 cells (−30..47,420) and 18,841 nonzeros, no halt.
• Diagrams (tools/diagram.py).
• img/records_2.7e6.png: --mode records --steps 2.7e6 --scale 2; 1,406 rows, cells −20..1385. Overflow rows are 78, 122, 306, 390 and 1,139.
• img/every50_cycle7_from_base.png: --mode every:50 --steps 58294 --scale 2 --from-config "$(cat work/base_cfg.txt)". This is the base config; the real tape at 16,590 is identical, as checked in check_proof §I. Cells −130..177 relative to the head, which is real cells −16..291.
• img/every16_init.png: --mode every:16 --steps 16590 --scale 2.
• img/default_site.png: --as-site.
• Summaries are in work/dg_*.json.

Candidate rules

4's 21 shift rules and R1, R2, R3, R4, R5, R5o (R4o as a remark), verbatim with the head states renamed.

• Shift rules: exact on the twin's own table, with the same step counts; A1 is never read.
• Macro rules: 40/40 random instances per rule, from the parent's runner prediction checked against direct twin simulation.
• Twin from blank: from step 1,711 to 3e7, all 857 canonical right-edge visits match the rule runner in configuration and step (check_proof §C; list in work/canon_3e7.txt). The other 12 right-edge B visits are the start or mid-conversion.

Checkpoint A (Dennis)

Card questions in observe.json. They are non-blocking, and confidence is high.

Informal proof

proof.md, a delta proof (2026-10-10). - Unchanged: rules, cycle lemma, hexagon. Adjusted invariant: none. - Changed: only the init. c0 →(16,590) S(6,14,4); Inv 5 0 14 4 holds, with 4Y+2Z ≥ N tight (64 = 64), like the parent's base. - check_proof.py: ALL CHECKS PASSED (S, L, A, M, I, C, B, H, O) in 7 s (check_proof.out). With --kmax 15 it extends the orbit to 5.04e9 (22 s, check_proof_k15.out).

Formalization log

• Plan check only: rocq/make_plan_check.py applies proof.md §5 to #4's .v (sha256 51e3dea1…, 504 lines).
• It renames the TM string and {{A}}→{{E}} ×37, {{C}}→{{B}} ×6, {{E}}→{{F}} ×35.
• It sets init0 = esx to CfgF 5 0 14 4 and the start index to (5,0,14,4).
• rocq/plan_check.v compiles in 6.7 s (rocq/compile.sh, native on), and Print Assumptions nonhalt is closed (rocq/plan_check.out).
• Next:
• Write the kill file <tm>.v with the same content and a clean header, with the comment-block state letters renamed.
• Run tools/check_kill.sh.

Outcome

KILLED_NONHALT (2026-10-10). See ## Kill.

Kill

• 2026-10-10: KILLED_NONHALT. Kill file 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v (510 lines, 532 sentences, sha256 0c89b5109f87c793105cadaa9b157902254e5b8e33d1f9bc610d76b9f7a43e37) proves top-level Lemma nonhalt: ~halts tm c0..
• tools/check_kill.sh: PASS 3 times on the same sha256. The audit and submission runs used ulimit -s unlimited and ulimit -v 8000000, with no other coqc/coqchk/check_kill running.
• Formalizer: compile 6.5 s (native on), coqchk pass 2.1 s, closed (rocq/check_kill.out).
• Independent audit, --json, 19:23:15Z: 17/17 checks pass, compile 6.9 s, coqchk pass 2.2 s, 0 assumptions. The audit also confirmed the string is line 17 of data/holdouts/2026-10-07_778.txt, byte-exact and once (holdouts.py contains, grep -x count 1). It read all 510 lines and found nothing suspicious: the only Requires are Individual62 and stdlib Arith/Lia/String; no Section/Module/Variable/Context/Axiom/Parameter/Admitted/Opaque/Set/Unset/Extract/Declare/Load; local notations only, no shadowing; nothing after nonhalt but the closing comment. The header is house style, with no repo-local paths.
• Fresh human-readable run for the submission, 19:25:05Z: 17/17 checks PASS, compile 7.0 s (native on), 0 assumptions (closed), coqchk pass 2.1 s (submission/check_kill.txt; raw copy rocq/check_kill_submission.out).
• The proof is the proof.md §5 delta applied by rocq/make_kill.py to #4's passing .v (sha256 51e3dea1…e923, 504 lines). It compiled on the first attempt (rocq/log.md):
• the TM string;
• σ = EDBCFA on every {{X}} in one re.sub (counts asserted: A 37, C 6, E 35);
• init0 (one esx, 16,590 steps) and init : c0 -->* CfgF 5 0 14 4;
• start index (5,0,14,4);
• header and rule-table comments. After the renaming, 4 code lines differ from #4's .v. The 22 es shift lemmas, the counter, QC, R1–R3, the Gad conversion (ConvNo/PostOV/ConvOV -> Conv0/Conv1/Conv1o), Inv, cycle_step and nonhalt's final unfold Inv. cbn. lia. (tight facet 64 <= 64) are #4's text. Imports Individual62 only. Direct proof on the holdout string; Eqv_v2.v TM7 is not used.
• Submission package: submission/.
• The .v, unchanged (same sha256).
• proof.md, a copy built by rocq/make_submission_proof.py (single-match replacements; refuses to write if a repo-local path is left): new title, header (lists, parent pointer, evidence, status, AI line), §5 "done as planned" paragraph with a delta-to-lemma map, one file mention dropped in §6, and §7. The working proof.md is untouched.
• parent-proof.md, a verbatim copy of #4's submission proof.md, because this proof cites it as P§n (same section numbers).
• check_kill.txt (the 19:25:05Z run), README.md.
• discord.md, a draft of 1,629 characters plus <LINK>. Not posted.
• Before posting:
• Post #4's message first (row 921; its draft is also unposted), or post the two as a pair.
• Both are on dyuan01's Oct 1 longitudinal list and mxdys's UBRRBA_TODO. Re-read the longitudinal thread and search Discord #bb6 for this string (never searched; our exports mention it only in those two lists).
• The draft says the result also settles the eqv-class member 1RB0LC_1LC0RB_0LD1LA_0RA1LE_0LA1LF_1LD--- via busycoq's Eqv_v2.v TM7 (its tm is the member's mirror, checked by check_proof.py §S, not in Coq). Drop that sentence if Dennis prefers.
• 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.