1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB---
Jump to navigation
Jump to search
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, and an alternative proof is underway by Autumn Pan.