Mark OEIS A185895 conjecture3 as solved

[KitaKen1]

This PR changes OeisA185895.conjecture3 from research open to research solved and links a kernel-checked Lean 4 proof.

It leaves the separate sign-change conjectures OeisA185895.conjecture1 and OeisA185895.conjecture2 open.

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

The external proof establishes the exact target theorem:

theorem OeisA185895Proof.conjecture3_solved (p : ℕ) (hp : p.Prime) (n k : ℕ)
    (hn : 0 < n) (hk : 0 < k) :
    OeisA185895.a (n * p ^ k) ≡
      OeisA185895.a (n * p ^ (k - 1)) [ZMOD (p : ℤ) ^ k]

Proof: https://github.com/KitaKen1/oeis-a185895-conjecture3/blob/e40e3db2b47beeef22b00a481fc3a41b518168d9/lean/OeisA185895Conjecture3FC.lean#L579-L589

Repository: https://github.com/KitaKen1/oeis-a185895-conjecture3

Lean4Web: https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2FKitaKen1%2Foeis-a185895-conjecture3%2Frefs%2Fheads%2Fmain%2Flean4web%2FOeisA185895Conjecture3Lean4Web.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.