Alternating sum of signs of powers of 3/2

The question

conjecture2. For $n$ large enough, does $a(n)>\sqrt{n}$ always hold?

conjecture3. Conjecture: asymptotically, $a(n)\sim C\log (n{)}^2$ for some constant $C>0$.

conjecture3_value. Conjecture: the constant $C$ in $a(n)\sim C\log (n{)}^2$ is approximately $1.4$.

The sequence $a(n)=-{\sum }_{k=1}^n(-1{)}^{\lfloor (3/2{)}^k\rfloor }$.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.OEIS.«71532» (3 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem conjecture2 :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → (a n : ℝ) > Real.sqrt (n : ℝ)

theorem conjecture3 :
    ∃ C : ℝ, 0 < C ∧ (fun n : ℕ ↦ (a n : ℝ)) ~[atTop] (fun n : ℕ ↦ C * Real.log (n : ℝ) ^ 2)

theorem conjecture3_value :
    let C : ℝ := answer(sorry)
    |C - 1.4| < 0.1 ∧
      (fun n : ℕ ↦ (a n : ℝ)) ~[atTop] (fun n : ℕ ↦ C * Real.log (n : ℝ) ^ 2)

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

• A071532

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.