Erdős Problem 317

Reference: erdosproblems.com/317

theorem Erdos317.erdos_317 : (∃ (c : ℝ), c > 0 → ∀ n ≥ 1, ∃ (δ : Fin n → ℚ), δ '' Set.univ ⊆ {-1, 0, 1} ∧ 0 < |∑ k : Fin n, ↑(δ k) / (↑↑k + 1)| ∧ |∑ k : Fin n, ↑(δ k) / (↑↑k + 1)| < c / 2 ^ n) ↔ sorry

Is there some constant $c>0$ such that for every $n\geq 1$ there exists some $\delta_k\in \{-1,0,1\}$ for $1\leq k\leq n$ with [0< \left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert < \frac{c}{2^n}?]

theorem Erdos317.erdos_317.variants.claim2 : (∀ᶠ (n : ℕ) in Filter.atTop, ∀ (δ : Fin n → ℚ), δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k : Fin n, δ k / (↑↑k + 1)| ≠ 0 → |∑ k : Fin n, δ k / (↑↑k + 1)| > 1 / ↑((Finset.Icc 1 n).lcm id)) ↔ sorry

Is it true that for sufficiently large $n$, for any $\delta_k\in \{-1,0,1\}$, [\left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert > \frac{1}{[1,\ldots,n]}] whenever the left-hand side is not zero?

theorem Erdos317.claim2_inequality : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (δ : Fin n → ℚ), δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k : Fin n, δ k / (↑↑k + 1)| ≠ 0 → |∑ k : Fin n, δ k / (↑↑k + 1)| ≥ 1 / ↑((Finset.Icc 1 n).lcm id)

Inequality in erdos_317.variants.claim2 is obvious, the problem is strict inequality.

theorem Erdos317.erdos_317.variants.counterexample : ¬∀ (δ : Fin 4 → ℚ), δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k : Fin 4, δ k / (↑↑k + 1)| ≠ 0 → |∑ k : Fin 4, δ k / (↑↑k + 1)| > 1 / ↑((Finset.Icc 1 4).lcm id)

erdos_317.variants.claim2 fails for small $n$, for example [\frac{1}{2}-\frac{1}{3}-\frac{1}{4}=-\frac{1}{12}.]