1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB---

1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB--- (bbch) is a BB(6) holdout.

Analysis by mxdys

https://discord.com/channels/960643023006490684/1239205785913790465/1441124403801755730

1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB---

start: S(18)

S(n) --> S((n+(3^i*6+i+4))/2), n mod 2 = i mod 2, 3^i*2-i-2 <= n <= 3^i*6-i-6
S(n) --> S(3^i*12-1), n mod 2 = (i+1) mod 2, 3^i*2-i <= n <= 3^i*6-i-10

These rules are closed if

(3^i*2+i+5)/(2^v2(3^i*2+i+5))>=2i+14 for all i>=50 

Further Analysis (Pomme, Autumn Pan, et al.)

Although it has not been proven in Rocq, it is known that the inequality holds. This has been proven informally by Pomme, though it references an external paper which makes it difficult to prove using computer proof assistants. Simulators written by Autumn Pan, Pomme, and vyx7 were used to verify the inequality for all $50\le i\le 10^{660}$.

Formal proofs by Opus 4.6/DrDisentangle

Lean files for both the rules and the proof of the inequality dependent on the well-known Baker–Wüstholz theorem as axiom are in https://github.com/rwst/bbchallenge/tree/main/1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB---. That axiom can only be removed when Baker's theorems are formalized in Lean. There are no doubts that they are true, however.

Proof of Inequality

The proof follows the path laid out by Pomme, but diverges by using Baker–Wüstholz instead of Baker, thereby lowering the amount of computation necessary. By using Hensel lift/shift, mathematical proof replaces computation that would have needed CPU years. Following is a more detailed outline, please refer to the Lean files for the ultimate details.

Path to the Inequality

The TM is macro-simulated using three families of configurations $S_1(a,b,c)$, $S_2(a,b)$, and $S_3(a,b)$ that all reach state C with a characteristic zebra pattern on the right tape and blocks of 1s on the left. From these configurations, two macro-rules emerge (BigStep0' and BigStep1' in machine.lean)

• BigStep0' at level $i$: when the parameter $n$ lies in a specific R1 window around $3^i\cdot 3+O(i)$, the machine performs a large but predictable number of steps and produces a new parameter $(n+6\cdot 3^i+i+4)/2$.
• BigStep1' sends states in the complementary R2 window to a fixed entry point for level $i+1$.

Analysis of the iterated application of BigStep0' reveals that the distance from the fixed point $C(i)=6\cdot 3^i+i+4$ is repeatedly halved. After exactly $v_2(N(i))$ halvings (where $N(i)=2\cdot 3^i+i+5$), the resulting state lands precisely at the upper edge of the R1 window for level $i$.

For the trajectory to stay inside the safe windows forever (never escaping the macro-loop that would allow halting), the halved distance must remain large enough that the final state after $v_2(N(i))$ steps still satisfies the R2 upper bound. This translates directly into the requirement that the odd part of $N(i)$ (i.e. $N(i)/2^{v_2(N(i))}$) exceeds $2i+14$. If it were smaller, the parameter would undershoot the valid window, breaking the invariant and potentially allowing the machine to reach a halting state.

Solving the Inequality

Let $N(i)=2\cdot 3^i+i+5$, then we need to show the odd part of it exceeds $2i+14$ for all $i$. The easy case is when $i$ is even: then $N(i)$ is already odd, and $N(i)\ge 2i+14$ is trivially true. We focus on odd $i$ which makes $N(i)$ even, with an unknown even part of the form $2^{v_2(N(i))}$, and $v_2(N(i))$ might be large. We must prove it cannot be too large. This is done in three ranges of $i$:

• $i<50$, by direct computation inside the Lean proof;
• $50\le i\le 2^{60}$, by $p$-adic analysis (Hensel's lemma for lifting solutions of congruences modulo higher and higher powers of 2, combined with the Lifting-The-Exponent lemma); and
• $i>2^{60}$, using a stronger version of Baker's theorem on linear forms in logarithms, specifically the Baker–Wüstholz theorem. This gives a lower bound on how close $2\cdot 3^i$ can be to a multiple of $2^k$.

Why is that axiom not formalized?

The Baker–Wüstholz theorem belongs in Transcendental number theory, an advanced and difficult subfield of number theory. Lean's Mathlib can be considered the most complete library of formalizations of number theory theorems, but even it struggles to include all the advanced math that is out there on paper. Accelerated production of formalizations using AI does not necessarily propagate to Mathlib because of the human review bottleneck. For example, the related Gelfond-Schneider theorem is stuck in the PR queue since Feb-2026. Baker–Wüstholz would need additional substantial Mathlib infrastructure before the proof can be formalized and submitted.