/machines/1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB/notes.md · raw

1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom) Class guess (agent / Dennis): Sync bouncer counter, spread-digit variant (agent, med) / — Spreadsheet notes / Discord thread: Results row 918, "Sync bouncer counter", no status, notes, links or strikethrough; no xlsx comment. On mxdys's UBRRBA_TODO (2026-08-24); Dennis 2026-10-10: fair game. Viewer: https://bbchallenge.org/1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB

Observation

step a gaps
3.6e4 11 28
2.4e5 47 68, 28
2.8e6 203 260, 68, 28
5.6e8 799 7, 4097, 1028, 260, 68, 28

Candidate rules

Checkpoint A (Dennis)

Questions are in observe.json (checkpoint_questions).

Informal proof

proof.md (2026-10-10, informal_proof stage; revised after skeptic round 1); evidence check_proof.py (10 checks; log work/check_proof.full.log). - Token view: right of the lead, the tape is a word over 00, 01 and Z = 100. A digit is b Z 01 Z^g. - Window lemmas: 23 of them, each a finite run, so each holds in every context. - Inc_L is proved parametrically, by induction on the carry depth. - Every pause rule is a chain Inc_L, B1, Inc_L, END-type lemma. ENDZX is 22 steps; ZXP2 ends with BN. - Overflow = right sweep, then the tail window T(f), then the UE/UF alternation over the R block, then BN (N) or BS (S). - N/S is decided by the parity of σ(f) and q = 2r + H. - T(f) is context-free for every f ≠ 1^15: the end unit is never read. - ENDCARRY = CF1, then the L3/L3F alternation, then PEN/PFN. - Macro arithmetic: the closed forms S/P1/P1S/P3 are derived by hand, and the interval invariant is closed. - First configuration in X ∩ INV: step 92,299. - Open: the Rocq route for the 16,384-entry T(f) table (proof.md §9 step 5). - Skeptic round 1 (2026-10-10): sound, 6 minor gaps, all fixed (proof.md Review log). The fixes: - PFN restated as the 73-cell window P1 <F → <F F(010000100100101); - F(f) is 73 cells, not 75; - M ≥ 256 added to INV; - a three-way slot rule (PO iff cyc ≤ w−1, WX iff cyc ≥ w+1, cyc = w excluded); - lemma RB (R-block return) written out by induction on q, with TAILFRONT/L* closure derived from four finite T(f) facts (T1)–(T4); - new check 10, which tests whole paths by direct simulation from INV configurations (N = 8 exhaustive). - check_proof.py now has 10 checks.

Formalization log

Outcome

—

Card data pass (2026-10-10)

Deepen pass (overnight 2026-10-10)

Outcome: the overflow pause is now mapped. It is a nested "wall" process with seven local rules plus two overflow transitions, all validated by direct simulation. A macro model built from these rules reproduces the real history exactly from step 36,124 to 555,048,797. One component is still undecoded: the bounded right-end tail (79 cells ending at hi = 11). It decides, at each overflow, whether a new R digit appears and whether the overflow is silent. Confidence stays med.

Inner-record form. Every left turn of A onto a 0, where the right side matches, has the form 0^inf W A>(001)^p 00 D T. - D = digits (0b10001 with (100)^g gaps, LSB leftmost), value v, N digits. - T = tail. - W = wall. In normal mode W is empty and p is the lead a. - Z(g) := (010)^(g+1) is a large gap g packed into the wall (a "zone").

Pause rules (scripts/deepen_rules.py, seed 7: 150/150 each, 1050/1050; seed 1: 70/70; exact whole-tape match at the next inner record). In P100/P010/ZX/ZXN/ZXP below, b0 = 0, and every counter increment must stay below 2^N. - P100: (100)^(n+1) 1 | p, v -> (100)^n 1 | p+1, v+2. - Steps: 12p + 6(g1+..+gj) + 24j + 19, where j is the carry depth of the second +1. - Exact on 60/60. - WX: 1 | p -> empty wall, i.e. normal mode with lead p+1 and v+2. - P010: Y (010)^(m+1) 01 | p -> Y (010)^m 01 | p+1, v+2. Same step formula as P100. - ZX (end of a zone): Y (010)^h 1001 01 | p -> Y (010)^(h-3) 01 | 0, with a new LSB digit 0 at gap p+2. The value becomes 2v+4. - Steps: 12p + 6S + 24j + 39. Exact on 60/60. - ZXN: (100)^n 10100101 | p -> (100)^(n-2) 1 | 0, new digit at gap p+2, value 2v+4. - ZXP: (100)^n 01 | p -> (100)^(n-1) 10 | p+1 (v+2) -> (100)^(n-3) 1 | 0, new digit at gap p+1, value 2v+6. - Y ranges over the wall prefixes seen in the run. - Inc (normal mode) is unchanged from the observe pass.

Overflow transitions (scripts/deepen_ovf.py: 260/260). These start from the 13 real overflow configurations up to 6e8 steps, randomising a, n, p and the large gaps G while keeping the R block and the tail. - NO (normal mode, all ones): A>(001)^a 00 D T -> (100)^a 101001 [Z(g) 1001 for g in G] 01 A> 00 D_R(0) T'. - PO (wall (100)^n 1, v = 2^N - 2): -> (100)^n (010)^(p+1) 1001 [Z(g) 1001 for g in G] 01 A> 00 D_R(0) T'. - SILENT (only the tail state of the step-1.45e7 event): there is no pause. The counter wraps to 0 and the lead grows by 1. - D_R(0) T' (the R block reset, possibly one digit longer, plus the new tail) depends only on T. It is the same for NO and PO in 13/13 cases (scripts/deepen_tail_typeindep.py).

What a pause is. 1. The overflow packs every large gap into a zone. The lead (NO) or the inner lead p (PO) goes into the wall. 2. The zones are rebuilt innermost first, with +2 per cycle. ZX restores each gap exactly; the gap-2 digit is ZX with p = 0. 3. The outer (100) wall is then eaten, also +2 per cycle. 4. The pause ends one of two ways: - WX first: back to normal mode with lead = wall + 1. This is the old "Ovf-short". - PO first: p becomes a new gap p-1 via ZXP, and the outer phase continues.

This answers the observe-pass open items: - Exact bits after a pause: v follows the rules above. - Gap formula: each new gap is p_ovf - 1. - Multi-insert at 1.14e8: three POs in one pause (1028, then 4097, then 7). The 7 is the remainder of the wall. - R growth: the tail emits a gap-1 digit at alternate overflows. The emission bit equals the new low bit of the tail's first 2-bit unit. - The 1.45e7 event: a silent overflow, which is why the next pause came only at 1.14e8 (a = 1849 + 4096 = 5945).

Macro model (scripts/deepen_abstract.py). It uses the tail oracle e0, e1, e0, e1, S, e0, e1, e0, e1 (e = R digits emitted, S = silent). It reproduces every normal-mode entry from step 36,124:

real step a v G
236,797 48 602 68, 28
2,847,332 204 2450 260, 68, 28
555,048,797 800 bits 01110100011000001 7, 4097, 1028, 260, 68, 28 (NR = 10)

Every value is exact.

Run forward with strict e0/e1 alternation and no silent events, the model is perfectly regular for 40 normal-mode cycles: each NO is followed by exactly one PO, the new gaps are 32778, 131076, 524292, ..., and no degenerate case occurs.

Tail. - Front: two 2-bit units 0x0y10001 (cells -66/-64 and -57/-55). - Further right: about 8 more cells that change rarely. - Driven only by overflow carries. - Synthetic driving (scripts/deepen_tail_chain.py): a fresh small counter is prepended each round. Over 675+ rounds (about 7,500 overflow events), every tail cell up to the last few has changed, with no right-edge move, no halt and no growth past the 79 cells. - Not decoded: - when an overflow is silent; - whether the tail cycles; - what its own top overflow does.

Remaining gaps (all needed for a proof): 1. The tail's full transition function (finite but undecoded). 2. A SILENT overflow during a pause. A synthetic PO with that tail state gives no pause, and no rule is written for it. 3. Degenerate small parameters that the arithmetic might produce after silent events: - a PO with p ≤ 2 (new gap ≤ 1, a zone with fewer than 3 blocks); - an outer wall n < 3 at a PO; - a < 2 at a NO. 4. Step counts for NO, PO, ZXN and ZXP (they are needed for the Rocq accounting, not for the argument).

Not a cryptid candidate: all arithmetic is linear (v -> 2v+4, gap = p+2), the tail is a deterministic finite-state transducer, and there is no parity branching on exponential values.

Deepen pass 2

Outcome: the tail is decoded far enough to drive the real dynamics, but not far enough for a proof. Confidence stays med; recommend more observation (round 3: a general tail rule).

Round 1's tail chain was wrong. deepen_tail_chain.py prepended a prefix with no gap-2 digit, so the tail sequence it produced is not the real one: about half its events were silent. Its "675 rounds, no right-edge move" result does not carry over. In fact the right edge does move, as shown below.

Correct driver (scripts/deepen2_rc_chain.c, Python reference deepen2_rc_chain.py): - RC = everything right of the gap-2 digit (the gap-1 R digits plus the tail). Tail cells change only at overflows. - So the RC at the next overflow is the RC after this overflow with its digit bits set to 1. - Each step simulates A>(001)^a 00 0110001(100)^2 RC directly, up to the next inner record, with a random a. - It reproduces all 12 real RC transitions exactly (steps 8,109 to 400,944,248, including the silent one at 1.45e7).

40,000 overflows (deepen2_rc_chain_40k.summary.json): - 34,984 NO and 5,016 SILENT. Nothing else, and no halt. Each NO left part is checked exactly; each SILENT is checked for lead a+1 with the gap-2 digit kept. - R ends with 17,496 digits; the RC is 175,040 cells. - The right edge moves +2 at overflows 9,057 and 24,241.

Tail decision rule (40,000/40,000). The front unit is cells c-78, c-76, counted from the right end before the first growth: - The cycle is 10 → 01 → 11 → 00 → 10. - SILENT ⇔ the wrap goes 11 → 10 instead of 11 → 00. - An R digit is emitted ⇔ c-78 flips 0 → 1. - Whether the wrap is to 00 or to 10 depends on the rest of the tail. Silent overflows come 7 or 11 overflows apart.

Tail shape. Five fixed units, then a growing end unit: 0?0?0?10001 | 0?0?10001 | 0?1000?10001 | 0?0?1000?10001 | 0?1000?1000?1000?1000?10001 | (0?)^m 01 - m = 3 → 4 → 5 at overflows 9,057 and 24,241. Every other cell is constant. - Up to overflow 9,057, the number of silent events so far is an exact linear function of the tail bits. Weights: 1, 2, 3, 6, 10, 16, 32, 52, 64, 104, 128, 256, 464, 720. - The end unit changes only at overflows 3313, 5361, 7009, 9057 | 14801, 18497, 20545, 22193, 24241 | 33681, 39425. - The gaps between those changes are 2048, 1648, 2048 | 5744, 3696, 2048, 1648, 2048 | 9440, 5744. They satisfy F(n) = F(n-1) + F(n-2), which looks like a Zeckendorf-style counter. Not yet a rule.

Macro model with the true oracle (deepen2_macro.py; deepen2_macro_8000.result.json). The run covers 8,000 overflows: 2,495 NO, 1,004 SILENT and 4,501 PO. - Silent overflows happen only in normal mode, never inside a pause. - Smallest parameters reached:

parameter minimum
p at a PO 8
wall at a PO 50
a at a NO 121
gap 7

New rules (deepen2_validate_s5.result.json: 60/60 each): - SILENTP, a silent overflow inside a pause: (100)^(n+1) 1 A>(001)^p 00 D(2^N-2) T_s -> (100)^n 1 A>(001)^(p+1) 00 D(0) T_s'. This is P100 with the counter wrapping. The macro model never reaches it. - SILENT re-checked with the real silent tail state (random a ≥ 0 and 0–3 large gaps).

Steps (all exact):

rule steps instances
ZXN 12p + 6S + 24j + 39 60/60
ZXP, first half 12p + 6S + 24j + 19 60/60
ZXP, second half 6(p+1) + 23 60/60
NO 3a + 3ΣG + 7|G| + C_NO(RC) 60/60
PO 9p + 3ΣG + 7|G| + C_PO(RC) 60/60

For NO and PO the RC is held fixed; C is 248 and 258 for the RC just before overflow 7. Sources: deepen2_validate_s5.result.json and deepen2_ovf_steps_s2.result.json.

Edge probes (deepen2_edge_s3.result.jsonl): NO with a ∈ {0,1}, PO with p ≤ 2 and PO with wall n ≤ 2 still give the NO/PO transition forms. The pause that would follow them was not followed.

Still open (needed for a proof): 1. A general tail rule: - the carry through the five fixed units (finite, so it can be enumerated); - a parametric rule for the end unit (0?)^m 01, including its growth. 2. A closed form for the macro dynamics as a function of the tail count: the super-cycle induction above. 3. The ZX and ZXP rules at small parameters. They are unreachable per the model, but that is not proven. 4. C_NO(RC) and C_PO(RC); these matter only for Rocq accounting.

Not a cryptid: every quantity seen is linear or follows a fixed recurrence (powers of 2 plus constants, Fibonacci-like tail gaps). There is no parity branching on exponential values.

Decision (2026-10-10)

Question: #8's left counter and overflow pause are fully ruled. Only the right-end tail, which decides NO / emit / SILENT at each overflow, lacks a general rule. Fund a third deepen round aimed at a tail-independent proof, or park #8? Answer: deepen3_oracle_free (Fund deepen round 3, scoped to an oracle-free proof). Dennis: go with all recommendations (2026-10-10).

Funded stage (2026-10-10, deepen3_oracle_free)

Outcome: both tests pass once test (1) is stated with the front-unit rule. The proof does not need the Zeckendorf-like schedule or the super-cycle induction. It needs four things: the tail closure, the front-unit automaton, one parametric end-unit rule, and a short interval invariant for the macro arithmetic. Confidence is now high; proof.md is next. Scripts are scripts/deepen3_*. The big closure tables are not kept; deepen3_closure.c rebuilds them in about 2 minutes in total.

Test (1): the macro model under outcome sequences (deepen3_macro.py, an event-level rewrite of deepen2_macro.run that adds SILENTP). - Regression: with the true tail sequence it gives the same counts as deepen2_macro_8000 (2,494 NO, 4,499 PO, 1,003 S; min p 8, min wall 50). - Arbitrary sequences fail. Uniform e0/e1/S at every slot: 200/200 seeds degenerate within 400 events (150 PO with p <= 2, 50 counter overflows during a rebuild). The arithmetic shows why. A PO with e0 right after a NO rebuild leaves 2 cycles to the next PO, and an S at a PO slot followed by an e0 PO overflows the rebuild. - Front-unit sequences pass. These are the TAILFRONT sequences (10 -e0-> 01 -e1-> 11 -e0-> 00 -e1-> 10, or 11 -S-> 10), with S free at every 11 slot, including slots inside a pause: - random runs: 400 seeds x 1,500 events (q = 0.05 / 0.3 / 0.7, plus S only in normal mode), 0 degenerate, 16,053 silent overflows inside pauses; - exhaustive DFS: all 2,265,815 such sequences of 72 events from the step-36,124 state (12.5 M nodes, 803,709 SILENTP), 0 degenerate. - Minimum values reached: p at a PO 8, wall at a PO slot 34, a at a NO 121. - Invariant (derived by hand, then checked). At a normal-mode overflow let M = 2^N, c = D(G,R) - 4 with D = 2^(k+R) - 2^(k+1) - 2·Σ(G_i - 1)·2^i, s = a - c, and f = the front unit. Then - f = 11 and 24 <= s <= M/4 + 2, or - f = 10 and s is in [8, M-14] or in [M+24, 2M]; - and always c = M/4 + κ with κ in {2, 8}. Between normal-mode overflows only four paths occur (P1 from either f, so five transition types in the data):

path from f acts M' s'
S 11 (to 10) S M s + M
P1 10 / 11 (to 11 / 10) e0 e1 4M M + 10 - s
P1S 10 (to 10) e0 e1 S 4M 5M + 10 - s
P3 10 (to 10) e0 e1 e0 e1 32M 9M + 32 - s

Test (2): tail closure (deepen3_closure.c, deepen3_closure_check.py). - The tail is a right-anchored window W(m) = the round-2 template with every ? free. RC = (0110001100)^r H W, where H = 01100 is the half R digit. - Every bit setting for m = 0..8 was run through one overflow by direct simulation: 33,488,896 inputs. All give N or S, with the NO wall / SILENT form checked, and the output is again in the shape (m or m+1). No halt, no other outcome. - L* (x = 1 and H = y; the real tails are in it): 8,372,224 inputs. All are closed in L*, and the front unit (y,z) with emission e = (r'+H') - (r+H) follows TAILFRONT exactly. - Outside L*, TAILFRONT does fail, so L* is the right invariant language. - The tables are byte-identical for (r,a) = (1,2), (2,2), (5,7) and (9,30) at m = 3 and 4. - They reproduce 9,299/9,299 true RC-chain transitions, including the m = 3 -> 4 growth at overflow 9,057 (deepen3_closure_vs_chain.py).

Locality and the end-unit rule. - When the 15 fixed bits are not all 1, the head stays at least 6 cells left of the end unit (m = 0, 3, 6). So those 16,383 L* fixed states give a finite table that holds for every m and every end-bit setting. - When all 15 fixed bits are 1, the carry enters the end unit. Read its bits left to right: - 1^j 0 rest -> j even: N, (10)^(j/2) 1 rest; j odd: S, (01)^((j+1)/2) rest. - 1^m behaves like j = m+1 (the end marker 01 counts as a 1), and the unit grows to m+1. - The fixed bits become 100100010001010 (N, H'=0) or 110000100100101 (S, H'=1), with e0 either way. - ENDCARRY 300/300 and NOCARRY 300/300 (emission included). Both used m = 9..60, r <= 12, a <= 40, 0-2 large gaps, a full wall-form check and a reset check on the R digits (deepen3_endunit_s11.result.json). - Pause context: random L* tails give the same new RC from a PO / SILENTP start as from a NO / SILENT start, 200/200 (176 N, 24 S; deepen3_po_context_s5.result.json). - Token view, for proof.md: right of the lead the tape is a word over 00, 01, 100. A digit is b 100 01 (100)^g; an R digit is b 100 01 100. The tail units are xyz Z 1, ?? Z 1, ? Z ? Z 1, ?? Z ? Z 1, (? Z)^5 1, ?^m 1, where Z = 100 and 1 = 01.

Non-halting argument (for proof.md). 1. Direct simulation from blank to step 36,124. The tape there is K(12; v=146; G=[28]) with r + H = 6, the tail is in L* with m = 3, f = 11 and s = 55. 2. The invariant set is: a normal-mode overflow configuration with the tail in L* and (M, s, f, κ) as above. 3. Each path above is a finite composition of the validated rules: Inc, NO, PO, SILENT, SILENTP, P100, P010, ZX, ZXN, ZXP, WX, the L* tail table and ENDCARRY. Each takes at least one step and none halts. Each lands in the invariant set again, whatever the tail decides at an 11 slot.

Still open (formalization only, none of it a mechanism question): - The L* fixed-part table has 16,384 states. It is too big for one case per state in Rocq, so proof.md should break it into token-level sweep rules over 00 / 01 / 100. - Parametric proofs are still needed for Inc, the R-digit carry, the end-unit carry and the pause rules. All are validated only on random instances. - The step constants C_NO / C_PO remain unknown; they are needed only if the accounting needs them. - The .v file will be large, and the nearest pattern is a hand-written multi-level counter proof (busycoq CounterClass3v2.v). - Round 2 (2026-10-10, formalization). check_kill PASS -- this is a kill (sha256 0ddf7487..a879a1; compile 10.2 s native on, coqchk 3.2 s, 0 assumptions). Built in rocq/T2.v (details and lessons in rocq/log.md): tail layer without any table (Tail10/Tail0z/Tail11 via the retf transducer, 13 generated first-zero leaves + the end-unit induction), overflow core OvN1/OvN0/OvS1, generic pause/zone-rebuild lemmas (TwoInc, ZXg, ZXP2g, Zones), NOrb/POrb/SILENT/SILENTP, the four paths pathS/P1/P1S/P3, INV (gaps >= 2 suffice), step, init (solve_init, 92,299 steps), nonhalt via progress_nonhalt_cond. Open: fold the retf reduction into proof.md section 9 / package the kill.

Kill