/machines/1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD/notes.md · raw

1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD

Status: CHECKPOINT_A Class guess (agent / Dennis): Bouncer + Chaotic Edge (the edge erodes the bouncer block) / ? Spreadsheet notes / Discord thread: Results row 899 has class "Bouncer + Chaotic Edge" and no status, notes, links, strikethrough or comment. It is on mxdys's 2026-08-24 UBRRBA_TODO list (line 82), which Dennis ruled fair game on 2026-10-10. No claim found. Viewer: https://bbchallenge.org/1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD

Observation

At 1e9 steps: no halt. Span 32,607 (lo −344, hi 32,262) and 31,695 nonzeros. The tape is 0^inf w 1^30399 0^inf with |w| = 2,205.
The bouncer: the block gains +1 cell per bounce, with 32,262 bounces by 1e9.
The edge:
It has positive entropy: factor complexity is about 1.53^k, roughly 0.6 bits per cell.
It is aperiodic: compress track gives 300 distinct skeletons in 300 snapshots.
Its left end has been frozen since bounce 4,790.
It grows into the block at +0.057 cells per bounce on average. Bursts reach 11 cells in one bounce and 60 cells in 50 bounces.
Dive depth per bounce: heavy-tailed. The median is about 20 cells and the maximum 888 (bounce 25,407).
Early close call: the block was only 2 cells long at bounces 10 and 14–16. It has been ≥ 29 since bounce 30.
Tools:
qsim found block size 2 and 0 prover rules. 200k loops reach only step 2.45M.
rulefit found no validated rules; all 16 fitted rules died in validation. Its pool-free unit tests pass (13).
compress: no stable skeleton for w.
Diagrams (img/):
edge_every4e5_1e9.png is the most telling.
closeup_waves.png / .html
records_1e8.png
default_site.png, explore_site.png
viewer.html
Own analysis code: work/. It contains sweeps.c/dumpw.c (per-bounce stats), inv00.c (invariant checker, mutation-tested), leftproc.py/validate_map.py (wall model), absbfs*.py (arbitrary-left abstraction search) and validate.py.

Candidate rules

Notation follows the wiki: x and y are arbitrary sides. - Bounce: x A> 1^n 0^inf --> x <C 1^(n+1) 0^inf, 2n+3 steps. 48/48. - x 0 1^k <C y --> x 0 <C 1^k y (k). 48/48. - C reading 0 splits completely into three cases: - x 00 <C y --> x 10 A> y (3). 40/40. - x 010 <C y --> x <C 011 y (3). 40/40. - x 110 <C y --> x <D 101 y (7). 40/40. - Bounce map, with the block treated as a wall: 0^inf w <C 1^n --> 0^inf f(w) <C 1^(n+1-e(w)) for n ≥ e(w)+3. f, e and s come from the wall model and do not depend on n. Validated 120/120 against sim.py on real w and random n, and exact on 32,061 consecutive real bounces. - Halting door: x A> 0 1 0^j 1 00 y --> halt in j+5 steps. 48/48. By the transition table this is the only route to E0 (A0 → B1 → F0^j → F1 → D0 → E0). - Invariant: the cells from head+1 to the rightmost 1 never contain 00. It held at every step from the blank tape to 1e9 (the checker was mutation-tested). - Local reason: the only left move that writes 0 is B0, and B's right neighbour is always 1. B is entered via D1, which wrote a 1 there, or via A0, where A's right context was already free of 00. - An arbitrary-left exhaustive search (right word ≤ 20) found 182,877 abstract states and 0 violations. The counts per length are Fibonacci, i.e. the golden-mean language. - Consequence: the machine halts only via A> 0 11 0^inf or A> 0 101 0^inf (40/40), i.e. if the edge eats the block down to 2 cells. - Open: a deterministic bound on erosion, meaning a potential showing that the edge grows by less than 1 per bounce. In the arbitrary-left abstraction the block can be eroded, so the bound must use the structure of w.

Checkpoint A (Dennis)

(pending)

Informal proof

Not started (waits for Checkpoint A).

Formalization log

—

Outcome

—

Decision (Dennis, 2026-10-10)

Flagged CRYPTID_CANDIDATE and deprioritized, based on research/erosion.md (no deterministic erosion bound). Still owed under the cryptid protocol: a Rocq rule reduction (the 7 bounce rules plus the no-00 invariant), like AntiHydra.v. Low priority. Twin #26 (1RB1RA_1LC1RE_---0LD_1LE1LD_0RA0LF_1LF0LB) likely shares the verdict; not yet checked.

Card data pass (2026-10-10)

Figures on the card: Fig 1 = img/edge_every4e5_1e9_labeled.png, Fig 2 = img/closeup_bounces54-57.png, Fig 3 = img/block_vs_edge.png, Fig 4 = img/default_site.png. Figs 1-3 are the primary figures, shown beside the checkpoint.
The card's mechanism is cut to 3 bullets. The full list before the cut:
Bouncer: a solid 1-block on the right gains one 1 per bounce (span ~ t^0.5).
Left of it is a chaotic edge: 2,205 cells at 1e9, about 0.6 bits of entropy per cell, not periodic.
Each bounce, C dives into the edge (carry-like zigzag waves, depth heavy-tailed up to 888), then A runs back.
Invariant: no 00 ever lies between the head and the rightmost 1. Checked at every step to 1e9; local proof.
So it halts only if the edge eats the block down to 2 cells. Edge drifts +0.057 cells/bounce; block +1.
Checkpoint questions are now yes/no questions about the figures. Moved off the card (strategy calls, not figure reading; settle them in proof.md / Checkpoint B):
"Should we post the Discord question below before spending proof budget on the erosion bound?"
Old Q3 asked whether to post "the Discord question below", but discord_check is null and Dennis decided on 2026-10-10 (cryptid candidate, deprioritized). Replaced by a figure question on block_vs_edge.png.

Rule reduction (2026-10-12)

This is not a kill. Status stays CRYPTID_CANDIDATE. The file is rocq/rule_reduction.v; compile it with rocq/compile.sh rocq/rule_reduction.v. It takes 1.9 s against unmodified busycoq (Coq 8.20.1) and contains no Admitted, Axiom or Parameter. Print Assumptions shows #5's lemmas closed under the global context, and the twin lemmas use only functional_extensionality_dep (baseline). - Proved: the local rules (AntiHydra.v style, es). - The walks walkA and walkC, the bounce x A> 1^n 0^inf -> x <C 1^(n+1) 0^inf, and the F sweep walkF. - T, Ca, Fo (6 steps) and Fo7 (x 110 <C -> x <D 101). - E1, E2, P1 and P2. - The mid-tape turn x A> 0 0 y -> x <C 1 0 y (rule_turnA). This adds to the table: the invariant allows A> 0 0, and research/erosion.md's claim that only 4 right contexts occur is stronger than what the invariant gives. - door_halts j: x A> 0 1 0^j 1 0 0 y halts. - Proved: the no-00 invariant, closed under every step (Inv_step). - Rg r means the right side is a word with no 00, followed by 0^inf. - Inv says: Rg of the right side; in state B, also Rg(head :: right); and D never sits at a 1 with a 1 on its left and a 0 on its right (hd r = 1 \/ hd l = 0). - The third clause was needed. Without it, the door has a second entrance, D1 -> B1 -> F1 -> D0 -> E0, which this clause rules out. It is a one-step history fact. - A0_cover: under Rg, the case split for A reading 0 is complete. The cases are: turn, A> 0 1 0^inf (F then sweeps right forever), the two door shapes, E1, P1, E2 and P2. - Proved: halting goes only through the door, with j <= 1 and nothing after it (halts_in_door, Door_back, FDoor_Rg, ADoor_BlockGone). - Stated as an open Definition (not proved): BlockGone c := exists l, c = l {{A}}> [0;1;1] *> 0^inf \/ c = l {{A}}> [0;1;0;1] *> 0^inf erosion_open c := forall c', c -->* c' -> ~ BlockGone c' In words: the edge never eats the 1-block down to 2 cells. - Proved reductions: - reduction : erosion_open c0 -> ~ halts tm c0 - nonhalt_iff_erosion_open : ~ halts tm c0 <-> erosion_open c0 (the converse holds via door_halts). - So the open property is exactly non-halting. What the file adds is that the invariant collapses every halting route to these two tiny-block shapes. - The research-level gap is unchanged: a deterministic erosion bound (eaten in w bounces <= aw + b with a < 1, research/erosion.md) would imply erosion_open, but that implication needs the bounce/wall-model decomposition and is not formalized. - Twin #26 is in the same file (Part 5).* - perm_twin : Perm tm26 (flip tm) sigma, with sigma = A->C, B->D, C->E, D->A, E->B, F->F. - reduction_twin : erosion_open c0_twin -> ~ halts tm26 c0, and nonhalt_twin_iff_erosion_open. - Here c0_twin = C;; tape0: #5's own table started in state C on the blank tape, not #5's c0. - The twin's own local rules (tw_*: walks, bounce, T, Ca, Fo, E1, E2, P1, P2) are also proved directly with es.

Rocq rule reduction (2026-10-12)

This is not a kill. Status stays CRYPTID_CANDIDATE. The file is [local working file]. It compiles in 2.8 s with coqc 8.20.1 against unmodified busycoq (-native-compiler yes) and contains no Admitted, Axiom or Parameter. Print Assumptions for reduction, reduction_iff, reduction_tm, reduction_twin and reduction_twin_iff says "Closed under the global context" for all five, so not even funext is used. - How it differs from rocq/rule_reduction.v (section above, written by a parallel session the same day): both compile and prove the same equivalence. - That file closes its invariant under every raw machine step and states the open condition on the machine's reachable configurations. - This file states the condition on the 7-rule system itself. Its invariant is stronger in mode A: the word from the head on (A's own cell included) is in (1|01). So A> 0 0 never occurs mid-tape, and research/erosion.md's "only 4 right contexts" claim is proved; rule_turnA is never needed. - Rules, each -->+ or -->* for arbitrary sides, by es: - A_walk and C_walk; End_turn (x A> 0^inf -> x 1 <C 0^inf); Bounce (x A> 1^n 0^inf -> x <C 1^(n+1) 0^inf). - T_rule, Ca_rule, Fo_rule, Fo7_rule, E1_rule, E2_rule, P1_rule and P2_rule. - Run_rule and F_sweep: with a 1-cell block, F runs right forever. - Door_halts j: x A> 0 1 0^j 1 0 0 y halts. - Configuration family: conf (MA,l,v) = l A> v 0^inf and conf (MC,l,v) = l <C v 0^inf (C reads the cell left of v), plus mode MF for the runaway. - The rules form the relation rstep: walks, T, Ca, Fo, end turn, E1, E2, P1, P2 and the runaway. - rstep_sound: every rule is a -->+ run of the machine. - rstep_deterministic: at most one rule applies. - Invariant: GM v means v is in (1 | 01), i.e. it has no 00 and no trailing 0 (GM_no00, GM_no_trailing0). rstep_GM: every rule preserves it. - Completeness: by rstep_progress, under the invariant some rule applies unless the state is eaten, i.e. A> 0 1 1 0^inf or A> 0 1 0 1 0^inf. eaten_halts: both of those halt. - The open condition is a Definition, used as a premise and never proved: reach s a : a is reached from s by rstep steps EdgeNeverEats s := forall a, reach s a -> ~ eaten a a0 := (MA, 0^inf, []) (conf a0 = c0) In words: along the rule orbit from the blank tape, the edge never eats the 1-block down to two cells. - Theorems: - reduction : EdgeNeverEats a0 -> ~ halts tm c0 - reduction_iff : ~ halts tm c0 <-> EdgeNeverEats a0 - reduction_tm: the same premise read on the raw machine (c0 never reaches l A> 0 1 1 0^inf or l A> 0 1 0 1 0^inf). - Twin #26: - perm_twin : Perm (flip tm26) tm phi and perm_twin' : Perm (flip tm) tm26 psi, with psi = phi^-1. The second gives the converse without flip_involutive. - reduction_twin : EdgeNeverEats a0_twin -> ~ halts tm26 c0 and reduction_twin_iff, where a0_twin = (MC, 0^inf, []) is #5's table started in C on the blank tape. - Gap (unchanged): the bounce-level wall map 0^inf w <C 1^n -> 0^inf f(w) <C 1^(n+1-e(w)) is not formalized. An erosion bound (eaten in w bounces <= a*w + b, a < 1) would need that layer to imply EdgeNeverEats a0.