1RB1LA 1RC0RF 1RD--- 0LE1RB ---0LA 1LD1RF
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 | 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.
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 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.
- 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 ofmacro_sim.py, bit-identically cross-validated) generated 63,765 era-boundary states, all of the canonical formM(L, c, [1]). Numerical experiments looked for a low-order recurrence on era state — linear fits onL_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 4are uniformly distributed; all 63,765(L, c)configs are distinct. Rules out forms C.2 (era recurrence) and C.4 (era-modular invariant) frominvariant_strategy.mdat the level of low-order arithmetic on era state. (The 2-adic-string analogue — a recurrence onLas a 2-adic digit sequence rather than onL_headalone — 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 patternR[k] = 2k−1·(2a + 1)for1 ≤ 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 existingmulti_bounce_general/shift_to_macro_progclosure 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.