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

From BusyBeaverWiki
Jump to navigation Jump to search

1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF

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 Provene0_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

An era begins when the tape is all-1s (no zero-markers) with state D reading the rightmost 1. This is the E_Config n configuration in the Lean formalization.

Observed E_Config events (D reading rightmost 1 of all-1s tape):

Era Step Tape length E_Config n
0 19 5 E_Config 4
1 84 11 E_Config 10

Corrected observation: After E_Config 10, the machine enters a complex multi-zero-marker phase and does not return to an all-1s E_Config within 1M+ steps. The machine's behavior becomes increasingly complex, with persistent zero-markers that are never fully absorbed.

(Earlier claims of era boundaries at tape lengths 13, 27, 77 were incorrect — those were moments when the tape happened to be all-1s but the head was in a different state/position, not the D-at-rightmost-1 configuration.)

Simple era example (len=9, within era 0→1 transition)

Zero positions at each E→A transition:

step  43: zpos=[1,7]   distance=6
step  58: zpos=[2,6]   distance=4
step  69: zpos=[3,5]   distance=2  → merge

Three cycles to converge. Each cycle: both zeros move 1 inward.

Complex phase (len=15+, after era 1)

step 120: zpos=[1,13]  distance=12
step 147: zpos=[2,12]  distance=10
step 170: zpos=[3,11]  distance=8
step 189: zpos=[4,10]  distance=6
step 204: zpos=[5,9]   distance=4
step 215: zpos=[6,8]   distance=2  → merge
step 230: zpos=[10,15] (tape grew to 17, new pair spawned)
step 243: zpos=[11,14] distance=3
step 249: zpos=[12,14] distance=2  → merge (then complex multi-zero phase)

After the main pair merges, a secondary pair spawns at the right side, requiring further sub-era processing. This cascading behavior prevents the tape from returning to a clean all-1s state.

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 = 3L ≠ []").

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