1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): Bell eats counter = SOMDCv6 TM7 + a "+1 pass at each 110 entered" / – Spreadsheet notes / Discord thread: Results row 1035: class "Bell eats counter"; Status, Notes, Sources, Done By all blank; no links, comments or strikethrough. Not on either Discord list in data/discord/. Its twin 1RB0RA_… (A1=0RA, row 1048) is also open. Viewer: https://bbchallenge.org/1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---

Observation

• The two machines differ in one transition: A reading 1 is 0RF here and 0RC in TM7. The other 11 are equal.
• Configuration at each left record (+2 steps): S(r) = 0^inf 11 D> r 0^inf, where r is a word over the digits L=110, 0=000 and 1=100. No other digit appears up to 1e9 steps.
• r = L^n T: a long run of L digits, then a short counter T.
• n = 0, 1, 3, 6, 8, 14, 19, … reaches 1619 by 1e9.
• There are 209 boundary configs, counting S(1) at step 5, so 208 complete sweeps.
• T (from the first non-L digit) has 1 to 25 digits. It has 1 digit at steps 5 and 16, and 25 at step 550,345,821: T = 1LLLLLLLLLLLL11L0L0000101. 17 boundary configs have |T| ≥ 17.
• T can contain L-runs of up to 12 digits, but it has only 1–11 digits that are 0 or 1.
• 1e9 steps: span 4,902 cells, 4,592 nonzeros, no halt. The span grows ~t^0.34 (2,220 cells at 1e8).
• Tools:
• qsim: block size 3, 1 Diff rule, no acceleration.
• compress: at right records it shows the bell as 0^inf 1^a (011)^b ….
• rulefit: coverage 3%. Its test suite fails 3 Antihydra tests, so its output was not used.
• The rules below come from manual fitting.

The pictures (img/)

Both pairs start from the same constructed configuration: S(L^4 1L1) = 0^inf 11 D> 110 110 110 110 100 110 100 0^inf. Neither machine passes through it from blank. Each pair shows every step, both panels top-aligned at the same scale. To regenerate: python3 -B scripts/compare_tm7.py. - eat_pair.png: one eating pass each, from the start until the eater reads the 1-digit at cell 12. - Both eaters eat the same 4 L's (k = 4). - TM7 makes an 11-step wiggle at each L: back 1 cell, forward 2, back 3, forward 4. - Ours starts the same wiggle. At A1 (its 4th step), instead of turning back, it runs one +1 pass (blue box) and comes back. - Cut ours' 4 passes (38 + 14 + 20 + 2 = 74 extra steps) and what is left is TM7's run: the same state and head cell at every step, 118 − 74 = 44. - sweep_pair.png: one full sweep each. - After the first stop, a drain pass reaches the L at cell 15 and fires A1 in both machines. TM7 turns back. Ours runs +1 pass 5. In both, the eater then restarts. - With the passes cut, the head paths agree up to TM7 step 70. There TM7 reads a 1 at cell 18 that ours' +1s had made 0. - So ours eats 2 more digits (k = 6 vs 4) and drains 6 passes vs 4. - Ours ends at S(L^9 111) after 421 steps, TM7 at S(L^7 101) after 237. Both end with the wall 1 cell further left. - The drain zigzags contain no A1, so they use the same transitions in both machines. Only the blue boxes are extra. - sweep_ours.html and sweep_tm7.html: zoomable viewers of the same two sweeps. Hovering shows the step, state and cell. - A real example (not drawn): ours visits S(L^8 0L11) at step 809. - Both machines eat L^8 0 L the same way (9 A1s). - Then TM7 meets the 1-digit at cell 30: it stops at step 102 with k = 10. - Ours' +1s had turned the next digits into 0s. It eats 3 more and stops at cell 39 at step 381, with k = 13. - The sweeps take 1,121 vs 641 steps. - Removed: the old eater_ours.png / eater_tm7.png. They showed the same 420-step window from that config, which is a different phase for each machine. Ours was still eating (eating ends at step 381). TM7 had finished eating at step 102 and was mostly draining. So the pair could not isolate the difference.

Candidate rules

The digit form is the same as TM7's in SOMDCv6.v.

Sweep: S(r) -->+ S(eat(r)), with the wall one cell further left.

eat is TM7's RIncs hx 0, plus the two clauses marked NEW. Together they say: every L entered fires exactly one +1, whether the eater enters it or a drain pass does.

eater, k:   0 -> L, k+1        L -> L, k+1, +1 to the rest (NEW)        1 -> L, enter count mode with k
count, k>=1: L -> L, back to eater with k, +1 to the rest (NEW)
             1 -> L, k-1       0 -> 0, (k-1)/2 if k odd       0 -> 1, (k-2)/2 if k even
right end:  k=0 -> 1;  k odd -> 0, (k-1)/2;  k even -> 1, (k-2)/2   (repeat)
+1 = little-endian binary over the 0/1 digits; L digits are skipped; overflow appends 1

• Count mode is not "add k to the counter". Each 1-digit absorbs one pass and becomes L. 0-digits and the right end take the leftover count by halving (bijective binary).
• Example: TM7 from S(L^8 0L11). The eater stops at the first 1 of the tail 11 with k = 10, and that 1 becomes L. The second 1 absorbs one pass (k = 9). The right end writes 9 as 0101, giving L^12 0101. Adding 10 to the tail would have given 1011.
• A sweep can have several eat-then-drain rounds. A drain pass that reaches an L restarts the eater: this happens in 115 of the 208 sweeps to 1e9.
• Without the count-mode L clause, the map fits only 95/208 sweeps.

Where the +1 comes from: A1 fires exactly when an L is entered, once per L digit of r in every sweep. - TM7's A1 = 0RC turns straight back. - Ours' A1 = 0RF runs one ordinary h-pass over everything to its right, then comes back. It ends exactly where TM7 is one step after its A1: state C, one cell right of the A1 cell. The only change is that the digits to the right are +1. The pass itself: - B> 100 -> 000 B> (carry); - B> 000 -> <C 100; - B> 110 -> 011 B>, then on the way back 011 <C -> <C 110. - Eater enters L: 1 D> 110 X -> 1 111 D> inc(X) in 6j+13 steps (j = digits before the first 000 in X). TM7: -> 1 111 D> X in 11 steps. - Drain pass enters L: B> 1 110 X -> 1 111 D> inc(X) in 6j+12 steps. TM7: -> 1 111 D> X in 10 steps. The eater restarts there.

Tests (all by simulation; run python3 -B check_rules.py):

Not a cryptid: the rules are counter arithmetic (+1, halving a pass count), with no branching on the parity of huge numbers.

Checkpoint A (Dennis), 2026-10-10

• Q1 (eat_pair): yes, in the EAT phase the rule change is one +1 pass per L entered.
• Q2 (sweep_pair): yes, in the DRAIN phase a pass entering an L fires +1 too. Build by extending SOMDCv6 TM7 rather than from scratch.
• Q3: "bells refill and drain against a creeping right edge" is right-ish; keep sheet class "Bell eats counter".
• His observation while reading: after the first eat, ours has an extra 1 to the right of the head versus TM7; it is absorbed in the next eat phase (5th +1 pass), and the drain leaves extra "icicles" on the right. Consistent with +1 passes changing the counter; the informal proof must cover it.
• Course change caused by Checkpoint A (pilot metric): yes for presentation and description. His objection to the first picture pair led to the skeptic pass, which corrected "TM7 eats silently" (false) and added the drain-pass-enters-L case (115/208 sweeps). The mechanism verdict was unchanged.

Informal proof

Not started (waits for Checkpoint A). Plan: 1. Copy TM7. 2. Add Inductive Inc, proved as sideRLs tm [h] (toRC r) (toRC r'). 3. Put Inc into RIncs_hx_ld (eater enters L) and RIncs_h1_ld (drain pass enters L). 4. Redo RIncs_nxt and the domain lemma; this is the main risk. 5. Prove nonhalt exactly as TM7 does.

Formalization log

Outcome

Card data pass (2026-10-10)

• Figures on the card: Fig 1 = img/eat_pair.png, Fig 2 = img/sweep_pair.png, Fig 3 = img/default_site_1e4.png, Fig 4 = img/records_1e9.png, Fig 5 = img/blaze_1e7.png. Figs 1-3 are the primary figures, shown beside the checkpoint.
• The card's mechanism is cut to 3 bullets. The full list before the cut:
• Tape = wall 11, then 3-cell digits L=110, 0=000, 1=100: a long L-run, then a short counter.
• Sweep: the eater (D) turns digits into a white bell until it reads a 1-digit; then k drain passes (k = digits eaten) rebuild L's; the wall ends 1 cell left.
• A drain pass that reaches an L restarts the eater there (115 of 208 sweeps), so a sweep can have several eat-then-drain rounds.
• Only change vs TM7: A1 fires once per L entered (by the eater or a drain pass). TM7 turns straight back; ours first runs one +1 pass over the digits to its right (6j+2 extra steps), then is exactly where TM7 is one step after its A1 (same state, same cell).
• Drain arithmetic as TM7: a 1-digit absorbs one pass and becomes L; 0-digits and the right end take the rest by halving. The +1s change the digits ahead, so ours usually eats further.
• Questions on the card are Dennis's answered ones (answers in the Checkpoint A section above), marked [answered: yes]; only the PNG names were replaced by Fig numbers.

Kill

• 2026-10-10: KILLED_NONHALT. Kill file 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v (597 lines, sha256 3b29083b31f348bb3172c47b7e51a389b324165d9c38a073a56d9f9a760a651d) proves top-level Lemma nonhalt: ~halts tm c0..
• tools/check_kill.sh: PASS 3 times on the same sha256.
• Formalizer, 11:45:36Z.
• Independent audit, --json: 17/17 checks pass. The audit also confirmed the string is line 301 of data/holdouts/2026-10-07_778.txt and read the file end to end; no suspicious constructs.
• Fresh human-readable run for the submission, 11:48:20Z: compile 3.96 s (native on), 0 assumptions (closed), coqchk pass 1.09 s.
• The proof is SOMDCv6 TM7 plus four changes:
• Inc (one h pass = +1, L skipped);
• an Inc premise in the two L clauses of RIncs;
• zero-pass end clauses Z1/Z0;
• the domain lemma key, with j pending +1s and Inv. Details: proof.md, rocq/log.md, atlas/rocq-notes.md.
• Submission package: submission/.
• The .v, unchanged.
• proof.md, a copy whose status lines are updated to "fully formalized"; the working proof.md is untouched.
• check_kill.txt, README.md.
• discord.md, a draft of 1,371 characters plus <LINK>. Not posted.
• 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 before posting.
• Twin 1RB0RA_… (A1 = 0RA, row 1048) is still open. Per observe.json it uses extra digits 010/011/111, so this proof does not carry over.

Checkpoint B (Dennis), 2026-10-10

• Reviewed by Dennis (review.html, compare.html); approved for posting.

Submission, 2026-10-10

• PR: https://github.com/ccz181078/busycoq/pull/14 (fork DennisKoshta/busycoq, branch nonhalt-, commit 59de137), one file verify/BellEatsCounter_1RB0RF.v, byte-identical (sha256 e434537e…) to the checked kill .v. Named descriptively because a module name cannot start with a digit under -Q . BusyCoq (upstream's old machine-named files fail the same way).
• Verified in a clean clone of the fork at BB6 0940bb9: make, in-place coqc 3.6 s, Print Assumptions closed, coqchk -norec passes.
• Discord post (Dennis, 2 parts): part 2 text in submission/discord/part2.txt; attach submission/discord/_writeup.md (public copy of proof.md: no internal paths, no agent review log).
• 2026-10-10: Discord post made by Dennis (2 parts + write-up attached). Awaiting maintainer response before posting the next family.