Erdős Problem 477

Reference: erdosproblems.com/477

theorem Erdos477.erdos_477 : (∀ (f : Polynomial ℤ), 2 ≤ f.degree → ∃ (A : Set ℤ), ∀ (z : ℤ), ∃! a : ℤ × ℤ, a ∈ A ×ˢ ((fun (a : ℤ) => Polynomial.eval a f) '' {n : ℤ | 0 < n}) ∧ z = a.1 + a.2) ↔ sorry

Let $f:\mathbb{Z}\to \mathbb{Z}$ be a polynomial of degree at least $2$. Is there a set $A$ such that every $z\in \mathbb{Z}$ has exactly one representation as $z=a+f(n)$ for some $a\in A$ and $n > 0$?

theorem Erdos477.erdos_477.variants.strong_negation (f : Polynomial ℤ) (hf₀ : 2 ≤ f.degree) : ¬∃ (A : Set ℤ), ∀ (z : ℤ), ∃! a : ℤ × ℤ, a ∈ A ×ˢ ((fun (a : ℤ) => Polynomial.eval a f) '' {n : ℤ | 0 < n}) ∧ z = a.1 + a.2

Probably there is no such $A$ for any polynomial $f$.