Mark the literal Erdős 367 higher-full-parts variant false

[KitaKen1]

This PR changes Erdos367.erdos_367.variants.higher_full_parts from answer(sorry) to answer(False), marks it research solved, and links a kernel-checked Lean 4 proof.

It leaves Erdos367.erdos_367.parts.i and Erdős Problem 367 overall open. It also does not settle the corrected existential-ε formulation (∃ ε > 0); the result here concerns the literal current target with ∀ ε > 0.

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

The counterexample specializes the universal statement to (r, k, ε) = (3, 2, 2). Since B r m ∣ m, the normalized product is eventually bounded by the finite value 2, so its EReal limsup is not ⊤.

Proof: https://github.com/KitaKen1/erdos-367-higher-full-parts/blob/560d371b5d4fece41079d457f8f0306d0991554f/lean/Erdos367HigherFullPartsFC.lean#L16-L80

Repository: https://github.com/KitaKen1/erdos-367-higher-full-parts

Lean4Web: https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2FKitaKen1%2Ferdos-367-higher-full-parts%2Frefs%2Fheads%2Fmain%2Flean4web%2FErdos367HigherFullPartsLean4Web.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.