1RB0LE_1LC1RD_1LA0RB_1RC1RB_1LF0LC_---0RC: never halts (CONDITIONAL — STUCK at the edge lemma)

• Machine: 1RB0LE_1LC1RD_1LA0RB_1RC1RB_1LF0LC_---0RC, viewer https://bbchallenge.org/1RB0LE_1LC1RD_1LA0RB_1RC1RB_1LF0LC_---0RC
• Sheet: Results row 903, blank status, class "Bouncer + Chaotic Edge", no notes. Discord: only on mxdys's UBRRBA_TODO list (2026-08-24), which Dennis ruled fair game. Mirror-image near-twins: #34 and R6 (see notes.md).
• Written for: the string itself.
• Status: STUCK at stage informal_proof. This is not a proof. Sections 2–5 reduce non-halting to one statement, the edge lemma (E′) in §6. Every other step is checked. (E′) is open, and it is the whole hard part. It says that a chaotic one-sided system never breaks, and no candidate invariant language for it is known (§6).
• Checks:
• python3 -B check_proof.py: all PASS, about 10 s.
• --sft adds the falsification test from §6.
• --cycles N sets the orbit length.
• python3 -B scripts/edge_sft/verify_refutations.py (about 10 min) re-checks the SFT refutations in §6 in pure Python.

Transitions: A0=1RB A1=0LE · B0=1LC B1=1RD · C0=1LA C1=0RB · D0=1RC D1=1RB · E0=1LF E1=0LC · F0=--- F1=0RC.

1. Families

Words (all fixed):

blk = 1101101101        R1 = 1011110110        G = 11110101
X0 = 110111100110011101100100100111101100100110110111010011           (54)
X1 = 1001001001100100100100110110110011101100100110110111010          (55)
X2 = 11011001001100100100100110110110011101100100110110111010         (56)
X3 = 101110100110110010011101100100100111101100100110110111010        (57)
X4 = 1101001101100100110011101100100100111101100100110110111010       (58)
X5 = 11011011001001100110011101100100100111101100100110110111010      (59)
X6 = 10011100110011101100100100111101100100110110111010               (50)

C_k(a, D) := 0^inf <A blk^a X_k D 0^inf, for k = 0..6 and a ≥ 0.

Tails are normalized. A tail D is a finite 0/1 word that is empty or ends in 1. D and D·0 describe the same tape, so trailing 0s always belong to the 0^inf. Every map on tails, in particular the probe map P of §6, is defined as "read the tape right of the junction and strip trailing 0s". check_proof.py does exactly this, and check NORM confirms that every orbit tail is nonempty and ends in 1. In Coq the issue does not arise: the tail is the side D *> 0inf, a stream, and a language becomes a predicate on sides.

One cycle is 7 bounces: C_0 → C_1 → … → C_6 → C_0. The bulk gains one block per cycle. Only the bounce out of C_0 (the probe) reads D.

2. Rules

Directed-head notation: <X reads the last cell on its left, and X> reads the first cell on its right. Steps are exact.

β = (β1..β6) = (9, 473, 55, 49, 77, 9), where β_k = 1 + j_k + 29 − 58·m_k (with m_5 = 0 and m_6 = 1).

Every rule except P0 is a context-free fact. Each finite rule (WS, WE, J_k, and the one-block bodies of RS and LS) was executed with every cell outside the displayed window set to UNKNOWN. Reading an unknown cell would fail the check, and none of them does. So each rule holds in every context, and RS and LS hold for all n by induction. J1–J4 and J6 do need their R1 context blocks: with one block fewer, they read an unknown cell. That is where the domain lower bounds on a come from. J5 needs none.

Composition for B_k (k = 1..6), written out: - Start: 0^inf <A blk^a X_k D. - →WS→ 0^inf 1 B> blk^a X_k D. - →RS(a)→ 0^inf 1 R1^a B> X_k D. - →J_k→ 0^inf 1 R1^(a−m_k) G <E 0 Y_k D. - →LS(a−m_k)→ 0^inf 1 G <E 0 blk^(a−m_k) Y_k D. - →WE→ 0^inf <A blk^(a−m_k+1) Y_k D.

Here Y_1 = X2, Y_2 = blk X3, Y_3 = X4, Y_4 = X5, Y_5 = X6 and Y_6 = X0 (J6 eats the leading 011 of its D). This gives C_{k+1}(a, D) for k ≠ 5, C_6(a+1, D) for k = 5, and C_0(a, D′) for k = 6, where D = 011 D′. B0 is the same composition with P0 in the J slot.

D is untouched by B1–B5. B6 reads only the 011. The probe touches nothing outside the R1 block and the cells to its right.

3. Coverage

The family is visited in the fixed order C_0 → C_1 → … → C_6 → C_0, and each C_k has exactly one rule. Each phase holds the tail its predecessor produced. C_1 to C_6 all hold 011 P(D), so B6's 011 precondition always holds. a never decreases and starts at 59, so every domain bound (a ≥ 0, 1 or 2) holds.

The only uncovered case is C_0(a, D) with D ∉ L. The invariant is Inv(C_0(a, D)) := a ≥ 2 ∧ D ∈ L. CYC preserves the a-part, and (E′) preserves the L-part.

4. Initial segment

0^inf A> 0^inf →(784,041 steps)→ C_0(59, D_0), where D_0 = work/D_cycle0.txt (261 cells, starting 0110010011011011…). This was checked by direct simulation from the blank tape in check_proof.py (INIT).

There is an earlier entry: the run is at C_1(58, 011 D_0) at step 758,939 (check INIT1). From there, B1–B6 lead to C_0(59, D_0) at step 784,041, matching the step formulas exactly (758,939 + 4·70·58 + 9+473+55+49 + 70·58+77 + 70·59+9 = 784,041). This is the earliest left-record moment at which the tape has the full C_k shape. The J rules read only short prefixes of the X_k (the skeptic reports 3 cells of X1 for J1 and 2 of X6 for J6), so trimming the X_k would probably allow an even earlier entry. That is not needed.

The initial segment is routine, not an open issue. Bouncer_v3.v proves c0 -->* S' 23 over 2,964,716,529 steps with eapply without_counter with (n:=…); eapply multistep_c'_spec; native_check_eq, where multistep_c'_spec is a lemma local to that file. 784,041 steps is far below that.

5. Conclusion (conditional on E′)

From C_0(59, D_0), CYC applies forever: C_0(59+n, D_n), with D_{n+1} = P(D_n) ∈ L. Each cycle takes at least 490·59 steps, so progress holds. Hence, if (E′) holds, the machine never halts (progress_nonhalt_cond).

Halting transition. F0 is the only undefined transition, and only E0 (1LF) enters F. So the machine halts exactly when E reads a 0 whose left neighbour is 0 (0 E> 0), for example via 001 C> 0 (C0→A1→E0→F0, as in notes.md). Every rule except P0 is an exact, fully defined run, so it never executes F0. For P0, (E′) itself demands that every excursion return, so the probe never halts either. The whole question of halting therefore sits inside the edge lemma.

6. The open piece: the edge lemma

6.1 What (E) says, honestly

The first version stated:

(E) There is a set L of normalized tails with D_0 ∈ L such that, for every D ∈ L, the run from R1 B> X0 D 0^inf reaches G <E 0 X1 011 P(D) 0^inf in finitely many steps, never reads left of the R1 block, never halts, and P(D) ∈ L.

(E) is not a reduction: it restates the problem. Take L = {D_n : n ≥ 0}, the orbit. It satisfies (E) exactly when the orbit never breaks, and that is non-halting itself. What §2–§5 actually establish is narrower. Non-halting reduces to (E), every other step is routine and checked, and the open content is a closed language L, which nobody has.

6.2 The sharper form: a one-sided protocol system (E′)

The probe splits cleanly at the boundary one cell left of the X0|D cut, between the last two cells of X0: - The left part is R1 X0[0..52] (63 cells; left of that, the context is unknown). - The right part is X0[53] D 0^inf = 1 D 0^inf. Call its cells 0, 1, 2, …

Check IFACE. On every one of 3,000 orbit cycles, the head crosses this boundary in the same sequence: 32 crossings, i.e. 16 round trips. As (state entering the right part, state leaving it) pairs, the sequence is:

(B,C)(D,E)(C,A)(D,C)(B,C)(D,F)(C,A)(B,E)(D,E)(B,C)(B,E)(B,C)(D,A)(C,A)(C,A)(B,C)

At the cut itself (between X0's last cell and D), the sequence is not fixed: there are 2 distinct sequences over the same 3,000 cycles. (notes.md previously said "crosses exactly 16 times"; that was wrong and is now corrected to 16 round trips.)

The left part's content is the same at every probe. It is deterministic, and it hears from the right part only through the states in which the head leaves the right part. So if the right part always answers with the out-states above, the left part always behaves exactly as on the orbit: - it sends the same in-states; - it never reads left of R1; - after the 16th return, it ends at G <E 0 X1[0..53], with the right part's cells 0..3 forming the last 4 cells of X1 011.

That leaves a statement about the right part alone.

(E′) edge lemma. Let in = BDCDBDCBDBBBDCCB and out = CEACCFAEECECAAAC. There is a set L of normalized tails with D_0 ∈ L such that, for every D ∈ L: - Start from the half-tape 1 D 0^inf (cells 0, 1, …). For p = 1..16 in turn, put the head on cell 0 in state in_p and run. The head eventually steps left off cell 0, in state out_p, without halting. - Afterwards, cells 0..3 read 0011. - P(D) := cells 4, 5, … with trailing 0s stripped, and P(D) ∈ L.

So (E′) implies (E). The left part's half is one finite execution, the same for every D, and the orbit run already performs it with the context left of R1 UNKNOWN (edge() in check_proof.py). Check E′ confirms that the right-part system with this protocol reproduces P exactly on the first 500 orbit tails. In busycoq this is exactly the Longitudinal split: - the left part's response to the fixed crossing list is a sideRLs fact (finite, vsideRLs_es_spec + native_check_eq); - the right part's response is (E′); - sideRLs_concat_v2 glues the two, as BigStep does in Bouncer_v3.v.

(E′) is still not proved. It isolates the open problem in a system with no bulk and no unknown context.

6.3 What is known about P (evidence, not proof)

• Orbit (scripts/edgemap.c, 5.5·10⁶ cycles; re-run here for 3,000):
• no break, no halt, no repeated D (exact hash);
• |D| ∈ [144, 564] with no drift;
• j0 ∈ [2257, 28813] over 3,000 cycles (the skeptic's independent 5.6·10⁶-cycle run: [2251, 39467]).
• Length. |D_n| is always a multiple of 3, and |D_n| + 3n ≡ 21 (mod 30) on 3,000 cycles (check NORM).
• Prefix. The first 24 cells of D take only 8 values. Deeper cells are chaotic: 3,786 distinct per-cell crossing sequences over 120 cycles, with no saturation. So a Bouncer/crossing-sequence argument on D is out.
• No arithmetic counter has been observed. The deep excursions (depths of 24, 56 and 80+ cells, and up to the end of D) look like zig-zag fronts that rewrite D locally. Whether any regular (finite-state) invariant exists is unknown. The data fit equally well with none:
• k-factor counts grow about 1.6^k with no saturation;
• every SFT_k tested is refuted (below);
• plain CPS does not close;
• D does not repeat in 5.5·10⁶ cycles.

So this is not a cryptid in the ground-rule-6 sense (no pseudo-random arithmetic has been seen), but nothing shows that it is tractable either.

6.4 What has been ruled out

1. SFT_k invariants: refuted for every k ≤ 36 tested. The SFT_k language is L(F, P) = {D : D[:k−1] ∈ P, every k-factor of D·0^k ∈ F}. For it to be an invariant containing the orbit, F must contain all orbit k-factors and P all orbit (k−1)-prefixes.

• k ≤ 22. Random tails built only from orbit factors break the cycle:
• with 200 samples per k (check_proof.py --sft), there are 30, 2 and 10 breaks at k = 8, 12 and 16 (this run; an earlier run gave 34, 7 and 11, because the sampling order depends on Python's string hashing, but both runs found breaks at every k);
• with 1,000 samples per k (scripts/edge_sft/sfttest.py), there are 74, 54, 125 and 3 breaks at k = 10, 14, 18 and 22.
• k = 24, 26, 28, 30, 32, 36 (new, this revision). The earlier "no breaks at k = 26" came from sampling with the orbit's prefixes only. A closed L(F, P) must also contain the prefixes of P(D) for every non-breaking D in it. scripts/edge_sft/sftgrow.c builds such a chain, and work/sft_refutations/refute_k<k>.txt records it for each k:
• link₁ ∈ L(orbit factors, orbit prefixes), so it lies in any such L.
• link₁ completes a cycle, so P(link₁) lies in L, and so does its prefix.
• D has only orbit k-factors and that prefix, so D ∈ L.
• D* breaks the cycle. Contradiction.

For k = 36 the chain has two links. The breaking tails are 195–693 cells long, comparable to orbit tails (144–564). scripts/edge_sft/verify_refutations.py re-checks every chain in pure Python: it regenerates the 200,001-tail orbit, checks factor membership, and checks that each link cycles and D breaks. In the sampling, the share of tails drawn this way that break falls only slowly with k: 6–9% at k = 24–30, and 2.5–3.5% at k = 32–36. So no SFT with window ≤ 36 is an invariant, and nothing points to a threshold k. - The observer's SFT* (avoiding {000, 0101, 01101111}) is not closed either (notes.md).

2. Plain n-gram CPS: does not close. These are scratch native tools, scripts/edge_cps/, written this revision and checked only on toy machines. A failure here means only that this abstraction is too coarse. - Whole machine (ngcps.cpp; no history, no LRU). It reaches an abstract halt for radii n = 4, 8, 12, 14, …, 26, and for (left, right) = (8,24), (12,24), (24,12) and (6,28). Radius 28 and (28,8) hit the 6 GB memory cap. - Edge system (E′) (edgecps.cpp). The left side is exact (the protocol), and the right side is an n-gram CPS with a wall-aware left window. It reaches an abstract protocol break for n = 4, 6, …, 24, for (26,24), and for left radius 6–20 with right radius 30 or 40.

3. busycoq CTL62 Nsolve_cert (whole machine): no result. I ran it twice, once with CPS_LRU 10001 2e6 2e6 10 3200 1 3 0 0 and once with NG 0 2e6 2e6 12 1 12 0 true. Each grew to about 10 GB RSS within 5 minutes and was killed to protect the host. That is not evidence either way.

6.5 Routes, with honest costs

1. A whole-machine CTL certificate (preferred, if one exists). It plugs into CTL62's Nsolve_cert / decide_nonhalt_spec as is: the conclusion is ~halts tm c0, and §2–§5 would become unnecessary. - Cost: a native reimplementation of busycoq's stronger CTL modes (NG with history/LRU, RWL_mod, MITMDFA) to search parameters beyond what mxdys's sweeps already tried. This machine is a holdout, so the standard ranges failed. Expect days of agent time, with an unknown chance of success.
2. An edge-only closed set, plus custom Coq glue. busycoq has no interface for this. CTL.v's decide_nonhalt_spec concludes only ~DHTMFromTM.TM.halts' tm DHTMFromTM.TM.c0, and CTL_decide_nonhalt_spec concludes ~halts tm config_init. Both are about a closed run from the blank tape; neither takes a custom start, an accept condition, or a protocol. Using an edge-only certificate therefore needs one of: - (a) a new checker for the (E′) protocol system (finite closed set of right-part configurations, with the start "1 D 0^inf, D ∈ L" and the 16 in/out transitions as side conditions), together with its soundness proof, giving (E′) as a Coq lemma; - (b) an adapted CTL closure check with a start-and-target pair.

Either is a new decider-sized development: estimate 1–3 weeks of agent time on top of finding the closed set, which nobody has (6.4). 3. Hand analysis toward a grammar. Treat the probe's excursions as particle rewrites and look for a non-SFT description of L, for example a context-free or counter-like constraint coupling D's prefix to its body. - The refutations hint at the coupling: in every chain, D* is built from orbit factors and fails only through a prefix/body mismatch. - Cost: open-ended research.

Priority call for Dennis. Should more budget go into (E′)? None of the routes is cheap, and whether a regular invariant exists at all is unknown.

7. Mapping to busycoq

What is new relative to Bouncer_v3.v: the bounce rules have seven junction phases instead of one, and the probe phase is chaotic. Everything except (E′) is routine.

8. Evidence (check_proof.py, 2026-10-10, all PASS)

• RS, LS, WS and WE with unknown context.
• J1–J6 with unknown context, plus minimality of their R1 context.
• B1–B6 by full simulation, with D UNKNOWN and the exact step formula, for 21 values of a each, from the domain minimum up to about 2,800. The skeptic independently checked up to about 3,800.
• P0 on a 3,000-cycle orbit from D_0. The junction stays intact, nothing halts, and the run reproduces work/D_edgemap_1951.txt at cycle 1951.
• NORM: orbit tails are normalized, and |D_n| + 3n ≡ 21 (mod 30).
• IFACE: the 32-crossing (16-round-trip) sequence one cell left of the cut is identical on all 3,000 cycles. The cut itself has 2 distinct sequences (info).
• E′: the right-part protocol system reproduces P on 500 orbit tails.
• B0 on 25 random pairs (a ∈ [1, 800], orbit D).
• CYC on 6 random pairs.
• INIT1 at 758,939 steps and INIT at 784,041 steps.
• HALT: only F0 is undefined, and only E0 enters F.
• Separately, scripts/edge_sft/verify_refutations.py confirms the SFT_k refutations for k = 24, 26, 28, 30, 32 and 36.

Not proved: (E′).

9. Review log (skeptic review, 2026-10-10)