1RB1RF_1RC0RA_1LD1RE_1LE0LE_0RA0LD_0RB---

Status: CHECKPOINT_A Class guess (agent / Dennis): Bell eats counter, BMO 7 layout with a base-3 counter (med) / _ Spreadsheet notes / Discord thread: Results row 1037: status blank, "Bell eats counter", no notes, link, comment or strikethrough. Not in the UBRRBA or dyuan01 lists. Absent from solved_index. Pilot rank #18. Viewer: https://bbchallenge.org/1RB1RF_1RC0RA_1LD1RE_1LE0LE_0RA0LD_0RB---

Observation

• 1e9 steps: no halt; span -312..4272 (4,585 cells), 2,285 nonzeros. Bell M ~ t^0.342; 312 phases.
• Most telling: img/state_C_one_phase_x2.png (one phase; marker diagonal + ticking counter strip), img/counter_from_zero.png.
• How each card diagram was made (re-run 2026-10-10: byte-identical PNGs; label fields in observe.json come from these runs). All via tools/diagram.py "$TM":
• state_C_one_phase_x2.png: --mode state:C --steps 158600 --from-config @work/phase_2097352.cfg --max-width 300. That cfg is the real tape at step 2,097,352 (checked), a phase start. --max-width 300 makes the tool draw only every 2nd cell ("x2"), which turns the bell (10)^M solid white or black and so shows the marker as the diagonal edge.
• counter_from_zero.png: --mode state:C --steps 21000 --from-config "0^inf A> (10)^100 00101001 0^inf" --width 28 --ox -7.02 --scale 5 (window = cells 197..224, the bell's right end + the counter; constructed, counter X(0) = value 0).
• phase_starts_counter_1e9.png: --mode records:L --frame right --width 110 --steps 1e9 --scale 3 (one row per left record = phase start, 313 rows).
• records_1e8.png: --mode records --steps 1e8. blaze_1e8.png: --mode blaze --steps 1e8 --as-site.
• Phase start: 0^inf A> (10)^M W 0^inf. The marker (a 00/01 phase boundary) moves right 1 block per bounce, and each bounce adds 1 to W.
• W as domain walls (cells where neighbours are equal): 1, d0, w0-d0, d1, w1-d1, ..., i.e. frames (d_i in 1..3, even width w_i >= 4). Inc = base 3 on the d's; widths never change in Inc.
• Eat: when the marker reaches W, the bell grows by g(W) >= 2 and W is rebuilt (W'). g and W' are independent of M. Per-phase dM: 1 in ~half of phases, else 4..38 (last 150 phases).
• History at phase starts: observe.json history (39 rows).
• Tools: rulefit gets 19% coverage (right-edge records only); sligocki prover gets 0 rules at block size 2; compress gives 244 skeletons out of 300 snapshots. None of them sees the wall counter, so the analysis is by hand (work/*.py).

Candidate rules

All were checked by direct simulation (tools/sim) from concrete configurations: work/validate.py, work/validate_phase.py. | rule | from -> to | tested | |---|---|---| | sweep chains | A> (10)^n -> 10 (01)^(n-1) B>, B> (10)^n -> (01)^n B>, (10)^n <D -> <D (01)^n, A> (01)^n -> (10)^n A> (2n steps) | 240/240 | | Inc, X form | 0^inf (10)^a A> (10)^(b+1) X(v) -> 0^inf (10)^(a+1) A> (10)^b X(v+1), b>=1; X(v)=D(v%3) 1 T(v/3) 001, D=0010/0110/0100, T=bijective base 3, 1/2/3=0001/0011/0010 | 450/450 | | Inc, frames | same with any frame list F -> inc(F) | 400/400 | | Phase | 0^inf A> (10)^M X(v) -> 0^inf (10)^(M-1) A> 10 X(v+M-1) | 40/40 | | Eat | 0^inf (10)^N A> 10 F -> 0^inf <E (10)^(N+g(F)) F', with g, F' independent of N | 60/60 | OPEN: a closed description of the Eat step. Its outputs include transient "pending" shapes (e.g. walls 1,1,1,3) that Inc then merges into new frames.

Template check (BMO7.v; diff C1 1RC -> 1RE): partly. LIncs (left bounce) holds 36/36; RInc (binary) fails on every odd counter (16/40 pass); the S1 big-step shape is reached 3/8 times, and then with a non-binary counter.

Checkpoint A (Dennis)

Informal proof

(not started)

Formalization log

Outcome

Card data pass (2026-10-10)

The card now shows at most 3 short mechanism bullets and yes/no questions that point at figures by number (primary figures first). The text they replaced is kept here. - Figure order on the card: Fig 1 = img/state_C_one_phase_x2.png, Fig 2 = img/counter_from_zero.png, Fig 3 = img/phase_starts_counter_1e9.png, Fig 4 = img/records_1e8.png, Fig 5 = img/blaze_1e8.png (Figs 1-3 primary). - Mechanism, full observer version: - Tape = long 10-sea (the bell) + short counter at its right end. - A marker walks right through the bell one block per bounce; each bounce adds 1 to the counter. - Counter is base 3: each digit is a wall at offset 1/2/3 inside its own frame; overflow appends a digit. - When the marker hits the counter, the bell eats its low end: bell grows by g>=2, counter is rebuilt. - g and the rebuilt counter depend only on the counter, not on bell size; bell ~ t^0.34. - Checkpoint questions before the rewrite (some were decisions, not questions about a figure): - state_C_one_phase_x2.png: is the black/white diagonal the bell's marker, with the right strip the counter? - counter_from_zero.png: do you read the ruler pattern as a base-3 counter (staircase = new digit)? - phase_starts_counter_1e9.png looks irregular: spend the next stage closing the eat step before any Rocq?

Deepen pass (overnight 2026-10-10)

Result: confidence med, recommend more_observation (not cryptid). The eat step is now closed for aligned counters. The next-phase "shifted" frames are explained, but their Inc and crossing rules are still open, and no closed invariant has been found yet. Full record: deepen.json; scripts: scripts/deepen_*.

What the eat is. It is not a separate rebuild. The marker keeps walking right through the counter, one bounce at a time, and each bounce increments the frames to the right of the marker's current S-run. So while the marker crosses frame j, frame j+1 is the low digit. The phase ends at the first frame that has digit 2 when the marker reaches it, or at the counter's end. g and the new counter don't depend on N because the walk only reads the counter.

Notation: 2-cell blocks aligned with the bell: S=10, Z=01, o=00, #=11. An aligned frame (d,e) is d=1 o S^(e+1), d=2 Z S^(e+1) or d=3 Z o S^e (width 2e+4); the terminator is Z. L is any word over {S,#}; sweep maps S->Z and #->o.

Tests: scripts/deepen_validate_walk.py with seed 1 (300 instances) and seed 2 (1000 instances). The left part L includes # walls, and e goes up to 40. As a mutation check, changing C1a or C2 by one block makes those rules fail 1000/1000.

The walk. R := inc^(M-1)(F), then frame by frame: - d=2: C2 ends the phase. - terminator: T ends the phase. - d=1: the frame is absorbed into the bell, then e_j more incs go to the rest. - d=3 with e_j>=1: a # is left behind, and the rest gets e_j incs (1 from C3a, then e_j-1 bounces).

Every branch is non-halting whatever the digits. Test: 3000/3000 random aligned counters ran 8 phases with no halt (scripts/deepen_xrand.c, scripts/deepen_randctr.py aligned).

Next phase. The new phase starts 2 steps after the left record. Its tape is read one cell shifted, so every untouched frame looks different:

This explains the Z-runs and the "pending" shapes such as 1,1,1,3.

Phase starts to 1e11 (scripts/deepen_phases_1e11.txt): no halt, 1324 phases, span -1324..20540, M=10902. They fall into three shapes: - 1071 have the shape (o S+)* (o Z*) (shifted frame)* o S (a C2 end). - 102 are aligned frames + Z (a T end). - 61 have a third junction shape, o S2 Z followed by #, Z or S; it is not derived yet.

Junction invariant: o S (one S) never sits directly before an empty junction (0 of 1324 phase starts). The reason is that C3b always leaves # S A>. Random counters that break this halt 37 of 3000 times.

Open (why not high): 1. Inc on shifted frames (renormalisation) has no closed rule. Example: o Z o Z o Z o S -> Z2 o Z o Z o S -> o S6 o S2 Z. 2. The marker crossing shifted frames, or landing directly on a token (after a width-4 digit-3 frame), is not tabulated. 3. The third junction shape is not derived. 4. There is no closed invariant. Random counters that fit the grammar still halt 19 of 9000 times, all with small odd M (up to about 37); for larger M the same counters run on. So the invariant must tie the shape to M, e.g. M at least the capacity of the aligned low part. The orbit has the risky shape (empty junction + shifted width-4 digit-3 frame) 37 times, 23 of them with odd M, always with M in the hundreds or more.

Not cryptid: in these tests halting needs M small next to the counter, not digit coincidences. That still has to be proven.

Next stage: - Close gaps 1-2 with the same block-level method using the block-level micro-rules below (derived by hand from the table and checked against traces). - Moving right, head on the block's left cell: - B> S -> Z B> - B> Z -> # E> - B> o: turn; the block becomes Z; go left in L1 mode - B> #: write o, then F reads the next block's left cell; if that cell is 1, HALT - E> o -> Z B> - E> S: turn; the block becomes o; go left in L2 mode - E> #: turn; the block becomes Z; go left in L2 mode - E> Z: F reads the next block's left cell; if that cell is 1, HALT - L1 (E reads the right cell): Z -> S and # -> o, keep going; stop on S or o, and A> starts on the block to the right. - L2 (D reads the right cell): - S -> Z and # -> o, keep going. - On Z, a B> restart on the block to the right. - On o: the block becomes Z, then F reads the next block; if that is 1, HALT. - At the left edge, the phase ends. - Then state an invariant grammar with an M-vs-capacity condition, and check closure by random phases. - The BMO7 template is not enough: the walk is recursive and spans several phases.

Deepen pass 2

Result: confidence med, recommend more_observation (not cryptid; one quantitative question is flagged below). Round 2 closes gaps 1-3: every Inc, marker crossing and sub-phase from phase 3 to step 1e11 (1321 phases) now falls under a validated rule. Phases 0-2 are just the first 41 steps. Gap 4 (the invariant) is now one inequality between M and the counter. It holds on the orbit, but in its simple form it does not carry over from one phase to the next. Full record: deepen.json. Scripts: scripts/deepen2_*.

New view: walls instead of blocks. A wall is a cell k with c[k-1] == c[k]. The bell (10)^M has no walls, and the zero tail has a wall at every cell. Write the counter C (the cells after the bell, starting on an even cell) as wall offsets 0 = p0 < p1 < p2 < ... . This view does not depend on the grid, so the "shifted" frames from round 1 are just frames that start at odd offsets. Aligned frame (d,e) = walls at 0 and d, next frame at 2e+4. The terminator Z is the frame (3, width 4) followed by the tail, and the tail itself is an endless run of width-2 frames o.

Rules (all checked by direct simulation from random concrete instances).

What the J-rule means: a junction is a sub-bell for the counter W to its right, which lives on the other grid. The first carry into it runs one complete phase of the same machine on (j-1, W), and the sub-bell comes back as the aligned d=1 frame o S^M', followed by the sub-phase's new counter. This is the "renormalisation" from round 1. For j=1 the J-rule is the ordinary d=3 carry. The "third junction shape" (Z # = walls 0,2,3, then an even run) is a narrow frame: one Gap-Inc merges it into a junction with odd p1, and the J-rule takes over.

Orbit replay (scripts/deepen2_orbit.py). The replay runs each phase at bounce level with the bell removed (Inc does not depend on the bell size). It reproduces all 1321 logged phase starts to 1e11 exactly. Every J bounce matches the J-rule (1702/1702); sub-phases are checked recursively. Kinds of Inc seen: Gap-Inc (p1 = 1 or 2, including the merges o o, o Z, o #, Z #), the J-rule (junction j = 1..34), and the tail. Marker crossings seen: d1, d2, d3 and T only; the marker never met a junction. Sub-phases use only the aligned rules.

Invariant, as far as it goes (scripts/deepen2_inv.py, deepen2_validate_closure.py). - A (aligned): every frame is wide, i.e. p1 in {1,2,3} and p2 even >= 4, all the way to the tail. - G1: either A, or (wide aligned prefix) X W. Here X is a junction head and W, read from where the head ends, is in A. X is one of: a narrow frame (p2 <= 3) with p3 odd; p1 odd >= 5; or p1 = 3 with p2 odd. - All 1324 orbit phase starts are in G1: 1149 have a narrow o head, 129 are A, and 46 have other heads.

Open (why not high): a proof needs a margin lemma: M-1 >= k_align(C) at every phase start. With it, the chain is: G1 start, then the Incs give A (Gap-Inc, plus J-rule sub-phases on aligned W, which are non-halting by the aligned walk), then the round-1 walk gives a G1 start. k_align is about 2·3^(h_total), where h_total counts the d=1 prefix frames, which come from # walls, along the chain of J outputs. On the orbit h (the # walls) is small: mean 1.0-1.2, max 6, while log3 M grows to 8.4. Also, max 3^h/M drops from 0.58 to 0.008 across the windows. Crude heuristic: each crossed digit is 2 (which stops the walk) with probability 1/3, so P(h >= k) ~ 2^-k. If digits behaved randomly, margin violations would be rare but not summable (about sum M^-0.63). This is the only place where something like pseudo-random arithmetic could enter, and mild violations look harmless (0/1100 halts with M in [3k/4, k]).

Priority question for Dennis: should the next stage try to prove the margin lemma (a structural bound on k_align via the J chain), or park the machine as a probable cryptid-margin case?

Next stage: 1. Prove the aligned-walk lemma: Phase(m, A) is non-halting and lands in G1. It uses only the round-1 rules plus aligned Inc, so it can be formalized now. 2. Bound k_align of the walk's output by the walk's own data: h = d=3 frames crossed, and the J chain set by the frames beyond the stop. Try to show M' - 1 >= k_align(C'), or find a reachable-looking counterexample. 3. If (2) fails, run a targeted search for margin violations: replay from the 1e11 state at bounce level, which is cheap. Then decide between cryptid and proof.

Correction to round 1: the micro-rule B> # writes Z, not o (B1 -> 0RA, A1 -> 1RF, then F reads the next block's left cell).

Decision (2026-10-10)

Question: Non-halting of #18 now reduces to the margin M-1 >= k_align(C) at every phase start. Fund one stage to prove it, or park #18 as a cryptid-margin case? Answer: prove_margin (Fund one ~2 h stage on the margin lemma). Dennis: go with all recommendations (2026-10-10).

Funded stage (2026-10-10, prove_margin)

Result: no margin proof; the bound failed, so #18 is parked as STUCK (a cryptid-margin suspect), per the stage's exit rule. - The strict margin M-1 >= k_align(C) is not provable from the counter's shape: random reachable-looking states break it. - It also depends on the exact bell. Changing a real orbit bell by 1 turns a next phase with k_align = 0 into one with k_align/(M'-1) = 0.979. - The orbit itself stays far from the edge: max ratio 0.467 up to M = 114,554, about 9.7e13 steps. - It is not flagged CRYPTID_CANDIDATE: no tested margin break has led to halting (0/400 runs), so it is not shown that the arithmetic decides halting.

Scripts and outputs: scripts/deepen3_*.

Fast phase map (scripts/deepen3_fast.py). This is round 2's bounce-level replay with one speed-up. On an aligned counter, the frames below the top frame count in bijective base 3: digits d in 1..3, with the widths fixed. So the remaining incs of a phase are added arithmetically. Three steps stay at cell level: the incs before the counter is aligned, the one inc that carries into the top frame, and the marker walk (deepen2_orbit.crossing). - Logged phase starts 3..1323: 1321/1321 reproduced exactly (21 s). - Direct check: a C simulation of one phase from a phase start (scripts/deepen3_onephase.c) agrees with the fast map on 40/40 random extended phases. These are phases 1323..3222, with M up to 27,680 (deepen3_onephase_check.txt). One phase takes 2.00·M² steps (2.0006 to 2.0043 over these 40).

Extended orbit (scripts/deepen3_extend.py -> deepen3_orbit_ext.txt): - Range: phases 1323..11798, M from 10,902 to 114,554. - About 9.7e13 steps. This is an estimate from 2.00·M² steps per phase, not a direct run. - No halt. The margin holds at all 10,475 new phase starts.

Ratio r = k_align/(M-1) per phase window (deepen3_tail.py -> deepen3_margin_windows.txt):

The worst ratio is not drifting toward 1, and the tail gets thinner as M grows.

What k_align counts (traced on the worst phases, 3535 and 1497): - Widths add up. The walk merges frames. Each # frame (D) of the next counter is the merger of one crossed d=3 frame and the d=1 frames after it, and its width is the sum of their widths. The d=1 frames before the first d=3 go into the bell: M' = M + 1 + (sum of w/2 over them). - The chain. Each junction in the next counter is resolved by a J-rule sub-phase. That sub-phase continues the old walk past a d=2 stop, with e-1 incs to the rest instead of e. The chain ends after the last d=2 digit of the post-inc counter: the digits above it are 1, so the last sub-walk runs to the top (T) and its output is aligned. - Cost. So k_align is the sum, over the chain's heads, of the 1-2 carries each head needs at its frame position q, each carry costing about 3^q incs. - Phase 3535: heads at positions 4, 6, 7, 7 and 8; k_align = 11,097 with M = 30,990. - Phase 1497: heads at 4, 4, 5, 5, 6, 6 and 7; k_align = 4,293. - After the chain. Once the chain has resolved, every digit of the aligned counter is 1. So the next post-inc counter is the base-3 expansion of x = M-1-k_align, written on that counter's frame widths.

The margin depends on the exact bell (the low base-3 digits of M-1-k_align). Orbit phase starts C_t were run for one phase with a changed bell:

The two near-misses in the ± 30 row: - Phase 10666 (M = 102,052) with a bell one smaller (102,051): the next start has k_align = 99,927 with M' = 102,052, ratio 0.979. On the orbit, the same phase gives M' = 102,077 with k_align = 0. - Phase 1675 (M = 14,268) with bell 14,264: ratio 0.77. The orbit gives 0.257.

So which counter comes next, and how deep its junction chain is, turns on the low base-3 digits of the bell, as in round 2's digit picture. My guess that a zero-free x is the bad case was wrong (120/120 fine). The bad digit patterns are rarer and also depend on the frame widths.

The margin does not follow from the counter's coarse shape either. Random starts were given exactly the shape that chain resolution leaves: an aligned counter with every digit 1 and V_al <= M-1, random widths 4..160, and a random bell M0 in [100, 2e4] (deepen3_inductive_lib.py). - Margin, 12 phases each (deepen3_violate.py, seed 3): it fails in 7/200 runs, with k_align/(M-1) up to 2.84. Each failure lasted one phase, then the margin held again. 0/200 runs halt and 0/200 leave G1. - Inv(k_align <= (M-1)/2 and V_al <= M-1), 8 phases each (deepen3_inductive.py, seed 1): it fails in 60/300 runs, from the k part 17 times and the V part 43 times. - Same margin test with widths drawn from real orbit frames (seed 4, deepen3_violate_s4_orbitw.txt): it fails in 4/200 runs, with k_align/(M-1) up to 2.66. Each failure lasted one phase. 0/200 runs halt, and 1/200 leaves G1.

No bound written only in terms of M, k_align and V_al is inductive on these families. What keeps the orbit's margin is the exact arithmetic of its bells and widths, which we have no structural description of.

Open (why STUCK and not proof-ready, and why not CRYPTID_CANDIDATE): 1. The strict margin lemma fails as a lemma. Random reachable-looking counters break it, by factors up to 2.84, and a one-cell change of a real orbit bell brings it to 0.979. On the orbit it holds to M = 114,554 with max ratio 0.467, but that rests on the arithmetic of the bells, not on a structure we can state. 2. Breaking the margin has not led to halting. All 11 breaks seen this stage (7 + 4 runs) recovered within one phase. Halting has only been seen with deep deficits (round 2: 6 of 7 halts had M < k_align/3). - A violation-tolerant invariant (k_align <= c·(M-1), c near 3, plus a recovery argument) is conceivable. - It would face the same question, though: whether the digit arithmetic ever produces a deep deficit. - It would also need the walk on an unaligned counter to be covered by rules (J-crossing with j >= 2, never met on the orbit). 3. What stays valid for any later attempt: - the rule set (J-rule, Gap-Inc, J-crossing, round-1 walk rules); - G1; - the fast phase map (exact, checked 1321/1321 and 40/40); - the extended orbit file. 4. Ready but not run: deepen3_perturb_multi.py follows orbit counters with a changed bell for several phases off the orbit.

Parked. If #18 is ever reopened, start here: - Measure how far a deficit can grow: for broken starts, look at the largest k_align/(M-1) over many phases, and test Inv_c (k_align <= c·(M-1), G1) for c = 2, 3, 4 on the random families above. - Write rules for the walk on an unaligned counter.