W6-4 1RB0LE_1RC1RB_1LD0RE_1LA1LC_1RB0LF_0LC---

740 list line 412. Sheet class "Chaotic Bell Class 1" (results row: no status, no notes, no "done by"). Wave 6 pick (CB1 cluster): the halting go/no-go with a port of ccz181078's certified CB1 executor.

Stage 1: Observe (2026-10-14)

Outcome: NO-GO for the HALT route (no halt found); rules exact; parked as STUCK. - The machine is ChaoticBell1Halt.v TM13's table, renamed, started in TM13's state D. All of TM13's rule lemmas hold here verbatim (26 rules + the halt window validated 40/40 each from random instances). - A Python port of ccz181078's certified executor (CBSim) reproduces the two upstream halts exactly (TM13 at tick 64,832, TM7 at tick 65,400) and matches direct simulation tick by tick for 4,000 ticks. - From our blank start the port runs 16,551,000 ticks (165x ccz181078's 100,000-tick budget) without a halt; the same table from 602's start (TM13's C) runs 10,000,000 ticks without a halt; from 299's start (TM13's B) 7,627,000 ticks without a halt. - New observation: after about 410^5 ticks the run leaves the chaotic phase (the phase where TM13 halts) and settles into a regular phase*: the left part is a stack of runs PL(n)^k_n for n = 0, 1, 2, ... with counts near 10^31 that shrink by a factor of about 5 every two levels (k_n - 5 k_(n+2) is small: 0..8, sometimes -89..178). The executor then spends 94% of its ticks on Pairs/Returns and the tape only grows from 10^31 to 10^33 cells in 10^7 ticks. A "divide by 5 with small remainders" law is a cryptid warning sign; whether it closes is open.

Checks

• Byte-exact: grep -nxF finds it at line 412 of data/holdouts/BB6_holdouts_740.txt.
• Claims: none. It appears only in data/sheet/2026-10-09_results.csv (class only), ..._classifications.csv (column "Chaotic Bell Class 1") and ..._direct-simulation.csv (columns "not simulated up to 1e14 / 1e15", i.e. the maintainers ran it to 10^13 steps without a halt). Nothing in data/discord/*.txt.
• Claimed in coord/claims.tsv as Wave 6 W6-4 (no Astra line for this machine or class).

Same table as TM13 of ChaoticBell1Halt.v

• Upstream verify/ChaoticBell1Halt.v (ccz181078, busycoq BB6 HEAD cdaf693) proves halts tm c0 for TM13 = 1RB1RA_1LC0RE_1LD1LB_1RA0LE_1RA0LF_0LB--- and TM7 = 1RB1RA_1LC0RD_1LD1LB_1RA0LE_0LB1LF_1RC---.
• State map ours -> TM13: A->D, B->A, C->B, D->C, E->E, F->F, no mirror (brute force over all renamings, work/mapfind.py). So our blank start = TM13 started in its state D.
• canon() per start state of our table: start B = TM13 from A (proved HALT upstream; not on the 740 list), start C = 299 (1RB0LE_1RC1RA_1LD0RE_1LA1LD_1LD0RF_0RA---, TM13 from B, mirrored), start D = 602 (1RB1RD_1LC0RE_1LD1LC_1RA0LE_1LC0RF_0RD---, TM13 from C, mirrored). Starts E, F: on no list.
• 338, 577, 730 are not this table (canon differs for every start of TM13 and of TM7); the wave-6 ranking pairs them with TM7 through their eqv members. Cousins, not siblings.

Notation (CB1 of ChaoticBell1Halt.v, renamed to our states)

Paper order (left part far-to-near, right part near-to-far). D n and S n are the two spellings of a digit n >= 0.

Rules (all are lemmas of ChaoticBell1Halt.v TM13; table-specific, so they hold verbatim here)

Validated here by direct simulation from random instances (random parameters, random left and right context), work/cb1_rules.py -> work/cb1_rules.json: 26 rules + the halt window, 40/40 each.

Plus blank, even, collision, turnB, defect0/1/2, defectBlank0/S, paired, scanR/B/C, scanPair (statements in work/cb1_rules.json).

Mechanism

• A bell: the head sweeps the whole tape. Going right (R) it turns each digit D n into S n; at the right end it appends two zero digits (emptyR) or meets a 10 marker (collide / pairR / defects). Going left (L) it turns S n back into D n.
• The left part is a stack of loop counters. A group 111 in front of (01)^(b+1) launches one full sweep to the right end and back (one "call"); PL blocks (made by pairR from two equal digits) replay 2n'+1 calls and then increment a digit (finishPL + J). At the far left end the counter 0^inf 1^(2b) ... turns the head around (over1/over2) and the tape grows.
• What the digit list does over time is chaotic (sheet class name). The same rules make TM13 (start A) halt after 64,832 executor ticks: the leftward sweep meets 11100 (the halt window) in an old fragment near the left end. Whether our start ever produces that window is only decided by running.
• Direct simulation: no halt to 10^9 (span -518..36,471, 22,051 ones). At every visit of the left end (to 210^9) the tape is a clean list of D digits (odd 1-runs separated by 00): 4,609 digits, largest 33, span 47,146 at step 1.610^9; span grows like sqrt(steps) (work/left_visits_2e9.json).
• compress.py track (10^7, records): the right edge shows the calls macro, 1^a ... (110)^b, a -3 and b +2 per visit (one 111 consumed, two zero digits appended per call). qsim: 1.19*10^6 steps in 20 s (no useful acceleration, as the ranking said).

The certified-executor port (work/cbsim.py, work/cbsim_fast.py)

• Untrusted Python transcription of Runs, RunMachine, CBExec, CBMacros and CBSim (same fuels: remove_fast 512, scan 512, normal 512, small <= 512, the 2^80 skip limit; use checks every rule instance; failures fall back to a raw step). It runs TM13's table under TM13's names, so our machine = start D.
• Checks: TM13 from A halts at tick 64,832, TM7 from A at tick 65,400 (both inside ccz181078's 100,000-tick fuel, as the upstream proofs require). The first 4,000 ticks from start D are each found, in order, in the direct simulation (exact tapes; 21,071,295 direct steps). The cons-list variant gives identical tick counts and rule statistics.

Template check (ChaoticBell1Halt.v, Module TM13 + shared CB1/CBMacros/CBSim)

• Rule sets: identical. Every TM13 lemma (scanR, scanB, scanC, scanPair, ones, right, left, blank, even, restart, overflow1/2, collision, leftJ, turnB, turnJ, finishP, defect0/1/2, defect_blank0/S, paired, halt_window, core) is about the table only; after renaming B->A, C->B, D->C they are our lemmas.
• Difference: only the start. CBSim's initial is Cfg [] [] A R with A = TM13's A; for us it is our A = TM13's D. A HALT .v would copy the CB1/CBSim modules with the state letters renamed (mq, align, choose, ScanB/ScanC...), use our TM string, and run check_spec with fuel above the halting tick.

Cryptid check

• Local rules: exact and closed (26/26 validated); no arithmetic in them beyond +1/+2 on digits.
• Early phase (to ~4*10^5 ticks): chaotic digit-list rewriting (the phase in which TM13 halts at 64,832 ticks). No closed law.
• Late phase (from ~4*10^5 ticks, seen from two starts): a regular stack of PL(n) runs whose counts fall by about 5 every two levels, with small non-zero remainders (k_n - 5 k_(n+2) in -89..178). A per-level "divide by 5 with remainder" law is the cryptid warning sign named in the ground rules, but the law itself is not fitted yet, so no cryptid flag today: status STUCK, with the fit as the next stage and the cryptid protocol as its stop rule.

Long executor runs (work/cbsim_TM13_{D,C,B}.json, logs *.log.jsonl, checkpoints ckpt_TM13_{D,B}.pkl)

• Tape growth from our start: 10^7 cells at 210^4 ticks, 10^21 at 1.810^5, 10^31 at 4.210^5, then only 10^32..10^33 up to 10^7 ticks. 602's start: the same shape (10^31 at 5.410^5).
• Rule mix over the whole run: 602 start (10^7 ticks) Returns 5,053,257, Pairs 4,285,040, raw 184,422; our start (16,551,000 ticks) Returns 8,883,943, Pairs 6,982,472, raw 189,473.
• The regular phase at tick 8*10^6 (our start; checkpoint since overwritten by the final one at 16,551,000): right part B> 0100 10 (1^7 00)^(1.5*10^30) 11100 (100)^(4.9*10^32); left part, nearest first: PL(0)^(2.0*10^31), separators, PL(1)^(4.9*10^31), ..., PL(73)^(3.4*10^6), each level separated by short (01)^a 11^b 101 101 groups. Counts: k_0..k_5 = 2.00e31, 4.91e31, 4.16e30, 9.81e30, 8.32e29, 1.96e30; ratios alternate 2.3578 and 0.0848 (product 1/5).
• Final checkpoints (16,551,000 ticks for our start, 7,627,000 for 299's): the same stack, now starting at PL(3) (the near levels PL(0..2) are used up), 80 and 79 levels with counts above 10^3, and again k_n - 5 k_(n+2) in -5..13. So the executor eats the stack from the near end at roughly one level per 310^6 ticks; at that rate the bottom (~80 levels) is ~210^8 ticks away, beyond a Python run but not beyond a level accelerator.
• Port variants: cbsim.py (plain lists), cbsim_fast.py (cons lists), cbsim_fast2.py (+ memoised skip_block equality, checkpoint/resume). All three give identical logs where they overlap; fast2 reproduces both upstream halts at the same ticks, and a resumed run equals a straight run.

Siblings and eqv partners

• Same table (canon): 299 (TM13 from B, mirrored) and 602 (TM13 from C, mirrored). TM13 from A is solved upstream (halts).
• eqv-1590 group of 412: also 1RB0LE_1RC1RB_1LD0RA_1LF1LC_0LC---_1RB0LA (= TM13 from E), not on the 740 list.
• Cousins (TM7's table, through eqv members): 338 (eqv member = TM7 from B), 577 (TM7 from D, and from F), 730 (TM7 from C). Not run here.

Next

Most valuable 2 h stage: an exact level accelerator for the late phase. From the checkpoints (work/ckpt_TM13_D.pkl at 16,551,000 ticks, work/ckpt_TM13_B.pkl at 7,627,000; resume with work/cbsim_fast2.py --resume), fit the map that consumes one PL(n)^k_n level (new counts of the remaining levels and of the right part as functions of k_n and the separators), validate it against the port over the next few levels, then iterate it to the bottom of the stack (~80 levels) and see what happens there (halt window, or a new epoch). - Stop rule: if the per-level map branches on k mod 5 (or another residue) with no closed form, apply the cryptid protocol for the whole cluster (412, 602, 299): formalize, flag, stop. - A predicted halt deep in the stack would still need a certificate Coq can check: CBSim's check_spec at ~10^8 ticks is likely too slow, so it would need the level map proved as a macro. - Cheap alternative: run the TM7 cousins (338, 577, 730 through their eqv members) with the port to 10^7 ticks each.