1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB (W4-1)

Status: CHECKPOINT_B (observe done 2026-10-10, confidence high; proof.md reviewed by skeptic round 1 on 2026-10-11, five minor gaps fixed). Not a cryptid candidate. Class guess (agent / Dennis): Bell eats counter, partial eat with residue (= kill #30's table, another start) / - Spreadsheet / Discord: results.csv row 1046, class "Bell eats counter", status/notes/sources/done-by blank; classifications.csv row 43 only lists it. Not in data/discord/*.txt. Not in upstream busycoq verify/ (pr3 checkout, feeffa1 on BB6 HEAD 9cf9e88; no hit for this string, #30's or #7's). holdouts.py solved: no byte-exact, renamed or mirrored proof. Holdout lists: byte-exact line 590 of data/holdouts/BB6_holdouts_740.txt (grep -nxF), line 626 of 2026-10-07_778.txt; in all 26 snapshots since 2024-06-14. Equivalence group (778 eqv file): singleton. Viewer: https://bbchallenge.org/1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB

The table is kill #30's

• sigma: #30 -> W4-1 = A->E, B->A, C->B, D->C, E->D, F->F (no mirror). W4-1 cell sigma(q),r = sigma(#30 cell q,r) for all 12 cells (scripts/check_w41.py section S, 12/12).
• So W4-1 from blank = #30's table run from 0^inf B> 0^inf (#30's names), a different orbit of the same macro map.
• canon over all starts (scratchpad starts.py + canon on both lists): the table has three holdouts:
• 740 line 710 = #30 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC (start #30's A; KILLED_NONHALT, claimed, not submitted);
• 740 line 590 = this machine (start #30's B);
• 740 line 381 = #7 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA (start #30's E, mirrored; at CHECKPOINT_A, confidence med, from its own closure/CTL stages).
• Start F (W4-1's F = #30's F: writes 0 and steps right into #30's A, i.e. #30's own run one step later) and the starts that halt at once (W4-1's B, C) are not holdouts.

Observation

• 1e9 steps: no halt; span -274..7451 (7,726 cells), 4,057 nonzeros (sim_1e9.jsonl). #30 at 1e9: 7,720 cells, 4,642 nonzeros.
• Left-record log to 1e11 (scripts/lrec.c, table parsed from the string at run time; data/lrec_1e11.txt): no halt in 1e11 steps; 520 left records entered in E with tape 0^inf <E 101 (001)^k T 0^inf, the last at step 99,729,345,754 (k = 12,697). Left edge moves 2 cells per epoch.
• qsim (block 3, 20k loops; data/qsim.jsonl keeps the start, rule and end events): 3 single-use diff rules, nothing recursive (as for #30). compress track (direct, 1e8, data/compress_track.txt): the hub skeleton 0^inf (110)^a 0 (011)^b ... and nested sub-hubs ... 1 (110)^c 1^5 (011)^d ... inside the right part (the D6 sub-epochs).
• Notation (W4-1 names): hub K(a,b,X) = 0^inf (110)^a 0 (011)^b B> X 0^inf; pre-record L'(k,Y) = 0^inf <D 01 (001)^k 000 Y 0^inf; left record L(k,T) = 0^inf <E 101 (001)^k T 0^inf (D0 = 1LE turns L' into L in one step).
• Start: blank -> L'(2, 1) at step 41 -> L(2, 0001) at step 42 -> K(1, 3, 1) at step 55 (img/explore_init_60.png). There is also a transient left record L(0, '') at step 4. #30's start is K(1, 8, 010001) at step ~330.

Rules (all of #30's, renamed; validated on W4-1's own table)

Words and the model are those of #30's .v (Section 2 and 5): blk d e w = d01 (001)^e 000 w, p11 x w = 11 (001)^x 000 w, p01 x w = 01 (001)^x 000 w, p00 w = 00 w, p10 w = 10 w, tails t0..t3 = '', 1, 010001, 110001. scripts/vmodel.py is a Python mirror of the .v's lpf/phif (fuel included) and Inv; it reproduces #30's fin694 exactly (orbit 100000 691 8 t2 = (17713, Y694), Inv 10).

Random words: the top-level constructor is drawn uniformly (tails, a/b blocks over G or nested H words, p11 x >= 1, p11 0, p01, p00, '10' + a-block, '10' + b-block (D6 trigger), the constant end words, H words). The eat cases: E1 (even), E2 (odd), E0, Et1-Et3, eats at constant words.

Finite part and invariant (sizing for the .v)

• orbit 100000 691 3 t1 = Some (17712, Y691) in the Python mirror, with Y691 = p11 10 (blk false 10 (blk false 6 (blk true 1 (blk false 1 (blk true 1 (blk false 1 (blk true 1 (blk false 1 (blk false 1 (blk true 1 (blk false 0 t0))))))))))).
• Inv 11 17712 Y691 holds (k = 11 is the only choice: 11 blocks, and Nlo 12 = 28,672 > N; corrected 2026-10-10 in the informal_proof stage, it was misprinted here as 31,744). It is the first epoch of the orbit where Inv holds for any k.
• Fuel: the minimum fuel left over 1,200 epochs (to N = 33,240) is 66,761 of 100,000, so #30's fuel constant is fine.
• Cost: #30's fin694 ran 691 epochs from N = 8 to 17,713 in ~1 s of vm_compute; this one is the same length.

• 30's proof.md threshold (N* = 14,796): first reached at epoch index 591 from K(1,3,t1), N = 14,797 (check_proof.py F9; corrected 2026-10-11, was misprinted here as "epoch 593 (590 epochs from the start)").

Template check (our kill #30's .v)

• 30's .v (1,726 lines, check_kill PASS, sha256 93a493f5...0c0): sections 1-10 are statements about #30's table and words; only Section 4 (init : c0 -->* K 8 t2) and Section 11's finite part (fin694, inv694, the nonhalt call) depend on the start.

• Rule set compared: #30's word-level rules (LP constructors LP_a ... LP_T6, Phi_B/E1/E2/E0/Et1-3, D6 = LP_6, Rst) are exactly the rules validated above under sigma; nothing new appears on W4-1's orbit (the model never returns None in 1,200 epochs and matches every TM left record).
• Two routes for the .v, both small: 1. Rename (#25/F2 recipe): TM string, sigma on the state names (#30's .v names only A, C and E: 23 {{A}}, 28 {{C}}, 8 {{E}}, in the Section 1 es lemmas, LPspec/Phispec, K and Rst; simultaneous A->E, C->B, E->D), init : c0 -->* K 3 t1 (solve_init, 55 steps), fin691 : orbit 100000 691 3 t1 = Some (17712, Y691), inv691 : Inv 11 17712 Y691. inv_step/LP/Phi/potentials verbatim. 2. Conjugacy (#24 recipe without flip): keep #30's development as tm30, prove ~ halts tm30 (B;; tape0) with the new init and finite part, then Perm tm tm30 phi (phi = sigma^-1) and busycoq's perm_halts. No edits inside the es lemmas. #7 needs the same plus flip_halts.
• Verdict: applies: yes. Both routes have since been built as drafts and pass check_kill (skeptic round 1, proof.md §8.3: route A fe781969..., route B c81ad0ae..., 0 assumptions). Route B is the one for this file: one TM literal, no bridge, no check_kill warning. Route A's progress_nonhalt_cond tm needs the one-token edit to tm30.

Cryptid check (ground rule 6)

Same macro map as #30, whose non-halting is proved in Rocq for every epoch satisfying Inv. Branching is on the counter's low digit (E1 vs E2) and the nested D6 levels; the halting condition (an eat before digestion ends) is excluded by a size inequality with growing slack, already formalized. Not a cryptid candidate.

Siblings

• 30 (740 line 710): the template, killed.

• 7 (740 line 381): checked here too. Its mirror image 1LB0LA_1RC0RD_1RE1RD_0RB0LE_1LF0RA_---0LA logged to 1e10 (left records in B): from L(16, 0001) at step 1,059 the model predicts all 257 later records exactly (scripts/sib7_check.py); the four records before it are transient words the model does not parse. Model from K(1,17,t1): Inv first holds after 687 epochs at N = 17,724 (k = 10 or 11). So #7 is covered by the same .v recipe plus flip_halts (init to K 17 t1 at about step 1,060).

Orbit merge (found in the informal_proof stage, not a premise)

• The model orbits of W4-1 (from K(1,3,t1)) and #30 (from K(1,8,t2)) first share an epoch at index 795 of both (N = 20,922) and are identical from there on (check_proof.py section C). Before index 795 they are distinct. This is why #30's Lemma D run to N = 400,000 gives the same 11,074 epochs on both.

Non-halting argument

blank -->* K(1,3,t1) (I); 691 model epochs (each sound: #30's model_sound + epoch_tm) reach K(1,17712,Y691) with Inv 11; #30's inv_step (proved for every k, N, y) keeps Inv forever and every step is an epoch K N y -->+ K (S k) y'; progress_nonhalt_cond gives ~ halts. Nothing in this chain depends on the start except I and the finite computation, both of which are closed computations Rocq checks.

Checkpoint A (Dennis)

Questions in observe.json -> checkpoint_questions. Non-blocking: proof.md (delta write-up) and the .v can start now.

Files

scripts/lrec.c (left-record logger, table from argv), scripts/vmodel.py (mirror of #30's lpf/phif/Inv), scripts/check_w41.py (rule validation on W4-1's table, model vs TM log), scripts/lemmaD_w41.py (#30's check_proof section D from W4-1's start), scripts/sib7_check.py (#7). Data in data/, figures in img/.

Kill

• 2026-10-11: KILLED_NONHALT. Kill file 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v (1,755 lines, 2,012 sentences, sha256 1d62b3e870e268e07e46593c66f9d8ac0106a44da0856e7f53785204376e9328) proves top-level Lemma nonhalt: ~halts tm c0.. It is #30's kill file renamed by sigma (route B: A->E, C->B, E->D on the 59 {{X}} tokens, all in statements), with init : c0 -->* K 3 t1 (55 steps, solve_init), B691/Y691/fin691 (orbit 100000 691 3 t1 = Some (17712, Y691) by vm_compute), inv691 : Inv 11 17712 Y691 and the nonhalt call (nonhalt_from 17712 Y691, exists 11). One TM literal, no bridge. Header cites "verify/FractalBEC.v, tm10" through "our proof for the parent".
• tools/check_kill.sh: PASS 3 times on the same sha256, each with ulimit -s unlimited and ulimit -v 8000000, one check at a time.
• Formalizer (round 1): compile 14.7 s (native on), coqchk -norec 65.7 s, 0 assumptions, no tm_text warning (rocq/check_kill_final.log).
• Independent audit, --json: 17/17 PASS, compile 14.8 s, coqchk -norec 65.1 s (no timeout), 0 assumptions. It also confirmed line 626 of data/holdouts/2026-10-07_778.txt (holdouts.py contains), read the whole file, and diffed it (comments stripped, sigma applied) against #30's kill file: only the TM literal, init, the finite part, inv691 and the nonhalt call differ.
• Fresh human-readable run for the submission, 00:29:43-00:31:03 PDT (checked_at 2026-10-11T07:31:03Z): 17/17 PASS, compile 14.3 s (native on), coqchk -norec 63.5 s, 0 assumptions (closed), about 80 s wall (submission/check_kill.txt). No warnings beyond the usual compile ones. The watchdog showed about 20 GB available just before, and nothing was killed.
• Submission package: submission/.
• The .v, unchanged (same sha256).
• proof.md: the public delta write-up, rewritten from the working proof.md (sha256 a36b4c9a…, untouched). Header (lists, parent, template FractalBEC tm10 via the parent, status, section map) + Summary + §1-§7 = the working §0-§7 with the math unchanged (W4-1/#30 written as "this machine"/"the parent", #30's write-up cited as "parent §n", the vmodel.py and observe-stage remarks reworded) + §8 the formal proof (the route-B delta as a description of the .v; the route-A plan, drafts, generators and scratchpad paths dropped) + §9 numerical checks (§9 of the working file without script names; [K] and [X7] dropped) + §10 siblings (#7 named by string). The working §11 (Checkpoint B) and the review log are dropped. tools/writeup_lint.py: 0 errors, 0 warnings.
• parent-proof.md: #30's public write-up (submission/proof.md of #30, verbatim, sha256 102acb07…), cited as "parent §n". Lint 0/0.
• check_kill.txt (the 00:31:03 run, verbatim; contains absolute local paths like the other packages' copies), README.md (lint 0/0).
• discord.md: a draft of 1,375 characters plus <LINK>. Not posted. Its before-pasting list: post #30 first or the three starts as one family (with an optional sentence for that); #7's draft note 3 still calls W4-1 not killed; search #bb6 first; PR #15 queue; Checkpoint B Q2 (the orbit merge is mentioned as a remark); numbers; check_kill.txt paths.
• Still open: Dennis's Checkpoint A/B answers (non-blocking; observe.json checkpoint_questions incl. "submit the three together?", proof.md §11).