1RB1LA 1RC0RF 1RD--- 0LE1RB ---0LA 1LD1RF

From BusyBeaverWiki
Jump to navigation Jump to search

1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF (bbch)

Similar to the following machines[1][2]. 

1RB1LA_0RC1LD_1LA0RE_1LF0LA_1LD1RE_1LB---
1RB1LA_0RC1LE_1LC0RD_1LE1RD_1LF0LA_1LB---
1RB1LA_1RC0RF_1RD---_0LE1RB_0LA0RD_1LD1RF
1RB0LE_1RC0RF_1RD---_0LA1RB_1RB1LE_1LD1RF
1RB1LA_0RC1LE_0LC0RD_1LE1RD_1LF0LA_1LB---
1RB0LC_0LA1RD_1RD1LC_1RE0RF_1RB---_1LB1RF
1RB---_0LC1RE_0LD0RB_1RE1LD_1RA0RF_1LB1RF
1RB---_0LC1RE_---0LD_1RE1LD_1RA0RF_1LB1RF

Most of the following was written by Opus 4.6, based on the Lean proofs and proof attempts, managed by Discord user DrDisentangle.

Tape structure

The tape is always a block of 1s with a small number of zero-markers scattered inside: 

0^inf  1^a₁  0  1^a₂  0  ...  1^aₖ  [HEAD]  1^b₁  0  1^b₂  0  ...  1^bₘ  0^inf

The total tape length grows slowly (O(log steps)). The number of zero-markers varies by phase but is always small (≤ ~log(tape_length)).

Summary of halt conditions

Halt Necessary condition Status
C,1 B reads 0 with 1 to its right Open — resists all proof attempts
E,0 F reads 0 with two consecutive 0s to its left Proven — e0_never_reached via E0Inv

Macro-level representation

The tape is encoded as a list of run lengths [a₁, a₂, ..., aₖ] where each aᵢ counts consecutive 1s between zero-markers: 

Let [0^inf, a₁, ..., aₖ, (c), b₁, ..., bₘ, 0^inf] denote the tape

    0^inf  1^aₖ  0  ...  0  1^a₁  0  1^(c-1)  A>  1  0  0  1^b₁  0  ...  0  1^bₘ  0^inf

(A> means state A reading the rightmost 1 of the cursor run.)

The special cursor (0) denotes "state A reading the left 0 of a 00 gap":

    [0^inf, a₁, ..., aₖ, (0), b₁, ..., bₘ, 0^inf] =
    0^inf  1^aₖ  0  ...  0  1^a₁  A>  0  0  1^b₁  0  ...  0  1^bₘ  0^inf

Invariant carried by all proven rules:
  - every aᵢ ≥ 1, every bⱼ ≥ 1;
  - cursor (c) with c ≥ 2, or cursor (0) with at least one left run and one right run;
  - for (0) configurations, the right side does NOT begin with (1, z+1, ...)
    — such a shape would trigger rule Halt.

=======================================================================
Proven macro rules (see machine.lean)
=======================================================================

In each rule, "..." on the left/right matches any (possibly empty) prefix/suffix
of runs unless explicitly restricted. All shown run-length parameters (a, b, c,
d, r, z, mᵢ) are ≥ 0 unless noted; so e.g. "c+3" means the cursor is ≥ 3.

--- Right-sweep with neighbors (cursor ≥ 3) ---

Sweep:    [..., a, (c+3), d, ...]   ->   [..., a+1, (c+1), d+1, ...]
          in 2c+13 steps.                         [macro_sweep]

SweepL:   [(c+3), d, ...]           ->   [1, (c+1), d+1, ...]
          in 2c+13 steps.                         [macro_sweep_left_empty]

SweepR:   [..., a, (c+3)]           ->   [..., a+1, (c+1), 1]
          in 2c+13 steps.                         [macro_sweep_right_empty]

SweepS:   [(c+3)]                   ->   [1, (c+1), 1]
          in 2c+13 steps.                         [macro_sweep_solo]

--- Right-sweep terminating at cursor 2 ---

SweepE:   [..., a, (2), d, ...]     ->   [..., a+1, (0), d+1, ...]
          in 11 steps.                            [macro_sweep_to_zero]

SweepLE:  [(2), d, ...]             ->   [1, (0), d+1, ...]
          in 11 steps.                            [macro_sweep_to_zero_left_empty]

SweepRE:  [..., a, (2)]             ->   [..., a+1, (0), 1]
          in 11 steps.                            [macro_sweep_to_zero_right_empty]

SweepSE:  [(2)]                     ->   [1, (0), 1]
          in 11 steps.                            [macro_sweep_solo_to_zero]

--- Cursor = 1 shift (auxiliary; never arises under the invariant) ---

Shift:    [..., a+1, (1), d, ...]   ->   [..., (a+1), 1, d, ...]
          in 6 steps.                             [macro_shift]

--- Zero-cursor bounce rules (right side has only one run) ---

EraDone:  [..., a+1, (0), 1]        ->   [..., (a+6)]
          in 8 steps.                             [macro_era_complete]

Bounce:   [..., a, (0), z+4]        ->   [..., a+4, (z+1), 1]
          in z+13 steps.                          [macro_zero_bounce]

BounceE:  [..., a, (0), 3]          ->   [..., a+4, (0), 1]
          in 12 steps.                            [macro_zero_bounce_to_zero]

--- Zero-cursor rules where right side begins with 2 ---

Two:      [..., a, (0), 2, d, ...]  ->   [..., (a+3), d+1, ...]
          in 8 steps.                             [macro_zero_two]

TwoS:     [..., a, (0), 2]          ->   [..., (a+3), 1]
          in 8 steps.                             [macro_zero_two_solo]

--- Multi-run bounces (two or more right-side runs, first ≥ 3) ---

Multi2:   [..., a, (0), r+3, z+2]
          ->   [..., a+4, r+1, (z+1), 1]
          in r+z+17 steps.                        [macro_multi_bounce_2]

Multi2E:  [..., a, (0), r+3, 1]
          ->   [..., a+4, r+1, (0), 1]
          in r+16 steps.                          [macro_multi_bounce_2_to_zero]

MultiN:   [..., a, (0), r+3, m₁, ..., mₖ, z+2]   (k ≥ 1, every mᵢ ≥ 1)
          ->   [..., a+4, r+1, m₁, ..., mₖ, (z+1), 1]
          in r+z + 3k + (m₁+...+mₖ) + 17 steps.   [macro_multi_bounce_general]

MultiNE:  [..., a, (0), r+3, m₁, ..., mₖ, 1]     (k ≥ 1, every mᵢ ≥ 1)
          ->   [..., a+4, r+1, m₁, ..., mₖ, (0), 1]
          in r + 3k + (m₁+...+mₖ) + 16 steps.     [macro_multi_bounce_general_to_zero]

--- Halting ---

Halt:     [..., (0), 1, z+1, ...]   ->   HALT
          within 6 steps (C reads 1, undefined). [macro_halt]

=======================================================================
Startup
=======================================================================

Init:     blank tape  ->  1^5 all-ones, D at rightmost 1
          in 19 steps.                            [sweeper_init_to_era0]

EraToM:   1^{n+1} all-ones with D at rightmost 1  ->  [(n+2)]
          in 5 steps.                             [era_to_macro]

Combining Init + EraToM(n=4) + SweepS(c=3):

InitM:    blank tape  ->  [1, (4), 1]
          in 43 steps.                            [init_to_macro]

Era structure

Define the configuration M(L, c, R) (with L,R lists of values) in the above notation as [0^inf, a₁, ..., aₖ, (c), b₁, ..., bₘ, 0^inf].

An era boundary is a shape M(L, c, [1]) with L ≠ [] and cursor c ≥ 4

  • Era 0 start: raw step 43, M([1], 4, [1]), reached from the blank tape via init_to_macro = Init + EraToM(4) + SweepS (see above).
  • Era end: EraDone (macro_era_complete) collapses [..., a+1, (0), 1] into the solo-cursor config [..., (a+6)].
  • Next era start: SweepR (macro_sweep_right_empty) fires immediately on that solo cursor, producing M(L, c+1, [1]) with c+1 ≥ 4.

Empirical era data (era-sim, see era_findings.md)

  • 63 765 era boundaries logged in era_full.jsonl over ~100 G macro steps by dedicated Rust macro simulator.
  • Every boundary has kind = M, R = [1], c ≥ 4.
  • Max observed size of L:|L| = 19; all L entries fit in u64; L = [1] only at era 0.
  • The last era boundary seen with |L| = 1 was M([2 059 956], 66 885, [1]), so they don't disappear.
  • No periodicity: distinct (L, c) at every recorded era.
  • Within an era: c decreases by 2 per Sweep until c ∈ {2, 3}, then SweepE/sweep_and_shift exits to an M0-cursor phase that runs through Bounce/multi_bounce chains until EraDone fires.

The first 50 era boundaries: 

  era   0  m=      0  raw=        43  M([1], 4, [1])
  era   1  m=      4  raw=       120  M([1], 10, [1])
  era   2  m=     28  raw=       567  M([12, 6], 5, [1])
  era   3  m=     79  raw=      1881  M([19, 2, 7], 9, [1])
  era   4  m=    114  raw=      2820  M([8, 7, 2, 7], 21, [1])
  era   5  m=    157  raw=      3931  M([42, 2, 7], 6, [1])
  era   6  m=    200  raw=      6002  M([13, 24], 28, [1])
  era   7  m=    226  raw=      6843  M([25], 50, [1])
  era   8  m=    446  raw=     19141  M([35, 39], 21, [1])
  era   9  m=    642  raw=     28664  M([16, 39, 19, 8, 13], 12, [1])
  era  10  m=    653  raw=     28933  M([40, 19, 8, 13], 35, [1])
  era  11  m=    949  raw=     42995  M([20, 94, 18], 5, [1])
  era  12  m=   1212  raw=     69570  M([120], 41, [1])
  era  13  m=   2077  raw=    149943  M([87, 11, 16], 93, [1])
  era  14  m=   2542  raw=    196126  M([39, 86, 79], 19, [1])
  era  15  m=   2732  raw=    218011  M([65, 70, 75], 23, [1])
  era  16  m=   3588  raw=    312008  M([41, 44, 166], 12, [1])
  era  17  m=   3599  raw=    312327  M([45, 166], 60, [1])
  era  18  m=   3656  raw=    315410  M([167], 116, [1])
  era  19  m=   4589  raw=    455568  M([24, 274], 13, [1])
  era  20  m=   4917  raw=    520689  M([153, 76, 38, 19, 8, 13], 14, [1])
  era  21  m=   6661  raw=    830505  M([57, 69, 71, 114, 19, 8, 13], 16, [1])
  era  22  m=   6714  raw=    834168  M([112, 71, 114, 19, 8, 13], 40, [1])
  era  23  m=   7163  raw=    909317  M([107, 110, 63, 76, 13], 22, [1])
  era  24  m=   7247  raw=    918546  M([178, 63, 76, 13], 71, [1])
  era  25  m=   8409  raw=   1107857  M([167, 201], 63, [1])
  era  26  m=   9239  raw=   1319254  M([64, 185, 190], 8, [1])
  era  27  m=   9453  raw=   1361310  M([329], 136, [1])
  era  28  m=  10869  raw=   1747511  M([53, 114, 146, 151], 19, [1])
  era  29  m=  10936  raw=   1750988  M([171, 146, 151], 25, [1])
  era  30  m=  11370  raw=   1845977  M([120, 135, 66, 71], 111, [1])
  era  31  m=  12223  raw=   1991854  M([49, 147, 306], 17, [1])
  era  32  m=  13403  raw=   2273429  M([119, 394], 34, [1])
  era  33  m=  14204  raw=   2491050  M([84, 345, 57, 62], 13, [1])
  era  34  m=  14629  raw=   2624017  M([211, 132, 199], 29, [1])
  era  35  m=  15534  raw=   2889239  M([307, 278], 10, [1])
  era  36  m=  16147  raw=   3097378  M([148, 374], 83, [1])
  era  37  m=  17532  raw=   3538974  M([316, 141, 69, 74], 31, [1])
  era  38  m=  18807  raw=   3881963  M([53, 279, 148, 74, 37, 17, 22], 15, [1])
  era  39  m=  19054  raw=   3947662  M([174, 326, 74, 37, 17, 22], 7, [1])
  era  40  m=  19424  raw=   4057867  M([282, 285, 37, 17, 22], 24, [1])
  era  41  m=  20084  raw=   4302642  M([261, 147, 169, 22], 80, [1])
  era  42  m=  22843  raw=   5315106  M([212, 486], 33, [1])
  era  43  m=  23055  raw=   5352785  M([675], 68, [1])
  era  44  m=  25059  raw=   6288271  M([237, 330, 43, 48], 113, [1])
  era  45  m=  27281  raw=   7045710  M([286, 431], 88, [1])
  era  46  m=  28000  raw=   7396795  M([356, 360], 103, [1])
  era  47  m=  29301  raw=   7854136  M([130, 477, 69, 74], 83, [1])
  era  48  m=  30841  raw=   8519664  M([393, 216, 221], 29, [1])
  era  49  m=  33269  raw=   9522575  M([218, 572], 101, [1])

Era mass strictly increases

Define the nth era mass Φn as the number of ones on the tape at the nth era boundary: Φn=(a1+a2+a3+…)+c+1, with ai the runs of ones to the left of cursor, and c the run at the cursor. Then Φn+1≥Φn+4. In other words, sum(L) + c is strictly increasing across every single era boundary. However, this does not prove the machine non-halting because it cannot be excluded at the moment that the halting path can be reached between era boundaries.

The proof of mass increase was formalized in Lean. A human-readable writeup exists: File:Phi strict.pdf. In short, for every non-halting rule the mass increase is shown to be ≥0.

Current status (2026-04-29)

Three reachability axioms (R1, R2, R3-narrow) were originally posited to bridge transient shapes that the macro rule set cannot directly handle. Of the three, R2 (M0(a::L', [r+3, 1, 2])) and R3-narrow (M0(a::L', (r+3) :: e :: f :: rest ++ [2])) have been closed. The only remaining custom axiom is R1 (reach_M_nil_3: M([], 3, d :: R)).

Empirical status of R1: the F1+F2 macro-step simulator (now ported to Rust as era-sim) records zero R1 firings across 99 G macro steps ≈ 6.2 × 1016 raw TM steps (era 63,765). Every era boundary lies in the strict-canonical shape M(L, c, [1]) with |L| ≥ 1 and c ≥ 4 — both conditions empirically incompatible with R1's shape M([], 3, R). The remaining work is to lift this empirical fact into a structural-exclusion invariant (form A.3 of invariant_strategy.md: "reachable ∧ c = 3 → L ≠ []").

Failed proof strategies

The core difficulty is that the naive invariant AllGe1 L ∧ c ≥ 1 ∧ AllGe1 R is not preserved by non-halting: many run-length configurations satisfying it actually reach the undefined C,1 transition and halt. For example M([], 3, R) halts for any R, as do M([], 7, R), M([], 15, R), etc. The "bad" cursor values at L = [] include {3, 7, 15, 31, 63, …} plus a Collatz-like cascade of even values reached through them — while the reachable orbit in fact avoids all of these. Several attempts to characterize the safe set failed:

  • Step-level invariants (C1Inv / SafeRight). Tracking a step-by-step predicate on the raw TM tape turned out to be unworkable: the bookkeeping for each phase transition explodes. Abandoned in favour of macro-step reasoning.
  • Mersenne-exclusion invariant. Adding L = [] → ¬IsMersenne c (i.e. c ∉ {3,7,15,31,…}) to the invariant. This was preserved by most rules but cascaded into conditions on L.head at c=1, which cascaded again into c=7, and so on — an infinite chain of increasingly complicated per-field conditions. Removed.
  • Compound-transition strengthening (Approach C). Proving chained macro rules (sweep_and_shift, zero_bounce_and_shift, era_and_sweep) to try to skip over the dangerous transient shapes. Blocked because halting depends on the full triple (L, c, R), not any single field: M([], 5, [1]) halts but M([], 11, [1]) does not, M([], 7, R) halts for every R but M([], 4, [4,6,2]) does not. No simple per-field condition can separate the two.
  • Strengthened EraPlusSweep predicate (RTailOkay). Restricting progress to configurations whose right-side run list "ends in 1 whenever it has ≥ 2 elements". Preservation fails at sweep_and_shift on M(L, 3, [1]), which produces M(…, [1, 2]) — a multi-element right side ending in 2, precisely the shape the predicate was meant to exclude.
  • macroEra function refinement. Defining a recursive macroEra that chains rules automatically and proves progress by computation. This closed most cases but left the same three transient shapes uncovered; they are genuinely reached by the raw TM and have no direct macro rule.
  • Backward cascade for R1 (Phase 2 layered analysis). Characterizing macroStep predecessors of M([], 3, R) layer by layer. Layers 0–4 completed (phase2.lean, ≈ 64 axiom-clean lemmas), but Layer 5+ branches unboundedly: each new producer shape begets two or more deeper producer shapes, with no fixed point in sight. Per-field invariants over the resulting branch tree are also ruled out (5 prior strengthening attempts failed for related reasons). Suspended; the realistic continuation is forward-simulation-driven derivation rather than backward enumeration.
  • Empirical era-state recurrence search. A native-code era simulator (era-sim, Rust port of macro_sim.py, bit-identically cross-validated) generated 63,765 era-boundary states, all of the canonical form M(L, c, [1]). Numerical experiments looked for a low-order recurrence on era state — linear fits on L_head[n+1], ratio statistics, residue patterns mod 4, periodicity, fixed-point attractors. All uniformly negative: L_head[n+1] / L_head[n] ranges over 0.006 … 378 with no clustering; L_head, c, L_sum mod 4 are uniformly distributed; all 63,765 (L, c) configs are distinct. Rules out forms C.2 (era recurrence) and C.4 (era-modular invariant) from invariant_strategy.md at the level of low-order arithmetic on era state. (The 2-adic-string analogue — a recurrence on L as a 2-adic digit sequence rather than on L_head alone — has not been ruled out.)
  • R3 doubling-chain decomposition (informational only). Of the 6,478 R3 firings recorded by the simulator, 29 % satisfy R[0] = L[0] + 1, and 1 % exhibit a clean recursive pattern R[k] = 2k−1·(2a + 1) for 1 ≤ k ≤ chain_len, with maximum chain length 11. This is the within-bridge structure of an R3 firing and was not needed for the Lean proof — the existing multi_bounce_general/shift_to_macro_prog closure handles all R3-narrow shapes uniformly without parametrizing the doubling. Listed here for completeness because it consumed analysis time before being recognized as not load-bearing.

Formalized proofs

  1. ↑ https://discord.com/channels/960643023006490684/1410023564249403577
  2. ↑ https://wiki.bbchallenge.org/wiki/File:BB6_holdouts_1104.txt
Retrieved from "https://wiki.bbchallenge.org/w/index.php?title=1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF&oldid=7500"