Mark OEIS A078590 as solved

[KitaKen1]

This PR changes OeisA78590.conjecture from a positive research open proposition to an answer(False) statement and links a kernel-checked Lean counterexample.

The Lean formalization was prepared by KitaKen1 (Kenta Kitamura).

The external proof establishes the exact corrected target theorem:

theorem OeisA78590Counterexample.oeis_A078590_solved :
    answer(False) ↔ ∀ n : ℕ, 3 ≤ n →
      OeisA78590.a (n - 2) ∣ 2 ^ OeisA78590.a (n - 1) + 1

Proof: https://github.com/KitaKen1/oeis-a078590-counterexample/blob/3bdf1cee8e7e4cbc4fe83354e4be8ca1eee46de3/lean/OeisA78590CounterexampleFC.lean#L55-L61

Repository: https://github.com/KitaKen1/oeis-a078590-counterexample

Lean4Web: https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2FKitaKen1%2Foeis-a078590-counterexample%2Frefs%2Fheads%2Fmain%2Flean4web%2FOeisA78590CounterexampleLean4Web.lean

#print axioms reports only propext, Classical.choice, and Quot.sound; there is no sorryAx.

AI Usage Disclosure: This formalization was developed with assistance from OpenAI Codex.