1RB1LA 1RC0RF 1RD--- 0LE1RB ---0LA 1LD1RF
1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF
Similar to 1RB0LE_1RC0RF_1RD---_0LA1RB_1RB1LE_1LD1RF (bbch), see https://discord.com/channels/960643023006490684/1410023564249403577.
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
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.
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 onL.headatc=1, which cascaded again intoc=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 butM([], 11, [1])does not,M([], 7, R)halts for everyRbutM([], 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 atsweep_and_shiftonM(L, 3, [1]), which producesM(…, [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
macroErathat 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.
Current state: three tape-level conjectures
With the strengthened invariant and the recursive macroEra machinery, sweeper_never_halts now compiles with zero sorries, modulo three axioms (reachability conjectures) that each assert a specific tape shape is non-halting. Each has been verified by 10M-step simulation of the raw TM. Described on the literal tape (with [HEAD] marking the head cell):
Conjecture R1: isolated short cursor run
The head is in state A on the rightmost 1 of a length-3 block of ones, with nothing but blank tape on the left, and at least one more run of ones on the right:
0^inf 1 1 [1] 0 0 1^d 0 1^{b₂} 0 ... 1^{bₘ} 0^inf
(Lean: M([], 3, d :: R'), d ≥ 1.) Any such configuration that actually arises on the orbit continues to run; in isolation M([], 3, []) halts, so this is a genuine reachability statement about the dynamics, not a statement about the shape alone.
Conjecture R2: three-run right side, last run a singleton, middle run a singleton
The head is in state A reading a 0, with at least one block of ones on the left, and exactly three runs on the right, of lengths r+3, 1, 2:
0^inf ... 1^a [0] 0 1^{r+3} 0 1 0 1 1 0^inf
(Lean: M0(a :: L', [r+3, 1, 2]), r ≥ 0, a ≥ 1.) The last run is a single cell of ones of length 2 and the run immediately before it is a singleton of length 1. Multi-bounce would fire, but the resulting cursor value equals the middle run (= 1), which requires an extra shift not covered by any existing compound macro rule.
Conjecture R3: long right side ending in a length-2 run
The head is in state A reading a 0, at least one block of ones on the left, and four or more runs on the right whose last run has length 2:
0^inf ... 1^a [0] 0 1^{r+3} 0 1^e 0 1^f 0 ... 0 1 1 0^inf
(Lean: M0(a :: L', (r+3) :: e :: f :: rest ++ [2]), lengths ≥ 1, r ≥ 0.) The defining feature is again the trailing length-2 run. Closing this conjecture would require a recursively defined compound macro rule that threads multi-bounce through an arbitrary-length middle tail when the final run is a singleton-of-2.
Summary
| Axiom | Tape shape (right side) | Reason macro layer cannot close it |
|---|---|---|
reach_M_nil_3 |
empty left, cursor-run of 3, nonempty right | cursor too small; macro_sweep_left_empty would output c=1, under invariant
|
reach_multi_bounce_last_2_mid_1 |
3-run right side [r+3, 1, 2] |
output cursor = middle run = 1, needs extra shift |
reach_multi_bounce_last_2_long |
≥4-run right side ending in […, 2] |
needs a recursive multi-bounce compound rule |
Each conjecture is an orbit-reachability statement: it claims that any such shape that appears in the actual trajectory continues for at least one more macro step without halting. They are proved by the machine but not by the macro layer — 10M-step direct simulation confirms they do not halt. The final sweeper_never_halts theorem has axiom dependencies exactly {propext, Classical.choice, Quot.sound, reach_M_nil_3, reach_multi_bounce_last_2_mid_1, reach_multi_bounce_last_2_long}.