1RB0RF_1RC1LB_1LD1RE_1LB0LD_1RF0RC_1RA---

Status: CRYPTID_CANDIDATE (observe, 2026-10-13; label W5-2; 740 line 409, 778 line 436) Class guess (agent / Dennis): Shift-overflow counter with SOC_2_5_v1.v TM10's macro rules. Halting hinges on the binary digits of a counter value, so it is cryptid-like. / (pending) Spreadsheet notes / Discord thread: sheet results row 438 "Shift-overflow counter", with no status and no "done by". No mention in data/discord/*.txt. Viewer: https://bbchallenge.org/1RB0RF_1RC1LB_1LD1RE_1LB0LD_1RF0RC_1RA---

Summary

The scout's premise was a near-port: this is TM10 with A1 changed, and A1 is used only at step 10.

That premise is wrong in one important way. ROv3_0/ROv3_1 are false for this machine, not merely unproved. TM10's invariant P contains halting configurations: cfgL(8,0,17) satisfies P and halts at step 10,189,718.

From blank, the run stays inside TM10's "normal cycle" for as long as one digit condition holds. The condition is that the counter value x has a 1-bit at an even position. Whether that holds forever is a question about the binary digits of an exponentially growing orbit. That is ground rule 6, so the machine is flagged CRYPTID_CANDIDATE with a priority call.

Observation

Simulation: - Direct simulation to 1e10 steps: no halt, span 218 cells. - With A1 replaced by a halt, starting from step 11: no halt to 3e10. So A reads 1 only at step 10. - qsim (Quick_Sim) proves no rules here; it gives 7.3e6 steps in 2e6 loops (data/qsim.jsonl). - Record-aligned compress track finds 81 skeletons with no clean exponent trends (data/compress_track.txt). The natural coordinates are TM10's counters below.

Notation

This is TM10's notation (busycoq BinaryCounter_v2), written as tape words.

The cycle from blank

The run reaches cfgL(3,6,1) at step 35. After that, every cycle between left overflows looks the same.

1. cfgL(L,0,2x+1), then LOv. Here n = 2x+1 is odd, so i = 0 and the run goes to R1(L, 2^L-1, 0, 0, x).
2. RC1_Ov_0 with lenR = 0, giving R4(L+1, 2^(L+1)-2, i1, 2^(i1+1)-2, x1), where x = (2x1+1) 2^i1.
3. A chain of RC4_Ov_1 steps runs while the current gap i is odd. Each step consumes the next 1-bit of x.
4. RC4_Ov_0 at the first even gap i = 2q gives R(L', K, 2m+1).
5. RInc and the LC/RC run lead to the next cfgL(L', 0, 2x'+1).

The new value is

x' = (2 k_c + 1) 2^(5q) + m

where m is x with the consumed bits shifted out, and k_c is the left counter after the chain. N stays odd, so the corner case (n = 2^L) and R1 with lenR > 0 never occur.

The chain stops at the first 1-bit of x at an even position. It empties (RC4_Ov_1_0) iff every 1-bit of x is at an odd position.

The closed form is F in scripts/Fmap.py. It reproduces the macro-rule simulator (scripts/absm.py) on 783 consecutive cycles.

Orbit facts (scripts/Fmap.py, scripts/chains.py logic)

• 20,000 cycles computed, with L up to 172,193 (TM steps roughly 2^172000). The chain never empties.
• E = number of 1-bits of x at even positions:

• Chain lengths: 13,650 × 0, 4,120 × 1, 1,588 × 2, 440 × 3, 150 × 4, 38 × 5, 9 × 6, 4 × 7, and a single 28 (cycle 14,614).
• Stop values: q = 0 in 72% of cycles, q = 1 in 20%.
• New 1-bits enter at the top of x. For a chain of length 0, the gap between the new top bit and the previous one is 7q+4: even when q is even, odd when q is odd.
• Older bits move down and are consumed by later chains. A run of q = 0 cycles leaves a run of same-parity bits, and a later cycle eats that run in one long chain (the 28).
• So x is a queue that feeds on itself: what is appended depends on what is read at the bottom.
• The bottom bits are mixed by the - (2^(i+2)-1) 2^(5q) borrow each cycle. They look random (Fig 2).

Heuristic (cryptid protocol)

If x's 1-bits were independent fair coins for parity, the chance that cycle t empties the chain would be 2^-(1-bits of x_t). That is at most 2^-17 from cycle 4 on, and it falls exponentially, since the number of 1-bits grows linearly. Cycles 1..20,000 are checked exactly.

So it is "probviously" non-halting. But non-halting is equivalent to a statement about the digits of an explicit arithmetic orbit, of the AntiHydra kind. No invariant was found: - E has no monotone bound. - The highest even-position 1-bit sits up to 19 bits below the top. - Gap parity is fed back from the pseudo-random bottom bits.

TM10's own orbit

From cfgL(5,19,1), TM10's chain empties once, at L = 11 (RC4_Ov_1_0). The continuation then has an even gap and returns to normal cycles, so it never reaches R3. TM10's proof does not care, because its ROv3 lemmas hold. The two orbits never merge.

Candidate rules

All of these are validated on the real TM by direct simulation from rendered configurations (scripts/validate.py, val_m0 run, scripts/valF.py). The parameters are random and satisfy TM10's P.

The RC3 overflow is where this machine differs from TM10: - lenR even, m odd: always halts (16/16), after 30(r+1) steps. - Other RC3 cases: some halt, the rest never reach TM10's result within 2e5 steps.

The cycle map F is checked on the real TM at the left record after the next LOv, which is 0^inf <B 1^(2L'+3) RC(2x'+1). 50/50 instances passed (chain length 0: 28, 1: 19, 2: 3; L' up to 21; data/valF*_partial.out).

The first three left records from blank match F exactly:

Exhaustion runs (x with all 1-bits at odd positions, built as cfgL(L,0,2x+1)) behave as follows: - cfgL(8,0,17) halts at step 10,189,718. - cfgL(5,0,17) halts at step 1,014,696. - The other 23 tried show no halt in 3e9 steps (their next cycles are exponentially long), so "may halt".

Template check

The template is SOC_2_5_v1.v Module TM10 (1RB0LB_..., line 5186 at upstream HEAD), which differs only in A1 (0LB there, 0RF here).

• The scout compiled TM10's module with this string and init cfgL(3,6,1). Everything except ROv3_0/ROv3_1 compiles.
• Iter.v admits those two lemmas and then "proves" nonhalt. That proof is unsound for this machine: from l 10 C> (10000)^(2n) 1 00 10000 r, A reads the 1 and moves right into r.
• TM10's P is not an invariant here, because cfgL(8,0,17) satisfies P and halts.

Other A1 variants of the table proved upstream are TM8/9/10/11/12/14/15/18/19, with A1 ∈ {1RD, 1LB, 0LB, 1LE, 0RE, 1LA, 0LE, 1LC, 0RC}. None has 0RF, and no upstream file or PR proves this table from any start.

Siblings

None. Starts B..F (canon) are not on the 740 or 778 lists, and the machine is a singleton group in the 1590 equivalence file.

Checkpoint A (Dennis)

Pending. There is a priority call in status.json: park it, or fund one stage for the Rocq reduction and an invariant search.

Informal proof

None: no non-halting argument is known. If the stage is funded, the formal reduction would take TM10's module with ROv3 removed. It would replace P by P plus "the current cycle's x is F^t(x0) and F^t(x0) is not in S for all t", and prove (forall t, F^t(3,3) not in S) -> ~halts tm c0, AntiHydra-style.

Formalization log

• Scout probe (scratchpad w5t/p409): Probe409.v fails at ROv3_0 (incomplete proof). Iter.v, with the two lemmas admitted, compiles. There has been no Rocq work in this stage.

Outcome

CRYPTID_CANDIDATE (2026-10-13), waiting on Dennis's priority call.

Files: - scripts/: tm.py (mini simulator), render.py (TM10 configs to tapes), absm.py (TM10 macro map), Fmap.py (cycle map F), chains.py (chain statistics), validate.py, val_m0.py, valF.py and valFc.py (rule checks), xbits_png.py (Fig 2). - data/: r3_overflow_config.txt (Fig 3 start), qsim.jsonl, compress_track.txt.