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