1RB0RA_1RC1RF_1LD0LC_1RA1LE_1RA0LC_---0RD: never halts (CONDITIONAL, three flagged lemmas)

• Machine: 1RB0RA_1RC1RF_1LD0LC_1RA1LE_1RA0LC_---0RD, viewer https://bbchallenge.org/1RB0RA_1RC1RF_1LD0LC_1RA1LE_1RA0LC_---0RD
• Sheet: results row 106, Unknown, no notes. Not claimed on Discord. One transition from SBCv8.v TM31 (F1 0RD vs 0RE).
• Status: this is not a proof yet. Sections 2 to 6 reduce non-halting to three lemmas, F1, F2 and F3 (stated in sections 3 and 5, listed in section 8). They are validated by simulation, not derived. Every other rule is an exact per-visit rule, checked on random instances (no symbolic proof yet; Rocq is the correctness check).
• Checks: python3 -B check_proof.py (pure Python, about 6 min; --quick about 2.5 min; last run: ALL PASS, data/proof/check_proof_long_seed1.txt). --long also reruns the C trackers from the blank tape (1.3e10 steps, about 1 min) and compares them with the stored files. Logs: data/proof/check_proof_*.txt.

Transitions: A0=1RB A1=0RA, B0=1RC B1=1RF, C0=1LD C1=0LC, D0=1RA D1=1LE, E0=1RA E1=0LC, F0=--- F1=0RD.

Halting condition (check HALT). F0 is the only undefined transition, and only B1 (1RF) enters F. So the machine halts exactly when B reads a 1 whose right neighbour is 0 (B> 1 0).

1. Picture

Positions are absolute cells. Blocks are 4 cells; "block k" means cells 2+4k .. 5+4k. The tape has three zones:

   zone L (cells <= 17)                         | zone M (cells 18..617)          | zone T (cells >= 618)
   wall, binary counter (6-cell digits),        | 150 blocks (4..153): the word w | cell 618 = 1, throttle s3 d0..d_{K-1},
   junction, inner throttle (cells 2..17)       | ('.' = 0110 when blank)         | marker Q, big region (0011)^e, 0^inf

• L counts round trips in a binary counter. Every 3·2^m trips it overflows into a pause. The pause runs a second, inner throttle at cells 2..17, and its carry-outs are sent right.
• M is a ternary word w. It is blank in the normal regime. In a pause it is filled by L's carries. Afterwards it is swept back to blank. The sweep either dissolves the word or leaves one glider that walks to the right end of M.
• T is the throttle observed in the earlier stages. Normal trips increment it, and a carry out of its top digit appends one block to the big region (the right edge grows). The glider arrives at T as five B visits, which can delete one throttle digit (K → K−1).

2. Visits and the zone decomposition

A visit at boundary b (between cells b−1 and b) starts when the head steps from b−1 to b in some state X (the in-state). It ends when the head next steps from b back to b−1, in some state Y (the out-state). We write it XY.

Composition principle (exact; busycoq Longitudinal, segRLs/sideRLs). Split the tape at b. Suppose the right part answers every visit it receives with an out-state that depends only on the in-state and its own content. Then the left part evolves as if every visit were answered by an oracle, and the right part evolves only through the visits it receives, in order. If every answer the right part actually gives equals the oracle's answer, then the whole machine never halts exactly when neither part halts.

Interfaces (checks IFACE-types, FULLPY). In the run from blank to 1.3e10 steps: - b18 sees only AC and DC (833,504 visits); - b618 sees only AE and BE (803,803 visits); - an independent Python run to 1.6e7 steps gives the same visit runs.

So L talks to M with the letters A and D and always gets C back. M talks to T with A and B and always gets E back. L is therefore autonomous: its run is one fixed sequence, whatever M and T contain. M and T only consume visit words. The proof below follows the visit words: L → (word over {A, D}) → M → (word over {A, B}) → T.

3. Zone L: the visit word it emits (F1)

Epoch structure (check IFACE-alternation, IFACE-epochs). L's visit word at b18 is

A^{N_2} D^{c_3} A^{N_3} D^{c_4} A^{N_4} ...

One D-run is the pause of one counter overflow (epoch m). Measured in the full run:

Epochs m = 3..8 are the start-up, and m = 5 also sends a 5-visit burst. For m = 9..16, N_m = 3·2^m − δ_m with δ_m ∈ {2, 4, 6, 8}. The proof uses only N_m ≥ 3,000.

What L does inside a pause is described in notes.md (rules PI, PJ: the pause-mode counter feeds an inner ternary throttle at cells 2..17; its carry-outs are the D visits, including the a(s3', t0, t1) cleaning visits of the inner-zone table). Each D visit is a carry of the inner throttle into M.

F1 (zone L, the pause counter): flagged. For every m ≥ 15, zone L at the start of pause m (left zone (011011)^(m−2), the fixed inner zone, oracle C at b18) never halts. It emits exactly D^{c_m} A^{N_m} with N_m ≥ 3,000, and then it is at the start of pause m+1.

Validated: m = 9..17 in the full run (this table); constructed pause starts m = 3..27 run to their ending (deepen stage); 550 mid-pause instances; PI 23,495/23,495 trips. Not derived: the pause-mode left counter (digits 011010/011011, wall 000001, three left records per pause) has no per-trip rule.

The values c_m do not matter below: M's rules hold for every c. Only "one D-run, then at least 3,000 A's" is used.

4. Zone M: an exact ternary word

State. w = w_4 .. w_153, one letter per block, LSB first: . = 0110 (0), 2 = 0010 (1), 1 = 1110 (2), and 0 = 0000, a transient junk block that only appears at the frontier. The frontier is the first block that is not ..

Rules (exact per visit; check ZM, 160 random instances; the earlier stages checked CL on 19,732/19,732 visits and PM on 23,495/23,495 trips). Every visit at b18 is answered C.

Inside an MA3 visit the 1 block passes through four intermediate patterns before it becomes .. Each one sends an increment signal right, and the four increments make the +4.

Lemma CL (the ending, exact given MA). Let v be the value of w read from its frontier (. positions skipped). An A-run changes v by the map g: - v ≡ 1 (mod 3): v → (v−1)/3, in 2 visits; - v ≡ 2 (mod 3): v → (v+10)/3, in 1 visit; - factors of 3 are free (the frontier moves).

For v > 5, g(v) < v. The values 0..5 go to 0, except 5, which is fixed (check GMAP: every v < 3^10 ends at 0 or 5; 3^8 of them at 5). So every word ends either clean (v = 0) or as the glider 12 (v = 5). The glider moves one block per A visit (12 → .12, since 2 + 4 = 5 + 1·3). At the top of M, its last two visits carry 1 and then 4 units out of block 153, so T receives exactly five B visits. After that, A visits pass (MA0).

Length bound. In an A-run the frontier advances at least one block every two visits: MA1 and MA3 advance it, and MA2 is always followed by MA1 on the same block. A glider advances one block per visit. So after at most 2·150 = 300 A visits the frontier has passed block 153, and M is blank and passes visits again. Since N_m ≥ 3,000, M is blank at the start of every D-run. In epoch m, T therefore receives a single B-burst B^{j_m} followed by A^{n_m} with n_m ≥ N_m − 300 ≥ 2,700.

Burst sizes. After D^{c_m} from blank, w is the ternary form of 2·c_m at block 5. While it fits in M (for m below about 236), j_m = 5 if g ends at the glider and 0 otherwise. The creep trigger at m = 14 and 22 follows from this, as the exact_rules stage showed at 18/18 pause ends. For larger m, MD carries out of block 153 (MO) and j_m also counts those carries. Their number roughly doubles with each m, so it is unbounded (check ZM includes 40 near-full words with top carries).

5. Zone T: the throttle

Canonical form T(θ; e): cell 618 = 1, then the groups θ = s3 d_0 .. d_{K−1} (P = 1001, Q = 1011, R = 1000), the marker Q, (0011)^e, then 0^inf. K ≥ −1; K = −1 means there is no s3 and the marker sits at 619. The rest point S0 has θ = PPP (K = 2) and e = 5,521 (check INIT).

Every visit is answered E. TB is the same frontier rule as M's MA. The throttle is to the middle what the word w is to L's carries.

F2 (the absorption tail): flagged. For every canonical T(θ; e) with K ≤ 2 and e ≥ 25, the word B^5 A^2600 never halts. Every visit is answered E, and it ends in a canonical T(θ'; e') with K' ∈ {K, K−1} and K' ≥ −1. K' = K−1 exactly when an R step is still half done after the fifth B visit.

Validated: all 40 throttles with K = −1..2 in the zone (check TBURST5). Not derived: how the A visits finish a half-done R step and drop the marker.

Restricted to K ≤ 2, and why. At S0, K = 2, and no rule raises K, so K ≤ 2 is the whole reachable range. For K = 3 the lemma as stated is false in the zone for 3 of 81 throttles (RRRP, RRRQ, RRRR; INFO line of TBURST5). They end with a dead slot: a 0011/0000 block between the digits and the marker, which then toggles while the marker stays put. The earlier full-machine grid (363 states, K ≤ 4) checked the middle and the record gaps, not the throttle's form, so it did not see this. The dead slot did not halt in 4,000 further A visits, but it is outside the canonical family.

F3 (the MS overflow, MO): flagged, and false in its canonical form. Needed: for every burst B^j, j ≥ 1, followed by at least 2,600 A visits (e ≥ 30), T never halts, answers E, and returns to a family that is closed under the epoch step. The canonical family is not closed. In 6 of 40 random tests (K ≤ 2, j ≤ ~2,700; INFO line of TBURSTJ), T ends with a dead slot (as in F2 at K = 3; for example T(RRQ) with j = 3) or with leftover big-region blocks. Every one of those runs still answered E and did not halt (40/40, check TBURSTJ).

Validated (safety only): 40 random throttles with K ≤ 2 and j up to about 2,700, and 190 constructed full-machine probes with at most 5 overflows per pause (deepen stage). Not derived, and the weakest point. A proof needs a wider invariant family, with dead slots and big-region remnants, that is closed under all later bursts. For j beyond the throttle's value, B visits pass into the big region, where they build a further counter with digits 0011 / 0111 / 0001. The throttle's carry-outs then dismantle it. That is a third nested counter level with no rule yet. j_m grows without bound from m ≈ 236 on (about 10^72 steps).

Why the burst shape matters (check TNEG). T is not safe for arbitrary visit words: T(RR; 30) fed B A^7 B A^8 B answers C on the last visit, which leaves the decomposition. So F2 and F3 must use the fact from section 4 that B visits come in one burst per epoch, followed by at least 2,700 A's.

6. Coverage and the non-halting argument (conditional on F1, F2, F3)

Invariant Inv(m), at the b18 rest point just before the D-run of pause m: - L is at the start of pause m; - M is blank; - T is canonical with some K ≥ −1 and e ≥ 30.

Step Inv(m) → Inv(m+1), for m ≥ 15: 1. L emits D^{c_m} A^{N_m} (F1), and every visit is answered C. 2. M: the D-run builds 2·c_m at block 5 (MD) and sends the MO carries as B's. The A-run then ends clean or with the glider (CL) within 300 visits (sending the B's of section 4), and passes the remaining A's. M is blank again. 3. T receives B^{j_m} A^{n_m} with n_m ≥ 2,700. If j_m = 0, it applies TA only. If j_m = 5, F2 applies (and j_m = 5 is the only nonzero case for m < 236). Otherwise F3 applies, in a form not yet found (section 5). With F2, T is canonical again, with K' ∈ {K, K−1}, K' ≥ −1 and e' ≥ e (TA only adds blocks; the burst checks also confirm e' ≥ e). The remaining A's are TA visits. 4. L is at the start of pause m+1.

Every case is covered. L has one rule (F1). M's visits are D or A on a blank or ending word (MD, MA0..MA3), and their order is fixed by F1. T's input is a single burst followed by a long A-run, with K ≥ −1. K = −1 is a fixed point: there is no throttle digit left to lose, and TA−1 and F2 keep the marker. From m ≈ 236 on, Inv(m) has to be widened to whatever closed family F3 turns out to need (section 5); until then the argument covers m < 236 only.

Progress. Each epoch has at least N_m ≥ 3,000 visits, each of them finite. The run is an infinite sequence of finite visits. If no visit halts, the machine never halts (progress_nonhalt_cond, with Inv as the invariant).

No visit halts. A halt needs B> 1 0. Every exact rule above is a deterministic finite run that ends in the stated configuration, so it never executes F0. F1, F2 and F3 each include "never halts" in their statement.

7. Initial segment

From the blank tape, direct simulation reaches the rest point S0 at step 300,032,133: the head at cell 17 in state C, M blank, T = T(PPP; 5521) (check INIT, from data/funded/cfg_3e8.txt; --long regenerates that file from blank). S0 lies in the A-run of epoch 14, after the m = 14 glider was absorbed. From S0 the remaining A visits of that run pass M (MA0) and act on T by TA. Inv(15) holds at step 623,793,383, the first D of pause 15, and the full run to 1.3e10 also confirms it directly (IFACE). Epochs m < 15, including the start-up, are covered by that direct simulation, not by the rules.

The step count is far below what Bouncer_v3.v's multistep_c'_spec + native_check_eq pattern handles (2.96e9 steps), so the start is routine for formalization.

8. The flagged lemmas, and what would close them

The proof uses nothing else that is unproved. MD, MA0..MA3, TA, TA−1 and TB are exact per-visit rules. CL and the 300-visit bound follow from MA by arithmetic.

9. Formalization notes

• Template: SBCv8.v TM31 (same 10 wall, d = 011011, w = 0011/0110 vocabulary) for its Longitudinal machinery: segRLs_addmul_v2 transfer lemmas, Incs/Ovs counter lemmas, and DivModCases for the mod-3 digits. TM31's own invariant does not match (no ternary throttle, no pauses).
• Each zone rule becomes a segRLs lemma over visit lists: M with h_D, h_A and the outputs h_A, h_B at 618; T with h_A, h_B and answer E.
• Zone M's word is a ternary counter, and its frontier rule is the same as T's. One parameterized segment lemma may serve both.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).