1RB1RF_1LC1RE_---0LD_1LE0LD_1RA0RF_0RE0LB

Status: CHECKPOINT_A Class guess (agent / Dennis): Bell eats counter (left unary "bell" pair + right binary counter; reset absorbs counter digits) / _ Spreadsheet notes / Discord thread: Results tab row 1043 = "Bell eats counter", status/notes/sources/done-by blank; no hyperlink, no strikethrough, no xlsx comment; not in dyuan01's 24 or mxdys's UBRRBA 86. Nobody on it. Viewer: https://bbchallenge.org/1RB1RF_1LC1RE_---0LD_1LE0LD_1RA0RF_0RE0LB

Observation

• 1e9 steps (C core): no halt; span 5,210 cells, 2,940 nonzeros; L ~ t^0.35 (L = 83 at 1.8e5, 1,717 at 1e9).
• qsim (block 3, 200k loops): 0 prover rules (chain moves only). rulefit: see open issues (tests fail; fit is junk, 7% coverage).
• Trip-level skeleton (C turning left at the right end): G(a,n,Q) = 0^inf (110)^a 0 (011)^n <C Q 0^inf, Q = counter word.
• One phase (img/phase_trips.png): the a|n boundary walks right one block per trip; Q is a binary counter (3-cell digits, 000 = 0, 001 = 1, LSB next to the head) that increments every second trip.
• Reset (img/reset_zoom.png) when n reaches 1 or 2: two full-width sweeps, a restarts at 2, L = a+n grows by dL.
• How the two zoom diagrams were made (both start mid-run from the natural configuration, saved with Config.dh(trim=False)):
• phase_trips.png: tools/diagram.py "$TM" --from-config @img/phase_start_step152677.txt --mode state:B:R --steps 40000 --scale 2. Rows = entries into B moving right: one per trip, plus 1–4 rows a few steps apart while the counter carries. The reset falls between rows 162 and 163.
• reset_zoom.png: --from-config @img/reset_start_step180953.txt --mode every:2 --steps 1700 --scale 2.
• Both show cells −46..240 / −46..230 at 2 px per cell. Every card diagram's labels are in observe.json → diagrams.
• phase_every32.png (every 32 steps from step 152,677) is no longer on the card: at that sampling each sweep shows as a near-horizontal streak that looks like tape structure.
• Record-aligned (B right records): 0^inf (110)^a 0 (011)^n 1 W B> 0^inf; a = 2^k - 1 at each record (counter overflow), L constant within a phase, W tail y^q x gains one y per record (x = 110, y = 111).

Candidate rules (all tested by direct simulation from concrete configs)

D(c) = c in binary, LSB first, digit 1 = 001, 0 = 000 (top digit 1). nu(c) = number of trailing 1-bits. - T (trip pair, clean Q): 0^inf (110)^(2c) 0 (011)^(n+3) <C 1010010 D(c) 0^inf --> 0^inf (110)^(2c+2) 0 (011)^(n+1) <C 1010010 D(c+1) 0^inf, steps 16n + 6 nu(c) + 62 (exact fit). 66/66 random (c up to 2,000, every residue mod 8, n up to 1,500) + 65/65 small-n probes (n+3 = 3..7). n+3 < 3 fails 0/39 (that is the reset boundary). - T' (any natural Q): G(a, n+3, Q) --> G(a+2, n+1, inc(Q)), steps 16n + K(Q). Q/inc(Q) from 15 natural trip pairs at 3e8, 6e8, 9e8; a, n random: 60/60. So the left pair (a,n) and the counter word Q are decoupled. - R (reset, clean Q): G(2c, n, 1010010 D(c)), n in {1,2} --> G(2, L+dL-2, Q'), L = 2c+n; dL = 1 if n = 2; n = 1: dL = 4 (c even), 5 (c = 3 mod 4), 6 + nu(c>>2) (c = 1 mod 4). 48/48 (each residue mod 8, c up to ~2,000, n = 1 and 2), 0 halts. Natural orbit to 1e9 (277 phases): dL = 1 whenever L is even (98/98); L odd gives dL from 2 to 25 (remnant digits in Q get eaten too). - R' (reset depends only on (n,Q)): natural reset configs after 3e8 and 6e8 (both n = 2) with a replaced by 6 values each: same Q' and same dL (12/12). - Killed: "B-record doubling" P(a,m,W) --> P(2a+1, m-a-1, W y) for arbitrary W: 3/65. The right word is not passive.

Template check

• IndBECv1.v Others.nonhalt7 = 1LB1LF_1RC1LB_---0RD_1RE0RD_1LA0LF_0LE0RB (mirror of 1RB1RF_1LC1RB_...): 1 transition away (B1: ours 1RE, theirs 1RB). Its certificate config_BEC 1000 3 B D [1] [0] [1] uses ex-rule r 1 B> 1^n 0 l --> r <D 0^(n+1) 1 l (our orientation): 24/24 on the template, 2/24 on ours (only n = 0). Certificate does not carry over; the decider method might, with a 3-cell-digit ex-rule.
• BECv7.v TM1 (1RB1RE_1LC1RD_1LD0LC_1RA0LF_1RE0RA_---0LE) is 5 transitions away; its shape (binary tail digits + canonical invariant + progress_nonhalt_cond) matches our mechanism.

Checkpoint A (Dennis)

(pending)

Informal proof

(not started; waits for Checkpoint A)

Formalization log

(not started)

Outcome

(open)

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/phase_trips.png, Fig 2 = img/reset_zoom.png, Fig 3 = img/state_auto_1e6.png, Fig 4 = img/blaze_1e7.png, Fig 5 = img/default_1e4.png (Figs 1-3 primary). - Mechanism, full observer version: - Tape = 0^inf (110)^a 0 (011)^n, then a binary counter word Q at the right end - One trip: zig-zag from the right end to the a|n boundary and back; a+1, n-1 - Every 2nd trip Q increments (3-cell digits: 000=0, 001=1, LSB nearest the head) - At n=1 or 2: reset = two full sweeps; a restarts at 2, L=a+n grows by dL (1 if L even; 2-25 seen if L odd) - Left pair and counter are decoupled: trips ignore Q, reset ignores a - Checkpoint questions before the rewrite (some were decisions, not questions about a figure): - phase_trips: is the right-walking black diagonal the a|n boundary, with the counter ticking at the right edge? - reset_zoom: OK to prove the reset as one lemma split on n in {1,2} and the counter's low bits? - Try the IndBECv1 decider (config_BEC sweep, mirrored TM) before a hand-written BECv7-style proof?

Deepen pass (overnight 2026-10-10)

Verdict: confidence stays med; recommend more_observation (not cryptid). The trip-level dynamics are now exact and cover the whole run. One quantitative race decides halting and is still open: re-alignment must finish before the next reset. Scripts are in scripts/: - tm15.py: simulator and helpers. - gdump.c: C dump of every G config. Build with gcc -O2 -o gdump scripts/gdump.c; run gdump MAXSTEPS. - validate_deepen.py, abstract_orbit.py, abstract_long.py, phase_race.py, closure_test.py, counter_vs_L.py.

Counter = digit list (closes "Q language" for the aligned case)

• Q (the cells right of the bell) is a list of digits b 0 (100)^m 0, LSB first, with bit b and length m >= 0. The 0^inf tail counts as [0,0] digits.
• In 3-cell blocks: bits sit at cell 0, the m-track 1^m1 0 1^m2 0 ... sits at cell 2, and cell 1 is always 0.
• The earlier encodings are special cases: 001/000 digits = [b,0]; 101 (001)^k 000 = [1,k+1]; the 1010010 D(c) prefix.
• LP(a,n) = 0^inf (110)^a 0 (011)^n. G = LP followed by <C on its last cell.
• <D arriving on that last cell behaves the same as <C (one step later both are in D). That is why only every other trip showed up as a G event.

Exact rules (checked against the full tape, head and state; random a up to 400, n up to 300, up to 25 digits, m up to 40)

• T1 (one trip, n>=2): LP(a,n) <C word(D) -> LP(a+1,n-1) <X word(inc D), head on the same cell. X = C with no carry, D with a carry. 860/860.
• The bell sweep only touches (011)^n and the a|n boundary. The right sweep enters Q as B>.
• On Q, 1-digits are marked (b0(100)^m0 -> 11(101)^m1) and the first 0-bit is set. The left sweep restores the marked digits to 0-digits.
• RI (n=1, D = [1,0]^j [1,m] R, m>=1): -> LP(a+2+j, m) <X word(inc R). dL = 1+j+m. 860/860.
• The A-sweep turns each [1,0] into a 101 bell block. It turns [1,m] into the separator plus (011)^m, then carries on into R.
• RII (n=1, D = [1,0]^j [0,m] R): -> G(0, a+2+j, 1 (100)^m 0 word(R)). dL = 1+j. 860/860.
• A writes the 0-bit and B turns at the digit's cell 1, so the bell becomes (011)^(a+2+j) in an alignment shifted by one cell.
• The new Q is the old word seen one cell later: a "shifted" word.
• These three rules account for the earlier observations:
• The odd-a G configs are RI sub-phases.
• "dL = 1 if L even" is RII with j = 0.
• The 2-25 spread for odd L is RI with dL = 1+j+m.

Regime map: validated on the whole run

• abstract_orbit.py (T1/RI/RII, plus direct sub-simulation of only the Q region for shifted words) reproduces the direct run exactly:
• every G config to 1e8: 24,605/24,605;
• every G config to 1e9: 111,287/111,287. That is 222,436 trips: 219,707 T1, 2,223 transient, 229 RI and 277 RII. Final L=1717, a=1140, n=577, matching the run.
• Language: all 111,287 natural Q are either aligned digits (DIG = ([01]0(100)*0)*) or DIG followed by one shifted word SH = [01](100)*0 DIG. In blocks, SH is the 010/001 "t-blocks".
• One processing pass maps DIG.SH into DIG.SH: 100,000/100,000 random words, exits only C or D, no halts.
• Counter invariant: V = sum b_i 2^i equals a+1 on 99.3% of aligned trips (1e6 trips). The exceptions are RI sub-phases, where V = a - const.
• At all 2,042 resets to 4e6 trips, V/L is 1 or 1/2, and the digit count is at most log2 L + 1.

Open gap: the re-alignment race (load-bearing)

• After RII, the shifted part is converted to aligned digits only when the counter's carry reaches it. That happens once the low aligned digits are all 1, so the lag is a power of 2.
• A reset that meets a still-shifted Q leaves the language and can halt. Example: 0^inf 0 011 <C 11001000001000000001000101 0^inf halts at step 44 (tools/sim.py, C reads 0). 3/300 random aligned+shifted resets halted.
• Measured, abstract orbit to 2.35e7 trips (L = 19,760, about 1e12 step-equivalents):
• 2,494 RII phases, never a reset on a shifted Q;
• lag = 2^k trips, at most 1024; distribution 1:63, 2:209, 4:367, 8:379, 16:301, 32:165, 64:84, 128:55, 256:18, 512:5, 1024:2;
• worst lag/L = 0.119 (L >= 200) against a deadline of about L trips.
• The transient pass has no closed form yet. It depends on the bits and on m mod 3: see the enumeration via closure_test.py/qproc in tm15.py.
• Proposed proof route: 1. Derive the pass rule. 2. Show the re-aligned digit count is at most floor(log2 L')+1. 3. With V = a+1, a digit at position p is re-aligned when V first reaches 2^p, and the phase ends at V = L, so re-alignment finishes in time.
• If step 2 instead needs parity-like facts about the counter, re-flag as a cryptid candidate.
• Not a cryptid as far as seen: the halting-relevant quantity follows the exact invariant V = a+1. No pseudo-random branching has been identified.

Deepen pass 2

Verdict: CRYPTID_CANDIDATE; confidence med; recommend cryptid (stop-or-continue call for Dennis). - The round-1 gap is closed: the re-alignment transient has an exact closed form (PROC), and the whole orbit now runs on validated closed-form rules. - Halting reduces to one arithmetic race. - A sufficient invariant wins it. That invariant survives every phase type except a rare "overflow" phase near L ≈ 2^k. - After an overflow, whether the race is won depends on the bits and widths left by earlier phases. - The closest natural race missed by 0.9998 bits, at L' = 4,193,612 = 2^22 - 692.

New scripts in scripts/: - procrule.py: the PROC rule and the realignment test. - fast_orbit.py: phase-level orbit. - compare_fast.py: fast orbit vs the trip-level orbit. - race_scan.py: race margins. - nearmiss_check.py: cell-level replay of the closest race. - invariant_scan.py: the invariant and where it breaks. - raceloss_reentry.py: what a lost race does.

Notation

• Digit (b,w) = b 0 (100)^w 0 (bit b, width w; 3w+3 cells), LSB first.
• Junction J(m) = 1 (100)^m 0 (3m+2 cells). This is RII's output: RII leaves G(0, a+2+j, J(m) word(R)), where R is the old digits above d_j, one cell out of phase.
• During a junction phase Q = word(A) J(m) word(R). A is the new aligned prefix; R holds the old digits.

Junction rule PROC (closes "re-alignment transient: no closed form")

• A trip increments A as in T1. When A is all ones, the carry enters J and PROC fires:
• PROC(m, R): R := R + m (m binary increments; widths stay with their positions; new digits have width 0); then ARR(R).
• ARR(d:R): if d = (0,w), stop. d becomes the new junction J(w), starting one cell after d's bit cell. If d = (1,w), run PROC(w, R); so (1,0) is simply passed. ARR([]) acts as d = (0,0).
• Output: A is zeroed, then comes ONE new aligned digit (0,x), with x = m + Σ(w+1) over the passed digits. Then J(w), then the rest of R. Exit state D.
• Mechanism at the cell level:
• The m blocks of J are a unary counter. Each B-arrival at R's first cell is one ordinary B> sweep in the old frame (R+1); the head bounces inside J, moving the hole one block per sweep.
• After m sweeps, A arrives at R's first cell instead of B.
• An A arriving on a 1-digit (1,w) gives cells identical to B entering J(w) (A1→1RF, F0→0RE versus B1→1RE, E1→0RF). That is why the rule recurses.
• Validation: procrule.py seeds 1-5 gave 11,500/11,500 exact on the full Q cells plus exit state D, by direct simulation of the Q region (tm15.qproc). Inputs: an all-ones prefix A of up to 6 digits, m up to 40, up to 12 old digits with widths up to 15.
• Realignment criterion: J(m) word(R) is aligned iff m = 0 and every old digit up to the top nonzero one has width 0. Checked against parse_digits: 200,000/200,000 (procrule.py 7 200000 --realign).
• Then the old 1-runs become widths. Each old 0-bit opens a new aligned digit (0, run of 1s above it); the first new digit is (1, run0).

Phase-level orbit (closes "whole regime map" beyond 1e9 steps)

• fast_orbit.py covers whole phases with closed forms only:
• T1: k trips = D + k, widths kept.
• Junction phase: the next PROC fires after 2^|A| - val(A) trips.
• RI: a,n := a+2+j, m; D := inc R.
• RII: a,n := 0, a+2+j; junction (m, R).
• It flags RACE_LOST if a reset sees a junction.
• compare_fast.py 2.4e7: 4,871/4,871 pre-reset configurations exact (a and the full Q cells) against the trip-level orbit (abstract_orbit.step, which matches direct simulation for all 111,287 G configs to 1e9). Final L = 19,965.
• Runs 1e7 phases (L = 68,590,476, about 26 octaves) in 4.5 min: 5,078,277 RI and 4,921,723 RII phases, no race lost.
• Correction to round 1: "V/L is 1 or 1/2 at resets" only held for small L. Chains of RI phases halve V each time, and V/L = 1/32 is seen at L ≈ 1.1e6.
• V = L exactly after every junction phase (496,376/496,376 to 1e6 phases), and V <= L at every reset (1e6/1e6).

The race, made exact

• Lemma B (timing). PROC pass i fires on trip 2^i - 1 of the junction phase, because A has i-1 zero digits before pass i. Re-alignment after P passes therefore needs 2^P <= L' = L+1+j. RACE_LOST means 2^P > L'.
• Lemma A (from PROC plus the criterion). Let W = 1 + the position of the highest digit of width >= 1 above j. Then P <= max(1, W - j).
• Reason: each pass consumes at least one digit. The first stop above the highest wide digit leaves J(0) with all remaining widths 0, and that is aligned.
• 0 violations in 4,921,722 junction phases (invariant_scan.py 1e7).
• Invariant Inv: W(D) <= bitlen(L) - 1, checked at resets. With Lemma A it gives 2^P <= 2^(bitlen L - 1) <= L < L', so the race is won. Preservation:
• T1: W is fixed and L is unchanged. RI: W drops by j+1 and L grows. OK.
• Junction phase in which no PROC addition carries past the top of R ("no overflow"):
  • The realigned D is P aligned digits plus 1 + zeros(R_final) tail digits. Each pass consumed at least one digit of R.
  • So W' <= |R| = max(W, bitlen V) - j - 1 <= bitlen(L) - 1 <= bitlen(L') - 1, using V <= L, which always holds. OK.
• Junction phase with an overflow: W' can reach |R| + (number of appended digits), which can break Inv.
  • An overflow needs the rest of R to be all ones when the junction reaches it. So it happens only when V's top bits are a long run of ones, near L ≈ 2^k.
  • Overflow phases cluster at octave crossings: 4,303 of 4,921,722 junction phases to 1e7 phases, none between L = 1.9e7 and 2.6e7.
• If overflows never broke Inv, non-halting would follow by induction from the start config, given cell-level proofs of T1, PROC, RI and RII. The open part is therefore only the aftermath of overflows.
• invariant_scan.py results:
• Inv is violated at 3 of 1e7 resets: RI at L = 11, RI at L = 4,193,607, and RII at L = 4,193,612. All 3 came right after an overflow phase, and only 1 was at an RII.
• That one RII is at L' = 4,193,613: W = 22 = bitlen(L'), j = 0. The race was still won, with P = 6 against the bound 22, because the junction passed the top run of ones in one ARR without carrying.

Closest race (load-bearing near miss)

• Phase 703,380: RII at L = 4,193,611 (L' = 2^22 - 692). V = (L+1)/2, j = 0, J width 15. Widths [15,3,0,11,0,0,1,0×13,1]: the top digit (position 20) has width 1.
• Pass 7 adds 1 to a remaining R of 13 ones, which overflows into 13 zeros. Each zero then costs one pass, and the width-1 top digit forces the junction all the way up: P = 21, re-alignment on trip 2,097,151 of 4,193,611.
• Margin log2 L' - P = 0.9998 bits. nearmiss_check.py replays all 21 passes at the cell level, exact.
• That phase leaves Inv broken: W = 22 at L' = 4,193,612 (above).
• A loss would need the next junction to stop just below the top run of ones on a digit of width >= 1. Here that digit (position 9) had width x = 0, because the passes through the overflow zeros all have x = 0. Whether that protection always holds is open.
• Margin per octave (race_scan.py 1e7):
• The minimum is 2.3-5.6 bits in every octave from 2^8 to 2^26 except 2^21 (0.9998).
• The P distribution creeps up about 0.25 per octave, and its upper tail falls about 3x per extra pass.
• Synthetic Inv-violating V = L configs (L = 2^k - s, wide top digit, random low widths): 1 race lost in 38,136 (k = 22, 30, 40). So even after a broken Inv, a loss needs a second coincidence.

What a lost race does

• The race is never lost naturally to L = 6.9e7, so these runs force one by stopping the closest race early.
• raceloss_reentry.py stops the closest race after k passes and resets with a small bell:
• 21/21 configs ran 3e6 steps without halting. Each had a few OUT G configs and then returned to DIG/ALS.
• A wider sample from the same phase had 4/388 halt within 2e6 steps, after 208, 208, 815 and 29,740 steps. Round 1 found 3/300.
• So halting needs a lost race (very rare) that is also a fatal one (a minority).

Why cryptid

• The rules are now complete and exact. The halting question reduces to whether a rare arithmetic coincidence ever happens at some octave crossing L ≈ 2^k: 1. an overflow junction breaks Inv; 2. at the next RII (V = L, j = 0) a carry runs through the top run of ones before the junction passes it; 3. the resulting lost race is fatal.
• Steps 1-2 depend on the widths x = m + Σ(w+1) and on low bits that build up over the whole history. No conserved quantity was found that controls them. That is the pseudo-random arithmetic of the cryptid protocol.
• Heuristically the per-octave loss chance is about 1e-5 and the fatal fraction is a few percent. Whether that chance shrinks with k decides "probviously non-halting" versus "halts astronomically late"; it is not settled.
• Route if Dennis says continue:
• Prove the overflow-aftermath lemma. After an overflow junction, the overflow zeros come back as x = 0 widths. Show that the next junction cannot carry into the top run before passing it, or that RI phases restore Inv first.
• The data supports it (1/1 natural case), but the argument must survive RI shifts and increments between the phases.
• Everything else (T1, PROC, RI, RII, realignment, Lemmas A and B, Inv preservation without overflow) is ready for proof.md.