1RB0RA_0RC0LE_1LD1RF_1LB1RD_1LD1LE_---1RA

Label: H-3 (halting hunt). 740 list line 244. Class: Counter Class 3.

Family, checked here by exhaustive renaming and mirroring against CounterClass3v1 TM4 (1LB1LA_1LC1RB_0RD0LA_1LA1RE_---1RF_1RC0RF). In TM4's labels the three tables differ from TM4 only in D0:

216 and 701 are one table from two starts. In 244's own labels the differing transition is C0. All three are claimed by claude in coord/claims.tsv (2026-10-13).

Halting hunt: exact model (2026-10-13)

Result: no halt to the horizon for all three machines (numbers in the results table below). The exact model reached these epochs:

• 244: epoch 108. The counter block is b = 7.3e35, and the TM step count is about 10^(2.2e35) when the run stops on the model's 2^120 count limit.
• 216: epoch 97 (b = 1.2e32).
• 701: epoch 96 (b = 6.0e31).

The earlier cc3acc runs reached about epoch 11.

Two findings change the H-3 brief:

• The differing transition is not startup-only. It fires again at every right-end event. Example: 244 fires C0 at step 402,723,884. This was checked with tools/sim.py (C engine) on the original holdout string, against the model's configuration cell for cell. By epoch 59, 244 has fired it 116,088 times. The brief's "fires 4 to 6 times, all before step 787,288" covered only the first 0.8 M steps. So these machines do not run TM4's table. Their own D0 drives the right end of the tape.
• Real step counts are doubly exponential. The upstream P0_n step (its Rocq proof uses the induction hypothesis twice) costs exactly 24*2^n - 6n - 24 TM steps. The cc3acc runs at 5.9e8 to 6.9e8 msteps were therefore already at roughly 10^1600 to 10^3200 TM steps (epochs 10 to 11). TM4's own certified halt comes out of the model at 1012 macro moves, with an exact step count of about 1.341e395 (a 396-digit integer). The plain and batched models agree on it exactly.

The model (scripts/rle.py, scripts/rle2.py)

Everything is in TM4's labels with the machine's own D0. The tape is run-length encoded with exact Python integers.

Plain model (rle.py). It uses three kinds of move:

• Chain moves for the self-loops A1 (1LA), B1 (1RB) and F1 (0RF). Each crosses a whole run in one move, with exact step counts.
• The upstream accelerator P0_n, proved in CounterClass3v1. It holds for our tables too, with the same step counts as TM4 on every check, so D0 plays no part in it:

l 0^(2n) <B 1^2 0 1^n r --> l <B 1^(2n+2) 0 1^n r 24*2^n - 6n - 24 steps

• Single TM steps otherwise. Every D0 firing is counted.

Batched model (rle2.py). It adds a word run U = (0 1^2), kept only in the left stack, and three batch rules. Each rule is a closed form of an iterated macro step that was derived from the table:

W  (wave, k >= 1, any L, R' starting with 0 or blank)
   L 0^2 <B 1^(2k+2) 0 1^k R'  -->  L U^k 0^2 <B 1^2 0 R'
   one iteration: L 0^2 <B 1^(2j+2) 0 1^j R' --> L U 0^2 <B 1^(2j) 0 1^(j-1) R'
   steps 24(2^k - 1) - 2k(k+1) - 9k

A  (absorption, x >= 1, c >= 1, any L, R'')
   L U^u <A:0 1^x 0 1^c R''  -->  L <A:0 1^(x+2u) 0 1^(c+u) R''
   steps 2ux + 2u(u-1) + 7u

P  (passes, g >= 3 zeros ending at the head, j <= b-1, any X, R)
   X 0^g <A:0 1^(2j+1) 0 1^b R  -->  X 0^(g-2p) <A:0 1^(2j+2p+1) 0 1^b R,
   with p = min(b - j, (g-1)//2) and g = infinity at the left end
   steps 24(2^(j+p) - 2^j) - 6p

Above 4000 bits, step counts are kept as log2 (steps_str prints ~10^x). Everything else stays exact.

Epoch structure. An epoch starts at 0^inf <A 1 0 1^b 0 1^c ... (the driver logs each one). It runs in four phases:

1. Passes grow the left block to 2b+1.
2. A wave turns b into U^b.
3. The same pass/wave machinery recurses into c, d, ..., down to the right end, where D0 fires.
4. Absorption folds the units back in. The next epoch starts with b' = 2b + 5 + (units made deeper down).

b roughly doubles per epoch.

Validation

• Rules on constructed tapes (scripts/validate.py): 1848 of 1848 pass. The checks cover P0_n (n <= 14), W (k <= 14), A (u <= 8, x <= 11, c <= 4) and P (j <= 9, all g up to the limit), on the 244, 216/701 and TM4 tables, with random contexts. Each check confirms the exact target configuration, the exact predicted step count, and that no cell outside the rule's window is read.
• Larger parameters: a further 174 of 174 checks pass, covering W (k <= 18), A (u <= 30, x <= 40, c <= 17) and P (j <= 14, b <= j+9, g <= 30). The largest is a 200,933,322-step pass batch.
• Direct simulation of the original holdout strings (scripts/anchors.py, tools/sim.py C engine): 14 of 14 anchors match on state, head and the whole tape.
• 244: epoch 2 (72,175 steps), the 5th C0 firing (402,723,884) and epoch 3 (805,378,447).
• 216: epoch 3 (2,360,753).
• 701: epoch 3 (197,316), the 5th D0 firing (98,621), the 7th D0 firing (6,442,646,598) and epoch 4 (57,982,256,712).
• Step-targeted anchors use P0_n applied partially (P0_n' for n' < n is the same lemma) to land on a chosen step: 216 at 29,999,998, 244 at 150,000,000, and the deep anchors 216 at 149,999,999,999, 701 at 150,000,000,000 and 244 at 149,999,999,994 (work/anchors_deep.out). The deep ones sit mid-epoch: inside epoch 3 for 216 and 244, and inside epoch 4 for 701.
• scripts/cmpdirect.py also matched every macro move of 244 up to step 2.0e8.
• Plain against batched model (scripts/cmp12.py): full tape, state, step string and D0 count are identical at every epoch start up to epoch 19 for all three machines, and up to epoch 21 for 244 (work/cmp12_*.out). At epoch 21 that is 656 M plain moves against 16,643 batched moves.
• Batched model with and without rule P (driver2 against driver3): b, tail, D0 count, block lists and step string are equal at all 64 common epochs of each machine.
• C port against Python (rle2c against driver3): msteps (exactly), b, tail, D0 count, nblocks and census are equal at all 64 common epochs of each machine. The C port also reproduces TM4's halt (1012 msteps, log10 steps 395.127).
• Against the cc3acc runs: the epoch-start block lists equal the cc3acc-style run (port of hints/cc3acc.py) for 244 epochs 1 to 9. They also agree with hints/trace244.txt and hints/trace216.txt (e.g. [10679, 6490, 993, 164, 23, 12] and [7427, 4001, 1279, 745, 151, 77, 35, 20]).
• TM4 reproduced: TM4 halts in the model at U^15 0 <B 1^2 0^2 1 -> E0, after 1012 macro moves. That is the halt certified in CounterClass3v1.

How these machines would halt

The only halting transition is E0. E is entered only by D1, and D only by C0.

Halting needs exactly this: a wave has just consumed a block, and the next block has length 1:

<B 1^2 0^2 1^L 0   (just after W)   halts  iff  L = 1     (F0, C0, D1, E0)

TM4 halts this way, with tail [.., 16, 1].

This pattern catches every possible halt. C is entered by B0 (1LC) or F0 (1RC), and a B0 entry cannot reach E0:

• B is entered by A0 or D0 (244). Either way B's right neighbour holds a 1, so the path runs C0, D1, then E1.
• B is also entered by B1, but then B's left neighbour is 1, so C1 fires.

So every E0 comes from F> 0 0 1 0. The F0 steps inside batch rules cannot halt, because each rule reaches its target configuration (derived, and checked on constructed tapes). Every other F0 is a single step at a macro boundary, and the census checks those. So the census misses no halt.

The census of L over the whole run:

These counts cover the whole C run. The Python census (driver3.py) agrees on the 64 epochs they share.

L = 1 never occurs.

Small counter blocks are made at the right end, where the right-end routines re-seed the last blocks. Right-end events have two forms:

(i)  U^k 0 1^2 0 1 0 <D:0          (a wave ate the last block)
(ii) 1^2 0 1 0 1^2 0^g 1 0 <D:0    (F erased a last block of length g+2)

Each routine is linear in k or g (scripts/endroutine*.py, k <= 24, g <= 39). Only two parameter values create a 1-block:

• 244: only routine (ii) with g = 4. In a constructed context it halts 163 moves later (U^13 0 1^2 0 1 0 1 E0).
• 216/701: only routine (i) with k = 0.

These two values really are the halting doors. Injecting them into real right-end configurations of the run, then continuing the exact model to the next epoch start, gives:

Over 30,000 right-end events (scripts/endseq.py, with bigrams) the event sequence follows a rigid grammar, for example:

k1 -> g1 | k2 | big
k2 -> g2
g1 -> k9 | k10 | g8 | big
gX -> k1   (244)

• 244 (30,000 events, about 50 epochs; the whole C run agrees, see Results) has small g only in {1, 2, 8, 9, 10, ...}. g = 3 to 7 never occur.
• 216/701 (20,000 events each) have k in {3, 4, 16, 18, 19, ...}. k = 0 never occurs (k = 3 only at startup).

The successor values are structural, not free:

• After a g1 event the next k is u + 5 (4,985 of 5,078 cases, u + 4 in 72), where u is the number of units next to the end. u is 4, 5 or at least 10 at every g1 event seen, so k = 4 does not follow g1.

• A g after g1 occurs only when the gap to the 1 0 1^2 marker is 4 or 5 (the observed values are g8, g61, g363 and g364).

• 244's nearest door is k2 -> k3. On constructed k2 contexts ... 1^2 0^G U^2 0 1^2 0 1 0 <D:0 (scripts/k2test.py, M < 70, G < 60), the next event is k3 or k4 when the gap G is small: k3 needs G <= 16, mostly even G; k4 needs G = 1. Otherwise the next event is g2. Through epoch 52 the run's k2 events (1,888 of them, scripts/k2gaps.py) all have G >= 18. The observed values are 18, 19, 22, 23, 26, 27, 31, 62, 63, ... So the closest the run comes to the halting door is G = 18 against a needed G <= 16.

• 216/701's right end is even more rigid. Over the whole C run (work/c_run/bigrams_216.txt, bigrams_701.txt), after startup the only small events are k4 (repeated) and g3:

o -> k4 -> k4* -> g3 -> o o -> k>15 -> ... -> g>15 -> o

701's startup alone shows k3, g2 and g6, once each. A nonhalting proof for 216/701 looks tractable along this line: the right end re-seeds from a fixed small seed (k = 4) or from big values only.

So the right end lives on a structured set that avoids the one halting value. Whether that holds forever is open. It is the natural nonhalting route, and the side upstream works on (CounterClass3v2).

Assessment

• Outcome: no_halt_to_horizon for 244, 216 and 701. The exit rule of the brief (last tail block invariant) does not literally hold: the last block cycles through {3, 12, 11, 2, ...} for 244. The stronger statement above holds instead: the right end never reaches the one halting configuration.
• Not flagged as cryptid. The rules are exact linear maps with min/compare branches, and the irregularity comes from nested counter comparisons. No modular (Collatz-type) step was seen. The end-event grammar looks finite at small values.
• Certification route if a halt ever appears. The CounterClass3v1 msteps module runs our TM string unchanged, since P0_n holds for our tables and D0 is an ordinary transition. It is cheap only while the halt is within about 1e9 cc3acc msteps, roughly epoch 12. Beyond that, the W, A and P batch rules need Rocq lemmas. All three are simple inductions (W and P iterate P0, A is a chain).
• Cost of going deeper. The batched model costs about 1.15x more moves per epoch, and 70% of the moves are right-end excursions (R depth <= 7).
• scripts/rle2c.c is a C port with the same move semantics and exact __int128 counts (TM steps as log2). It equals the Python census run on msteps, b, tail, D0 count, nblocks and census at all 64 common epochs of each machine. It runs about 60x faster.
• The port also logs, per epoch, the right-end event histograms (g_hist, k_hist) and 244's k2 gap minimum. It writes the bigram table to work/c_run/bigrams_<line>.txt. Its histograms equal endseq.py at epoch 50 (e.g. g1 4952, g2 1459, g8 6), and its k2 count equals k2gaps.py at epoch 52 (1,888 events, minimum G 18).
• The port stops itself when a count passes 2^120, about epoch 110. Going further needs a bignum port (no GMP on this box) or memoising right-end excursions.

Results (C run work/c_run/, 2026-10-13)

Right-end statistics over the whole run (work/c_run/bigrams_<line>.txt and the g_hist/k_hist fields):

• 244: small g only in {1, 2, 8, 9, 10, 11, 12}; small k only in {0, 1, 2, 9, 10, 11, 12} (k0 once, at startup). k2 events: 20,457,604, minimum gap G = 18, none with G <= 17.
• 216: small g only in {3}; small k only in {3, 4}; k = 0 never.
• 701: small g only in {2, 3, 6}; small k only in {3, 4}; k = 0 never.

Notes on the run:

• 244 stopped itself on the 2^120 count limit at epoch 108, after 31,069,556,794 macro moves.
• 216 and 701 were stopped by hand at epochs 97 and 96, to free a slot for the deep anchors.
• Each epoch costs about 1.15x the previous one, and the expensive epochs alternate with near-empty ones.
• Python runs: work/rle2_run/ reached epoch 66 to 68, and work/rle3_run/ (census) reached 64.

Scripts and logs

All in scripts/:

• rle.py: plain model.
• rle2.py: batched model.
• validate.py: rule checks.
• anchors.py and cmpdirect.py: direct-simulation anchors.
• cmp12.py: plain vs batched.
• driver.py, driver2.py and driver3.py (census): run drivers.
• nearmiss.py, d0classes.py, endseq.py, endctx.py, endev.py and endroutine*.py: right-end analysis.
• g4test.py, k0test.py, k2test.py and k2gaps.py: halting-door experiments.
• rle2c.c (binary rle2c): C port of the batched model and census. summarize.py summarizes its logs.
• explore*.py: tracing. prof*.py, run2.py, d0check.py, firstd0.py and fitp0.py are the profiling and fitting scratch behind the statements above.

The long run's logs are in work/c_run/ (epochs_<line>.jsonl). Logs of the Python runs are in work/rle2_run/ and work/rle3_run/ (epochs_<line>.jsonl, one line per epoch; checkpoint ckpt.pkl). work/anchors_long*.out and work/cmp12_*.out hold the anchor and comparison outputs. work/rle_run/ is the first plain-model run, stopped at epoch 15/16 because it was superseded.