1RB0RF_1RC0RE_1LD1RA_1LA0LD_1RA---_0RA0LB

Status: STUCK after the funded crossing stage (confidence med: Lemma S proves the bell after any epoch with Y_e < 2^(bitlen N_e + 1) is safe, so non-halting reduces to the Big-Y lemma, which was not proven; stop rule: parked with R2; see "Funded stage (2026-10-10, crossing)" and decision.json) Class guess (agent / Dennis): Bell eats counter: FractalBEC-like 101/00 bouncer plus a 3-cell binary counter with transparent J blocks; the bell shifts the counter one cell / – Spreadsheet notes / Discord thread: Results row: class "Bell eats counter"; status, notes, sources and done-by are all blank. Not in data/discord/*.txt (mxdys UBRRBA 86, dyuan01 longitudinal 24). No claim. Byte-exact in data/holdouts/2026-10-07_778.txt (line 215). Present in all 26 snapshots since 2024-06-14. Not in data/solved_index.tsv (no byte-exact, notation or mirror/rename match). Viewer: https://bbchallenge.org/1RB0RF_1RC0RE_1LD1RA_1LA0LD_1RA---_0RA0LB

Pool: R3 in reports/targeting.md §4.4. - Template neighbour: FractalBEC.v tm1 = 1LB0LF_1LC0LE_1RD1LB_1RA0RD_1LA---_0LA0RB. Its L/R mirror 1RB0RF_1RC0RE_1LD1RB_1LA0LD_1RA---_0RA0LB differs from ours only in C1 (template 1RB, ours 1RA). - Open 1-transition neighbour (found with python3 -B scripts/near.py "$TM" ../../data/holdouts/2026-10-07_778.txt 2; tools/holdouts.py contains confirms it): 1RB0RF_1RC0RE_1LD1RA_1LA0LD_1RA---_0RE0LB (F0: 0RE instead of 0RA), line 408, sheet class "Bell eats counter", notes blank, no machines/ folder. It is not a trajectory twin: at 1e9 its span is -528..4283 with 2,064 nonzeros, ours is -520..4329 with 3,147.

Observation

• Direct simulation (tools/sim.py, C core): no halt to 1e9. Span -520..4329 (4,850 cells), 3,147 nonzeros at 1e9; 677 cells at 3e6; -1476..13891 (15,368 cells) at 3e10 (scripts/hublog.bin). Span grows like t^(1/3).
• compress track (record-aligned): right records are 0^inf (101)^a 0^2 (101)^b <counter> C> with a = 2^k - 1 (a doubles per visit). Left records are 0^inf <D (010)^N T 0^inf, one per epoch, with an irregular residue T.
• Hub found by hand from per-step traces (scripts/tmlib.py, parse_K): K(a,b,G) = 0^inf (101)^a 00 (101)^b A> 0 enc(G) 0^inf. The head is in A, has just moved right, and reads the cell between the block region and the counter. enc maps 3-cell groups: 0 = 000, 1 = 010 (counter digits, LSB first), J = 100, x = 001, z = 011, w = 101. A J block is exactly a 101 block in its left-pass form, which is why J blocks can turn back into blocks (rule E).
• From blank: K(0, 2, ε) at step 12. The hub log data/hubs_1e9.txt has 192,530 hubs to 1e9: 82 bell sweeps, 487 b = 0 hubs, N = 1,603 at the end.
• Epoch lengths N (the a+b right after a bell): 2, 5, 6, 11, 18, 44, 50, 53, 83, 93, 94, 104, ... 1,583, 1,603. dN ranges from 1 to 103.
• Counter value = a within an epoch until the first partial eat (for example a = 8 has digits 0,0,0,1). The J blocks sit between digits and are skipped by the carry.
• Non-standard groups x/z/w appear only right after a bell. In the 1e9 log, x/z/w are always followed by x or 0. No b = 0 hub ever has one, neither in the direct run to 3e10 (1,394 b = 0 hubs) nor in the macro run (below).
• Images (img/):
• default_site_10k.png: bbchallenge Default, site view.
• hubs_counter_epochs.png: custom, one row per hub, 4 epochs from step 2,850,432. Most telling.
• explore_constructed_eat.png: Explore view from K(5,2,0JJ1). It shows R1, E, R1, then B1.
• records_1e8.png, blaze_1e7.png.
• Tools:
• rulefit was not run: the exponents are not the right coordinates, because the state lives in the word G.
• qsim was not needed: the dedicated hub logger reaches 1e9 in 5 s and 3e10 in about 2.5 min.

Candidate rules

Notation: inc = +1 on the digit groups of G (LSB first, J skipped, a new top digit appended after the last group). σ(G) = shift every 1-cell of enc(G) one cell to the left and re-read the cells in 3-cell groups. So σ maps a digit 1 to J, and a J to an x/w mark on the group before it.

• Random counts are over seeds 2026, 7 and 99. Command: python3 -B scripts/validate_rules.py <seed>. It runs direct TM simulation from the constructed K configuration up to the next hub.
• Orbit lockstep: python3 -B scripts/check_orbit.py data/hubs_1e9.txt. Every one of the 192,529 hub transitions from blank to 1e9 matches R1/R1x/E/B0/B1. The macro simulator scripts/macro.py reproduces all 1,394 b = 0 hubs of the direct run to 3e10 (data/hubs_b0_3e10.txt) in order.
• Macro run (scripts/macro.py): 20,000 epochs, reaching N = 192,042 (very roughly 1e15 TM steps, from a 3N²-per-epoch estimate calibrated on 1e9). No b = 0 hub with x/z/w.
• Cleanup: in 19,773 epochs a bell left x/z/w marks. Each time the marks were gone after n = 2^q increments, with q ≤ floor(log2 N); the typical q is floor(log2 N) - 12. The worst margin was 16 of 25 (epoch 8). Data: data/macro_epochs_2e4.json.
• R1 step count: about 6b plus a carry-dependent term in steps of 4. Not fitted; not needed for Checkpoint A.
• Things that died:
• My first hub parse: transit 101 blocks right of the gap look exactly like J blocks. Fix: a hub's first group is never J.
• My first C pre-filter rejected hubs whose G starts with x.
• Two "E failures" in validate_rules were harness artifacts: a mid-eat parse with G[0] = w was accepted. The real next hub matched E.
• Halting is reachable from bad words: K(5,6,1z0101) halts in 19 steps, and random words with x/z/w followed by 1/J/z/w halt or leave the language (56/800 halts in scripts/l0test.py). So the invariant has to be specific.

Template check (verify/FractalBEC.v, Section FractalBEC + tm1 at line 206; I read the whole file): - The template's rule set is LInc (2-cell counter d1 = [0;1]), RInc (w1^(1+n) w0 w1^m → w1^n w0 w1^(1+m), w1 = 101, w0 = 00), Incs, and Ov (L(2^n) |> R 0 m r → const 0 <| w0^n w1^(2+m) r), then the fractal P0/P1 recursion with config i = w1^(2^i - 1). - Ours shares the bouncer: the gap step inside R1 is RInc, mirrored. - The counter is different: 3-cell digits 000/010 with transparent J = 100 blocks. LInc was not run, because the encoding does not match. - There is no Ov or fractal recursion. The b = 0 step is E/B0/B1 by the low digits, with the one-cell shift σ, and the epoch lengths are irregular rather than 2^i - 1. - Verdict: partly (bouncer only). - The closer relative is R2 (1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LD0RC, BECv1 tm108 twin). Its deepen stage found the same "drop a suffix, shift the grid one cell" eat and a pending-size invariant.

Cryptid check (ground rule 6): not a cryptid candidate. - The b = 0 branch is a regular function of the low digits (prefix 0 1^r J^k, 0 1^r 0 or 1), and the bell is a fixed one-cell shift. There are no parities of exponentially growing numbers, no ×3/2 and no Collatz-style branching. - N grows by about 9.6 per epoch on average. - Non-halting reduces to a structural lemma (cleanup before the next b = 0) whose bound is a power of 2 against N. In the data this bound never comes close at large N.

Checkpoint A (Dennis)

(waiting; questions on the card, decision in decision.json)

Informal proof

Not started (stage gated: confidence med). Sketch for the proof-prep stage: 1. Formal hub K a b G with G an Inductive list of groups. R1 by induction over the digit list (J transparent). E, B0 and B1 as finite case lemmas, with σ as a list function. 2. Invariant I(G): G is standard ({0,1}{0,1,J}*) at every b = 0 hub. After a bell, G = σ(W) for a standard W. 3. Cleanup lemma (the open piece): for G = σ(W), the first carry into the lowest x makes z, and the next carry into z x^j turns the run into 0 J^(j+1) and continues. All marks are gone after 2^(p+1) increments, where p is the digit index of the lowest mark. Need 2^(p+1) ≤ N, from where σ puts marks: J blocks come only from old 1-digits. 4. Then the nonhalt argument: each hub reaches another hub (R1, E, B0 and B1 are total on standard G; R1x is total on σ-words during cleanup), so progress_nonhalt applies on the hub family.

Formalization log

–

Outcome

–

Decision (2026-10-10, auto-applied)

Question: Should R3 get a proof-prep stage on the cleanup lemma (x/z/w marks left by the bell vanish before the next b=0), done together with R2's size invariant, or be parked? Answer: prep (Proof-prep stage on the cleanup lemma (shared with R2)). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was at lunch). Override any time.

Funded stage (2026-10-10, prep)

Scope (decision prep): derive the carry transducer on σ-words natively, prove the cleanup bound on paper, fuzz it. Shared theme with R2's size invariant. Scripts and outputs are in scripts/prep/. Coq was not used. proof.md was not written, because the bound did not close.

Outcome: the cleanup is now exact, and the bound reduces to one inequality L*, which is not proven. Confidence stays med. The old guess (cleanup within 2^(p+1), p = index of the lowest mark) is replaced by a closed form.

New coordinates: A-frame tokens (tok.py)

• Read the cells right of the hub head starting at the head cell (a 0 at a hub), greedily:
• 0 = 000, 1 = 001, j = 010 (3 cells each);
• t = 10 (2 cells);
• bad: 011 (A0 B1 E1 halts) and 11 (A1 F1).
• A standard group word reads letter for letter (0→0, 1→1, J→j).
• The bell shift σ (drop one cell) on a clean word: before the first j, 0→0 and 1→j; the first j becomes t; the rest is unchanged. So a bell leaves exactly one t, or none when V has no j. The x/z/w marks of the group view are this single t plus the phase shift after it (xx0J0w0w = 0tj101j1j, zx00Jw = 1tj011j).
• Mechanism:
• The right pass reads these tokens in state A: 001→111, 010→101, 10→00, and it turns at 000.
• The D pass erases 111 and restores 101→010.
• At a passed t (now 00) it restarts: it writes 1 0 1 and starts a fresh right pass one cell later.

R1 on every word (derived from the TM; replaces R1x)

inc(ε)=1, inc(0R)=1R, inc(1R)=0·inc(R), inc(jR)=j·inc(R), inc(tR)=j·inc(σ(inc R)) | check | result | |---|---| | all reachable marked words: σ(W) for every W = 0{0,1,J}^≤7, followed to clean (reach.py 7) | 11,584/11,584; each has exactly one t | | lockstep from blank to 1e9 (lockstep_tok.py, all R1 transitions in data/hubs_1e9.txt) | clean 189,846/189,846, one-t 2,196/2,196; every hub word has ≤ 1 t | | random clean words, direct TM from K(a,b,·), a ≤ 50, b ≤ 40 (fuzz_tok.py, seeds 2026/7/99) | 1,200/1,200 | | random one-t words on random post-bell paths, same harness | 1,000/1,000 (328 + 333 + 339) |

Cleanup time, exact

• Set-up:
• V is the clean word the bell shifts (B0: 0T'', B1: inc T).
• The depth of a token is the number of digit tokens (0/1) before it.
• The j's of V have depths d_1 ≤ … ≤ d_k, and f = d_k.
• Y = value(V) + Σ_i 2^(d_i).
• Cleanup lemma (paper, from the recursion):
• The t walks through V's j's in order.
• The digits below the t always hold exactly the number of increments since the bell.
• Each cascade adds 1 at the next j's depth and freezes the 1-digits it passes into j.
• So the t vanishes at increment exactly 2^P, with P = the number of 0 bits of Y among bits 0..f−1 (P ≤ f).
• After cleanup, Y's 1 bits are j's, its 0 bits are digit slots, the top j has depth zb(Y) (the zeros of Y below its top bit), and the counter value equals the number of increments since the bell.
• Validated (cleanup_formula.py):
• 100,000/100,000 macro epochs: the exact cleanup time; the top-j depth on all 19,774 dirty epochs of the first 20,000.
• 4,800/4,800 random V in the model.
• 240/240 random V by direct TM, counted hub by hub from K(0, 2^P+3, σ(V)) (84 + 77 + 79).
• The A-frame macro simulator (amacro.py) reproduces the N sequence of data/macro_epochs_2e4.json (20,000/20,000).

Proved on paper

1. Closure. {clean words} ∪ {words with exactly one t} is closed under inc and under σ of clean words, and inc never meets 011 or 11 there. So no halt occurs inside R1. The t-case recursion terminates because the number of j's after the t drops.
2. Depths never increase. σ and inc map tokens one to one (only 1→j and j↔t change, plus new top digits).
3. value(T) ≤ a at every b = 0 hub, with equality at the first b = 0 of an epoch (cleanup leaves value = increments = a; R1 adds 1 to both; E gives value(T') ≤ value(T)/2^(r+1) < a+2+r). Hence N ≥ value(V) at every bell (B1: value(V) = value(T)+1 ≤ a+1 = N; B0: value(V) ≤ value(T)/2^(r+1) < N). Checked on 199,045 b = 0 hubs and 100,000 bells (invariants.py 1e5): 0 failures.
4. If V has a digit after its last j (S1′), then 2^P ≤ 2^f ≤ value(V) ≤ N, so the t is gone before the first b = 0.
5. L* ⇒ S1′ next epoch. L*(e): 2^zb(Y_e) ≤ N_e. Then by the first b = 0 of epoch e the count has carried past the top j. E, B0 and B1 keep that order, so V_{e+1} has a digit after its last j, and (4) covers epoch e+1.

Open: L* (the only gap left for non-halting)

• L* must hold for every epoch e ≥ 16. Epochs 1 to 16 are a finite prefix to check directly; their cleanups are in time (the worst is epoch 8, at 16 of 25).
• Observed to 100,000 epochs (N = 1,091,790):
• L* fails only at epochs 7, 8, 14 and 15. S1′ fails only at 8, 9, 15 and 16, as (5) predicts.
• L*'s margin shrinks: min log2 N − zb(Y) is 0.687 bits to 20,000 epochs, then 0.319 at epoch 62,386 (N = 654,227, zb = 19). Y/N reaches 2.10. So L* may fail later, and it is probably not the right inductive statement.
• The quantity that actually matters, 2^P ≤ N, keeps a wide margin: min log2 N − P = 2.32 bits for N ≥ 100 (epoch 62,386, P = 17), and 0.64 overall (epoch 8).
• No inductive proof was found. A sufficient condition is Y_e < 2N_e with Y_e not a power of two at or above 2^bitlen(N_e). Since value(V) ≤ N, this is a bound on the j-weight Σ_j 2^depth(j) ≲ N. It needs control of how the frozen top bits of one epoch's Y re-enter the next Y.

Shared theme with R2 (and #28/#29/#30)

• R2's balls-and-gaps view counts a t as a pending increment of weight 2^gap, and INC adds 1 to (digit value + Σ_t 2^gap). Our Y is the same potential (digit value + Σ_j 2^depth).
• Our cleanup lemma is R2's Lemma A made exact.
• L plays the role of R2's R1 (T_k + 1 ≤ I_k). Both machines need the same crossing lemma*: the frozen top bits of the potential must not pile up while it passes a power of two.
• R3 is the cleaner instance:
• at each bell, every j becomes pending (the t walks through all of them);
• the cleanup time is a closed form;
• the safety requirement is the single per-epoch number 2^P(e) ≤ N_e, which has a 2.3-bit margin.

Proof route (unchanged in shape)

• Use the busycoq hub K a b T with T a token list.
• Prove R1 as a recursive inc lemma, by induction on the word; the t case uses well-founded recursion on the number of j's. E, B0 and B1 are finite case lemmas, with σ as a list function.
• The cleanup lemma is pure list arithmetic.
• The epoch induction needs L*, or a replacement for it. That is where a formal proof would stall today.

Still open: L* (or a direct inductive bound on 2^P ≤ N), the finite prefix (epochs ≤ 16) as an explicit hub chain, and step counts per macro rule.

Decision (2026-10-10, auto-applied, round 3)

Question: R3's cleanup is now exact and safety reduces to one per-epoch inequality (2^P <= N, via L), the same crossing arithmetic R2 is stuck on: fund one joint crossing-lemma stage, start Rocq on the exact rules, or park? Answer: crossing* (One joint crossing-lemma stage with R2 (2 h, native)). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.

Funded stage (2026-10-10, crossing)

Scope (decision crossing): search natively for an inductive bound aimed at 2^P(e) <= N_e, together with R2's R1. Stop rule: if nothing inductive appears, park R2 and R3 together. Scripts and outputs are in scripts/crossing/. Coq was not used.

Outcome: STUCK (stop rule). The per-epoch requirement is now weaker than L* and fails at no epoch to 1e7. It is still not proven inductively, so R3 parks with R2. Confidence stays med.

Integer epoch model (nmodel.py)

• A clean word is a pair (n, M): n is the value of the digit tokens, and M is the multiset of j depths. This restates tok.inc, amacro.b0rule and the prep cleanup lemma in integers:
• Y = v + Σ_{d∈M} 2^d; Z_x(Y) = number of 0 bits of Y below x; P = Z_{max M}(Y).
• Post-cleanup multiset M* = {Z_d(Y) : d ∈ M} ∪ {Z_p(Y) : p a 1 bit of Y}; its maximum is zb(Y).
• b=0 loop on (a, n, M*):
  • B1 (n odd): N' = a+1, v' = n+1.
  • E (n mod 2^μ = 2^μ − 2, μ = min M*, k copies): eat, n → (n >> μ) + k − 1, depths −μ, then repeat.
  • B0 (otherwise): N' = a+2+r, v' = n >> (r+1), depths −(r+1).
• Validation: | check | result | |---|---| | lockstep vs the token model amacro.py from blank, every epoch: N, v, M and the cleanup time (cmp_amacro_1e5.txt) | 100,000/100,000 | | same, token model run on its own to epochs 350,260..350,280 (cmp_amacro_350k.txt) | 21/21, including cleanup at 2^21 at epoch 350,274 | | whole epochs by direct TM, random states with N <= 200, from K(0, N, σ(V)) hub by hub to the next bell (epoch_tm.py, epoch_tm_3seeds.txt) | 1,200/1,200 (400/400 on each of seeds 2026, 7 and 99) |
• Speed: 1e7 epochs (N = 144,073,582) take about 2 minutes. The token model needed several minutes for 1e5 epochs.

New fact: the safety margin falls to 1 bit

• Every epoch is safe to 1e7 (longrun_1e7.txt). But the minimum of log2 N − P is 1.000 bit, at epoch 350,274. There N = 4,193,611 = 2^22 − 4,693 and the cleanup takes 2^21 increments; the token model agrees.
• So the prep stage's 2.32-bit margin holds only to 1e5 epochs.
• Cause: an exact-power pair. Y = 2^22 exactly at epochs 350,273 and 350,274, with N just below 2^22.
• L* fails at exactly 6 epochs to 1e7: 7, 8, 14, 15, 350,273 and 350,274.
• Every one of them has Y_e = 2^bitlen(N_e) exactly.
• They come in pairs: the first has eat shift s = 1, the second s = 0.
• The 1-bit margin is structural. Lemma S below proves that epoch safe, with a margin of about log2 N − (m − 1).

Potential identities (paper; checked)

• Let U = n + Σ_{d∈M} 2^d be the potential of the word at b=0.
• The three b=0 steps act on it as follows:
• E(μ, k): U → (U + 2)/2^μ − 2.
• B0(r): Y' = (U + 2)/2^(r+1) − 1.
• B1: Y' = U + 1.
• Checked: all 199,046 b=0 steps of the first 1e5 epochs and 96,498 random steps (lemma_s.py).

Lemma S (paper; checked)

Setting. Let epoch e be safe. Let m = bitlen(N_e), and let s be the total shift of e's b=0 loop: the sum of μ over its E eats, plus r+1 for a B0 bell (s = 0 for a B1 bell with no E). Write zb(Y) for the number of zero bits of Y below its top bit.

Statement. - C(e) means: zb(Y_e) ≤ m − 1 + s, or (s = 0 and Y_e = 2^m). - Lemma S: C(e) implies that epoch e+1 is safe.

Proof. - The top j of V_{e+1} has depth at most zb(Y_e) − s, and P_{e+1} is at most that depth. - Case zb(Y_e) ≤ m − 1 + s: then 2^P ≤ 2^(m−1) ≤ N_e < N_{e+1}. - Case s = 0 and Y_e = 2^m: - All old depths stay, because Z_d(2^m) = d. So M* = M ∪ {m}. - The B1 bell gives Y_{e+1} = 2^(m+1) + (N_e − v_e + 1). - Hence P_{e+1} = m − popcount(N_e − v_e + 1) ≤ m − 1, using 1 ≤ N_e − v_e + 1 ≤ 2^m and v_e ≤ N_e. - In the edge case N_e − v_e + 1 = 2^m, P = m and N_{e+1} = 2^m, so the epoch is still safe.

Corollary. If Y_e < 2^(m+1), then C(e) holds, because zb(Y_e) ≤ m with equality only for Y_e = 2^m. So C can fail only when Y_e ≥ 2^(bitlen(N_e)+1), which needs J_e > 2^m > N_e.

Checks. - Trajectory to 1e5: C holds at every epoch, and C ⟹ safe(e+1) holds 100,000/100,000. - Random states (half tuned to Y ≈ 2^q, 3 seeds): 59,887/59,887. - C is close to sharp: in the 113 random states where C fails, the next epoch is unsafe 10 times.

What is left: the Big-Y lemma

Needed: for every epoch, if Y_e ≥ 2^(bitlen(N_e)+1), then zb(Y_e) ≤ bitlen(N_e) − 1 + s_e. - With Lemma S and the prep results, this gives non-halting from blank. C also holds at epochs 7, 8, 14 and 15, so no finite prefix is needed beyond init and epoch 1.

Observed to 1e7 epochs (crossing_stats_1e7.txt): - The hypothesis Y_e ≥ 2^(m+1) occurs only 3 times: epochs 9, 16 and 350,275. - Each of these is the epoch right after an exact-power pair. - Their C-margins are 3, 3 and 15. C never fails.

Conjecture C0: 2^zb(Y_e) ≤ N_e, or Y_e = 2^bitlen(N_e). - It implies C and holds at all 1e7 epochs. - It is not inductive on its own (c0test.py). Over 2 seeds, 5 epochs per start: - from 6,000 perturbed reachable states, C0 broke 3 times; - from 6,000 tuned near-crossing states, C0 broke 7 times, and one start became unsafe.

Half of a proof: - Right after an exact-power epoch with s = 0, Y_{e+1} = 2^(m+1) + (N_e − v_e + 1). - C(e+1) then needs only popcount(N_e − v_e + 1) ≥ 2 − s_{e+1}. - Missing: that big Y arises only there. Concretely, a bound on the j weight at depth ≥ m − 1: J_e ≤ 2^m unless epoch e−1 had Y = 2^m. This is the crossing lemma in its smallest form, now about a rare event rather than about every epoch.

Joint with R2 (details in R2's notes.md, "Joint crossing stage (from R3, 2026-10-10)")

• R2's R1 was not proven, and R2's status is unchanged.
• Candidates that may transfer, untested on R2:
• The "eat shift buys one bit" step of Lemma S. R2's Lemma B already has gap − 1 at an even eat.
• The exact-power pair, which is R2's special case V* = 2^m.
• Running an integer epoch model past N = 2^23. R3's minimum margin first appeared at N ≈ 2^22, after 3.5e5 epochs.

Still open: - the Big-Y lemma (or C0); - step counts per macro rule; - the Rocq model, which has not started.

Decision (2026-10-11)

Question: The crossing stage hit its stop rule (Lemma S proven, the Big-Y lemma open, with 3 instances in 1e7 epochs): park R3 with R2, fund one Big-Y stage, or start Rocq with Big-Y as the one hypothesis? Answer: park (Park R3 with R2 (stop rule)). Dennis: go with recommendations (2026-10-11).