1RB0LF_1RC0LB_1RD1RB_1RE1RF_1LA---_0RC1LA

Status: STUCK (parked after the funded inv_search stage, 2026-10-11; confidence med: the mechanism is exact, but no inductive invariant exists among product n-gram languages with short windows, see the Funded stage section) Label: W4-5 (740 list line 469; 778 list line 499) Class guess (agent / Dennis): two-zone block/pair shuffler (a chaotic two-stack list machine), not a counter / - Spreadsheet notes / Discord thread: Results row has class "Counter Class 2" and no status, notes, sources or "done by". Direct Simulation tab: not simulated to 1e14 or 1e15. No hit in data/discord/*.txt. Upstream (busycoq BB6 HEAD 9cf9e88) only has the Eqv_v3 TM540 equivalence (E0 = 1LD variant <-> this machine) and Eqv_v2 TM359 (that variant <-> 1RB1RF_1RC1RD_1LB---_0RA1LE_1RF0LD_1RA0LF). Neither is a nonhalt proof. Viewer: https://bbchallenge.org/1RB0LF_1RC0LB_1RD1RB_1RE1RF_1LA---_0RC1LA

Family (canon up to renaming + mirror, all 6 start states)

The macro model below also predicts every E-event of the start-D run (holdout 599) and of the B/C/E/F starts: 1,032,103 / 1,033,544 / 1,034,114 events to 3e7 steps each, 0 mismatches (scripts/macro.py check N start).

Observation

• No halt to 1e11 steps (tmsim; span 779, lo -77, hi 701, 349 nonzeros at 1e11). The 1e12 run was still going at write-up. qsim (Quick_Sim, block size 2) reaches only 1.04e8 steps in 700 s and proves 0 rules (36,378 failed proofs), so accelerated simulation does not help here.
• Growth: 462 cells at 1e9, 779 at 1e11. The time between right records grows like span^4.4 (and the exponent creeps up). The right edge grows 4 cells per right record, the left edge 1 cell per left record.
• Two zones split at the head. Left of the head, the tape is 1-blocks separated by single 0s ("block form"). Right of the head it is (10)-pairs separated by zero runs, plus an occasional lone 1 ("pair form"). A leftward A/F sweep (A1 = 0LF, F1 = 1LA) turns the block next to the head into pairs. A rightward B/C pass (C1 = 1RB, B0 = 1RC) turns pairs back into a block. So the head always sits at the interface (scripts/turns2.py prints this at every turn).
• Only 5 kinds of turn occur: E0L, A0R, B1L, B0R, F0R (31,298 turns to 3e5).
• At right records the whole tape is in block form: 46 blocks at 1.76e9, with lengths 2, 6, 10, ... (mostly 2 mod 4, sometimes 0 mod 4). Between right records the block list is reshuffled completely (img/records_2e9.png). This is not the fixed skeleton of CounterClass2v1.

Candidate rules (macro model, scripts/macro.py)

E-event K(L; a; r; R) := 0^inf 1^b1 0 ... 0 1^bp 0 1^a E> 0^r R 0^inf, with E reading the first 0 of 0^r. L = closed blocks b1..bp, a = the block next to the head, r = the zero run (inf when the run reaches the blank), and R = the pair-form tokens P^j = (10)^j, Z^n = 0^n, D = a lone 1 that is followed by a pair. In each rule, y and b are the last two closed blocks, and a missing block counts as 0 (left edge).

Validation: - Random instances (scripts/validate.py; the TM is run from the constructed tape to the next E-event): - INV-shaped: 6,000/6,000 (seed 11): Ee 2,611, Ee left edge 525, Eo->C4 521, Eo->C3 n=3 468, Eo->C3 n>=5 1,437, Eo->right edge 438. - Wild (odd blocks, even runs): 6,000/6,000 (seed 12), including 313/313 halts and 603 even-run cases. - Step formulas: 3,000/3,000 (scripts/stepfit.py). - Real run: every E-event from blank matches the model, 34,479,962/34,479,962 to 1e9 (start A; scripts/macro_check_1e9_startA.txt): Ee 17,239,831, Eo->C3 17,239,713, Eo->C4 298, right edge 118, left edge 1.

Halting. E1 is the only undefined transition, and E is entered only by D0. Going through the rules, E can read a 1 only in H: a right pass that meets exactly 0^2 after a pair. So the machine halts iff some C-pass meets Z^2.

Parity. At all 1,722,791 E-events to 5e7 (scripts/ctx.py), and at all 103,296 to 3e6 (scripts/inv.py --real): - every closed block is even; - r is odd or inf; - every zero run Z in R is odd (1, 3, 5, ...); - D always sits between two pair groups. Each rule keeps these parities (b+1, x+1, n-2, r-2 are odd when b, x are even and n, r are odd). This holds only while three side conditions hold: - (I2) a = 2 only with r = inf; - (I6) a pair group just before a zero run has j >= 2; - (I7) the group after a D has j >= 2 unless it is the last token. The danger is drop_pair on a P1 before a Z, which merges a Z into r and makes it even.

Open. The side conditions hold on the real run, but they are not inductive. In the random closure test (scripts/inv.py), about 2% of steps from INV states leave INV, all through r = 1 events (D creation). The natural strengthening (r = 1 implies the next group has j >= 3) already fails on the real run at step 2,403,364. So the non-halting argument needs a finer context invariant, possibly a regular language over abstract tokens.

Template comparison

CounterClass2v1..v4 (upstream verify/, BB6 HEAD) all differ from this table in exactly one slot, our A0 (v1: 1LC in our names, v2-v4: 0LB; v4 also has E0 = 1LD). They start in our D (v1, v4), E (v2) or C (v3). - A0 is the turn that starts rule Ee. In the templates, A turns left there and continues; here A0 = 1RB makes B erase the next two closed blocks. - v1's rule set is a deterministic counter on a fixed skeleton: SkelE n = 1^2 (0 1^(6+4k) 0 1^(6+4k))_k, with Bnext on (n, j, b), ClosedCall side lemmas and GoodB. Ours has no fixed skeleton: the block list is a stack that rules Ee/C2/C4 push and pop, with chaotic contents. - So the template applies only in its top-level shape (progress_nonhalt_cond with an invariant on a symbolic config type). The Eqv_v3 TM540 / Eqv_v2 TM359 equivalences link this machine to two other unproved tables, so they give no proof either.

Cryptid check (ground rule 6)

Not cryptid-like in the sense of rule 6: there is no pseudo-random arithmetic. The macro rules only add and subtract (y+3, b+1, x+2, n-2), and halting needs a parity defect (an even zero run) that every rule avoids while the local context conditions hold. The unpredictability is combinatorial (a shuffled two-stack list), as in the chaotic classes, so the realistic proof is an invariant (closed language), not a counter formula.

Checkpoint A (Dennis)

(pending)

Informal proof

Not started (waits on the invariant; see decision.json).

Formalization log

-

Outcome

Parked (STUCK) after the funded inv_search stage: no invariant, and a precise obstruction (see Funded stage). Earlier CTL probe: 85 small RWL_mod / NG settings of the extracted CTL62 decider (scripts/ctl/sweep1.jsonl) all returned false, plus 2 resource failures.

Decision (2026-10-11)

Question: W4-5 (469) and its same-table sibling 599 have an exact macro model where halting needs one parity defect: fund one ~2 h stage to search for an inductive context invariant, or park both? Answer: inv_search (Fund one ~2 h invariant-search stage for 469 + 599). Dennis: go with recommendations (2026-10-11).

Funded stage (2026-10-10, inv_search)

Funded 2026-10-11 (Dennis: go with recommendations). Goal: an inductive invariant over the validated macro model, or a precise obstruction, then park. Result: no invariant; a precise obstruction for every left/right-product n-gram invariant with short left windows, plus evidence that the missing invariant is not local. Parked (STUCK). Covers 469 (start A) and 599 (start D): every run below uses both starts.

What was built (all stdlib, in scripts/; outputs in scripts/absint_runs/): - absint2.py: n-gram CPS at the macro level. Abstract state = head (a, r or the C-pass x) + the first K symbols of each stack (closed blocks; tokens P/Z/D). Integers are exact below T, else n mod M, with separate (T, M) for head values, pair counts, zero runs and blocks. Every rule of macro.step / macro.cpass is replayed on all abstract branches; the worklist re-wakes states when a new (K+1)-gram appears. - absint3.py: the same with R read as groups (j, separator), so one window slot holds about two tokens. - absint4.py: absint3 plus one parity bit per stack for the part beyond the window (weights of GP below). Revealing the bottom marker needs bit 0, so a spliced tail must keep GP. This is a sound refinement. - splice.py: the obstruction test. Take two sampled E-events of the real run that share a window of W consecutive entries (exact values, or matched under an abstraction). Keep the first's head, the first's top p+W entries (1 <= p <= 2) and the second's rest. The spliced configuration has the first's head and first window, and every (W+1)-window in it occurs in a reachable configuration. So every product n-gram invariant with windows of at most W entries contains it, whatever the value abstraction and whatever the other stack does. Then run the macro model up to 10,000 macro steps. verify_splice.py re-runs every halting splice on the TM itself (C engine, from the constructed tape). - gpar.py: the global parity GP (below), checked on the real run, rule by rule, and on the splices.

Results 1. Closures: every setting fails. absint2: 115 settings (KL 2-4, KR 3-7, P (3,2)/(4,4), Z (4,4)/(6,4), B (6,4)/(10,4)), all FAIL: 58 reach HALT, 48 Z1-not-followed-by-P, 9 D-not-followed-by-P (sweep_tokens_absint2.jsonl). absint4: 58 of 128 settings run (KL 2-8, KR 2-3), 56 FAIL and 2 LIMIT at 3e6 states (KL 6-8 with B (12,4): 13-27k left grams). absint3 spot runs fail the same way. Every failing trace passes through a pattern that never occurs on the real run (a zero run before a D, a leading (0, D) group, D P1 Z, P1 before a zero run). 2. Splices of the closed-block stack halt; splices of the right side do not. - Left stack, exact windows (seeds 2, 4, 7; 590-3,993 samples): halts at every W from 1 to 4. W=1: 7 halts (plus 2 unruled) in ~600 splices; W=2: 5 (+4); W=3: 7 (+2); W=4: 3 (+2). W=5..9: 0 halts in 1,264 splices (1 unruled at W=6). - All 16 saved halting splices (seeds 4 and 7) were re-run on the TM from the constructed tape: 16/16 halt (E reads 1) at steps 2,595 to 272,326 (verify_splice_L_s4.txt, _s7.txt). Fig 6 shows the shortest one. Over all four splice runs, 45/45 saved halting splices halt on the TM. - Right side (groups), exact windows: 0 halts in 560 splices for W=1..6 (splice_R_s1.txt). The cut is within reach: from sampled times the head touches nearly every original R group within 4,000 macro steps. - Left stack matched under a coarser block alphabet (exact below 8, else mod 4; seed 11): halts at W = 1, 2, 4, 5, 6 and 7 (6, 4, 0, 2, 1, 2 and 2 in about 250 splices each). 17/17 halt on the TM (verify_splice_Labs84_s11.txt). - Both stacks spliced at once (two donors, exact windows; seed 12): halts at W = 1..5 (3, 5, 1, 2 and 1 in about 250 each), none at W = 6-7 (424 splices, 1 unruled). 12/12 halt on the TM (verify_splice_LR_s12.txt). - Consequence. No invariant that is a product of n-gram languages over the two stacks exists in these cases: - left windows of at most 4 exact blocks, with any value abstraction and any right side; - both windows of at most 5, exact; - left windows of up to 7 blocks once blocks are read as "exact below 8, else mod 4". The closures above are all of that kind, so their failure is not a tuning problem. Only near-exact windows of at least 6 entries on both sides remain possible. In Python that is far beyond reach (3e6 states already at KL 6-8 with KR 2). 3. The defect is not local. In the 9 seed-4 halting splices, the head reaches the spliced part within 1-105 macro steps. The first local INV violation (always I6, P1 before a zero run, made by C4 on "D P2 Z") comes 47-6,628 macro steps later, and the halt 100-9,337 macro steps later. In between, every rule application keeps parity and I1-I7. 4. A global parity GP. A GF(2) nullspace search over 20 count features of the real run gives one non-trivial relation: GP = [r = 1 mod 4] + [floor(a/2) odd] + #(groups with odd j) + #(zero runs = 3 mod 4) + #(blocks = 0 mod 4) + #blocks = 0 (mod 2). - It holds at every E-event of the real run (gpar.py real: GP = 0 at 3,000,000/3,000,000 E-events for start A and for start D, absint_runs/gpar_real_3e6.txt). - Rule by rule on 20,000 random parity-correct instances it is kept, except C4 on a final "D P1" (R empties) with x = 0 mod 4: 44 of 1,663 Eo|D cases. - 24 of the 45 halting splices break GP (exact L 9/16, joint 8/12, coarse L 7/17). The other 21 satisfy GP. The 7 checked GP-respecting splices of seeds 4/7 also satisfy all 14 relations of a 56-feature GF(2) search. So parity bookkeeping alone does not explain them. 5. TM-level CTL, wider sweep (scripts/ctl/sweep2.jsonl): 191 more RWL_mod settings (block size 1/2/4, mnc 2-5, mod 2/4, len1 4/6/8, len2 0-3) and 24 NG-with-history settings (n 6-16, len 0-4). All false (5 timeouts at 60 s). Together with sweep1: 300 settings, none true. 6. Structure seen along the way, all on the real run: the total number of blocks + groups is nearly conserved; it grows slowly, 15-28 over 3e5 macro steps. Left-edge Ee events are rare: start A has 38 in 2e6 macro steps, 35 of them with L = [2], a = 6, r = 3.

Still open - The missing invariant couples the whole block stack with the right side. GP is one part of it; the 21 GP-respecting halting splices show there is more. Where those defects come from is not known. - An n-gram invariant with near-exact windows of at least 6 entries on both sides is not ruled out: no halting splice turned up there (exact L W 5-9: 0/1,264; joint W 6-7: 0/424). Testing it would take a compiled closure with exact blocks and about 10^7-10^8 states. That is a long shot, given that the halts come from a non-local mechanism. - Resume condition: a method with coupled left/right automata (MITM-DFA-style triples), or a non-regular invariant, or the compiled closure above.