1RB1LA 1RC1RE 1LD0RB 1LA0LC 0RF0RD 0RB---: Difference between revisions
Jump to navigation
Jump to search
Added categories |
|||
| Line 1: | Line 1: | ||
{{machine|1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB---}} | |||
{{TM|1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB---|undecided}} is a [[BB(6)]] holdout. | {{TM|1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB---|undecided}} is a [[BB(6)]] holdout. | ||
| Line 15: | Line 16: | ||
= Further Analysis (Pomme, Autumn Pan, et al.) = | = 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. | 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. | ||
[[Category:BB(6)]] | |||
Latest revision as of 10:19, 29 November 2025
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.