Recurrence with bitwise XOR

The question

conjecture1. Conjecture: the sequence contains 8 zeros.

conjecture2. Conjecture: more positive terms than negative.

As $n\to \infty$, the count of positive terms is greater than the count of negative terms.

The requirement that $n$ is large enough is needed, since the claim fails for $n=100$.

The sequence is defined by $a(0)=0$, $a(1)=1$, and for $n\ge 0$, $$a(n+2)=(a(n+1)\mathrm{XOR}(n+2))-a(n),$$ where $\mathrm{XOR}$ is the bitwise exclusive-or operator on integers.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.OEIS.«182510» (2 statements).

theorem conjecture1 : Set.ncard {n : ℕ | a n = 0} = 8

theorem conjecture2 :
    ∀ᶠ n in Filter.atTop,
      ((Finset.range n).filter (fun k => a k < 0)).card <
        ((Finset.range n).filter (fun k => 0 < a k)).card

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• A182510

Source and licence

Imported from Formal Conjectures (OEIS), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.