Busy Beaver Challenge: Antihydra

Reference: bbchallenge

theorem busy_beaver_antihydra (a : ℕ → ℕ) (b : ℕ → ℤ) (a_ini : a 0 = 8) (a_rec : ∀ (n : ℕ), a (n + 1) = 3 * a n / 2) (b_ini : b 0 = 0) (b_rec : ∀ (n : ℕ), b (n + 1) = if a n % 2 = 0 then b n + 2 else b n - 1) (n : ℕ) : b n ≥ 0

Antihydra is a sequence starting at 8, and iterating the function $$H(n) = \left\lfloor \frac {3n}2 \right\rfloor.$$ The conjecture states that the cumulative number of odd values in this sequence is never more than twice the cumulative number of even values

It is a relatively new open problem with, so it might be solvable, although seems quite hard. It is equivalent to non-termination of a particular 6-state turing machine.

theorem busy_beaver_antihydra.variants.set (a : ℕ → ℕ) (a_ini : a 0 = 8) (a_rec : ∀ (n : ℕ), a (n + 1) = 3 * a n / 2) (n : ℕ) : (Finset.filter (fun (x : ℕ) => Odd (a x)) (Finset.Ico 0 n)).card ≤ 2 * (Finset.filter (fun (x : ℕ) => Even (a x)) (Finset.Ico 0 n)).card

Alternative statement of busy_beaver_antihydra using set size comparison instead of a recurrent sequence b.