1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---

Status: KILLED_NONHALT (2026-10-10): check_kill PASS, independently re-verified; see ## Kill. Before that: CHECKPOINT_B, delta proof from kill #11, validated, scratch .v delta compiled. Label: #11b. Class guess (agent / Dennis): Skelet 1-like Class 2 (sheet). It is kill #11's table 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- renamed by τ = (A,B,C,D,E,F) ↦ (E,A,B,C,D,F), no mirror, started in #11's state B. / pending Viewer: https://bbchallenge.org/1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---

Holdout status and existing work

• Line 511 of data/holdouts/BB6_holdouts_740.txt (the current list), byte for byte: tools/holdouts.py contains exit 0, grep -x -F, od -c. Also line 541 of the 778 list, and on all 27 snapshots. Its eqv_1590 group has no other member.
• Not in busycoq: no row in data/solved_index.tsv, and no file in vendor/busycoq contains the string.
• The sheet credits it to hipparcos.
• Results row 1276: class "Skelet 1-like Class 2", Sources "1", Done By "hipparcos". Status and Notes are empty.
• Level 1 tab, row 44: Sources "1", Done By "hipparcos". Status and Notes are empty.
• Both "1" links go to the Discord thread https://discord.com/channels/960643023006490684/1432566675533992019. The thread ID decodes to 2025-10-28 03:08 UTC. No other cell in the sheet links to it.
• Double-check of Dennis's reading (2026-10-10). Dennis reads the claim, and the alleged completion, as being on kill #33 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---, not on this string. What the data says:
• The Results, Level 1 and Level 0 tabs were re-fetched live on 2026-10-10 (/export?format=csv, HTTP 200). They are byte-identical to the 2026-10-09 export, so the sheet has not changed.
• The hipparcos credit and the thread link sit on this string's rows (Results 1276, Level 1 row 44), and only there.

• 33 is on Results row 1277, directly below: class "Skelet 1-like Class 2", note "Machine with the most common transitions", no Sources, no Done By. #33 is also on Level 0 row 35 ("Fun fact: machine with the most common transitions", nothing else). It is not on the Level 1 tab, and no sheet link points to it. So by the sheet, #33 is unclaimed and this string is the claimed one. Rows 1276 and 1277 are adjacent, which may explain the mix-up.

• We could not read the thread: Discord needs a login, and a web search for both strings finds nothing. If the thread itself is about #33, then the sheet's credit is one row off, and the possible prior work is on #33, which we have already killed. In that case #33's submission needs the same note.
• Decision (Dennis, 2026-10-10). This string is still on the 740 list and carries a claim, so we prove it anyway as part of the #11 family. The submission must say plainly that there may be existing work by hipparcos. (Before this, #11's proof.md §4 and reports/family-sweep.md had set it aside as claimed.)
• Not in data/discord/*. Discord #bb6 was not searched (no access from here).

Observation

• Relation (by table matching and simulation, check_proof.py §S, §R). τ is the only one of 720 × 2 relabelings taking #11's table to this string (12/12 cells). This machine's A is #11's B. The run from blank equals τ(#11's run from 0^inf B> 0^inf) at every step (lockstep to 2·10⁷ steps). From #33's table the only map is CEABDF + mirror, start C; from #33b's, BCEADF + mirror, start D.
• Changed low-level rules: none. #11's 20 window lemmas S1–S6, T1–T14 hold on this table with states renamed by τ: the same windows, the same step counts, and transitions = τ of #11's (§L). F is entered only by D1 (= τ of #11's E1), and it reads 0 every time.
• Macro rules: the same. M and O with #11's formulas, head state A> instead of B> (§A on random instances, §H on every link of #11's chains, on this table).
• Invariant: unchanged. INV is stated on the triples. The base is in class A.
• Init (new). K-configurations from blank:
• 122 K((1,1,2);2,1), 263 K((0,0,1),(2,1,2);4,1), 363 K((3,0,1);5,3), 463 K(;10,5): none in INV;
• then 732 K((1,1,10);8,1), class A (S = 6, T = 0).

#11 from A has its K-configurations at 142, 283, 383 and its base at 483. - 10⁹ steps from blank: no halt. The family sweep (tools/sim/tmsim) measured 77,693 cells and 38,841 nonzeros, against #11's 77,685 and 38,836. Our own long run matched the real machine against the macro model at all 19,332 macro boundaries to step 999,838,005 (check_proof_long.out §D). - Coupling (explanation only, §X). In triples, the macro orbit equals #33b's from macro step 0, except for one top-digit exponent that is larger by 1. It equals #11's from macro step 54, except for one top-digit exponent that is larger by 4. The same rule fires at every macro step. Checked for 1.2·10⁶ macro steps (t ≈ 3.7·10¹²). - No card or images were made: the mechanism is #11's, and #11's card shows it.

Candidate rules

11's rules, verbatim, with the K head state A (proof.md §1). Tested on this table:

• M 700/700, O 350/350, and random INV states 2,846/2,846 for one macro step (§A);
• 37,220 M chains and 9,995 O chains (O including m = 0), link by link (§H).

The real run from blank equals the rules at every macro boundary from step 732: 3,384/3,384 to 3·10⁷ (default), and 19,332/19,332 to 10⁹ (§D).

Checkpoint A (Dennis)

No card. It is not blocking: confidence is high, because the table, the rule statements and the invariant are those of kills #11 and #33b.

Informal proof

proof.md is a delta proof from #11's proof.md. It has: - the map τ and Lemma R (§0); - what carries over (§1): rules, INV, closure, progress; - what changes (§2): the init and the base; - the complete argument (§3); - the couplings with #11 and #33b (§4, explanation only); - the .v delta (§5).

check_proof.py imports #11's check_proof.py read-only. SUMMARY PASS, sections S, R, L, A, H, C, D, B, G, X, V. - Default run: 23 s, check_proof.out. - Long run --seed 2026 --tm-steps 1e9 --orbit 1.2e6 --induct 6e5 --lockstep 2e7 --no-rocq: 122 s, check_proof_long.out.

Formalization log

• 2026-10-10, scratch check only (stage informal_proof). rocq/make_delta.py applies proof.md §5 to #11's passing .v (sha256 8bca47b1…53c0):
• the TM string;
• τ on every {{X}}: B 22 → A, C 18 → B, D 5 → C, E 18 → D;
• init : c0 -->* K [d1 1 10] 8 1 (732 steps, the same solve_init) and the base in nonhalt;
• comments.

The result is rocq/delta_check.v (696 lines, sha256 58e9e640…88ca). rocq/compile.sh: Coq 8.20.1, 8.4 s, exit 0, Print Assumptions nonhalt: Closed under the global context (rocq/delta_check.out). It compiled on the first try, with no tactic changes, so nothing is new for atlas/rocq-notes.md. - Not done (the kill stage): copy to machines/<tm>/<tm>.v with a house-style header, run tools/check_kill.sh, an independent audit, and the submission package. The package needs #11's submission proof.md attached as the parent and the existing-work note.

Outcome

Open (CHECKPOINT_B). Next: the kill stage, then a submission that says plainly that hipparcos may already have worked on this machine.

Before posting: - #11's and #33b's twins paragraphs, and #11's notes, still call this machine claimed or not formalized. Update them. - If the thread turns out to be about #33, add the same note to #33's submission.

Kill

2026-10-10: KILLED_NONHALT (fourteenth kill). tools/check_kill.sh PASS, independently re-verified. - Audit (independent, on the formalizer's file sha256 7fc83eeb…2ae3, 701 lines): check_kill exit 0, all 17 checks; string at line 541 of the 778 list (once); whole .v read; Print Assumptions nonhalt closed; header claims (tau, the 732-step base, SBCv6 TM21, #11's .v hash) re-checked. One cosmetic finding: header lines 2, 7, 11 and the line-277 banner used internal labels ("kill #11", "#11's .v"). - Final file sha256 153aa11aeb194c31281cc26d9ff28cacf6868c67ea16ebdb44ce3ecbec22290a, 702 lines, 756 sentences. Comment-only edits to the audited file: the header and the invariant banner now say "the parent" (with #11's full string on line 2) instead of "#11", and the informal proof is "the accompanying write-up (proof.md, a delta proof that cites the parent's write-up, parent-proof.md, as P section n)". With comments stripped, the code is identical to the audited file. Fresh check_kill on the final file: RESULT: PASS, exit 0, compile 9.17 s (native), coqchk -norec 1.79 s, 0 assumptions, 12.3 s wall (submission/check_kill.txt). - Existing work, re-checked. data/discord/2025-10-27_hipparcos_1RB0RB.txt (the thread's opening posts, pasted 2026-10-10) is about this string, 1RB0RB_…, and not about #33's 1RB0RE_…. So the sheet's credit (Results 1276, Level 1 row 44) is on the right row. The posts are an analysis: block rules over an RLE tape, a stride acceleration, digit-collision cases, and the hypotheses "first-group exponents never reach zero, second-group exponents stay even". hipparcos writes "I don't have enough analysis to prove that yet". Later posts were not pasted. #33 needs no hipparcos note on this evidence. The "not in data/discord/" lines above, and check_proof.py §S, predate the paste. - Package submission/: the .v (= the checked file), proof.md (public delta write-up rewritten from proof.md: header, summary, §0–§6, no process material; tools/writeup_lint.py 0 errors, 0 warnings), parent-proof.md (#11's submission proof.md, verbatim, cited as P§n; lint 0/0), check_kill.txt, README.md, discord.md (1,472 characters before the link; not posted). The README, the write-up and the .v header carry the line "There may be existing work on this machine by hipparcos (marked done on the community sheet, not yet in busycoq)." They also credit the thread's analysis and say the proof is adapted from #11's, not from the thread. - Before posting:* #11's discord draft says only that this machine "reaches the same invariant in simulation". #33's and #33b's drafts and READMEs say it is "not formalized". Update them. Post #11 first, or the whole family together. Read the rest of hipparcos's thread first.