beaver_math_olympiad_problem_4

[BMO#4](https://wiki.bbchallenge.org/wiki/Beaver_Math_Olympiad#4._1RB3RB---1LB0LA_2LA4RA3LA4RB1LB_(bbch)) Bonnie the beaver was bored, so she tried to construct a sequence of integers $\{a_n\}_{n \ge 0}$. She first defined $a_0=2$, then defined $a_{n+1}$ depending on $a_n$ and $n$ using the following rules: * If $a_n \equiv 0\text{ (mod 3)}$, then $a_{n+1}=\frac{a_n}{3}+2^n+1$. * If $a_n \equiv 2\text{ (mod 3)}$, then $a_{n+1}=\frac{a_n-2}{3}+2^n-1$. With these two rules alone, Bonnie calculates the first few terms in the sequence: $2, 0, 3, 6, 11, 18, 39, 78, 155, 306, \dots$. At this point, Bonnie plans to continue writing terms until a term becomes $1\text{ (mod 3)}$. If Bonnie sticks to her plan, will she ever finish? [BMO#4](https://wiki.bbchallenge.org/wiki/Beaver_Math_Olympiad#4._1RB3RB---1LB0LA_2LA4RA3LA4RB1LB_(bbch)) is equivalent to the non-termination of 2-state 5-symbol Turing machine [`1RB3RB---1LB0LA_2LA4RA3LA4RB1LB`](https://wiki.bbchallenge.org/wiki/1RB3RB---1LB0LA_2LA4RA3LA4RB1LB) (from all-0 tape). The machine was informally proven not to halt [bbchallenge.org](bbchallenge.org) contributor Daniel Yuan on July 19th 2024; see [sketched proof](https://wiki.bbchallenge.org/wiki/1RB3RB---1LB0LA_2LA4RA3LA4RB1LB) and [Discord discussion](https://discord.com/channels/960643023006490684/960643023530762343/1263666591900631210).

theorem beaver_math_olympiad_problem_4
    (a : ℕ → ℕ)
    (a_ini : a 0 = 2)
    (a_rec : ∀ n, a (n+1)
      = if a n % 3 = 0 then a n / 3 + 2 ^ n + 1 else (a n - 2) / 3 + 2 ^ n - 1) :
    ¬ (∃ n, a n % 3 = 1)

Recent Submissions

No submissions yet. Be the first to attempt this problem.