Erdős Problem 349

Reference: erdosproblems.com/349

def Erdos349.IsGoodPair (t α : ℝ) : Prop

This defines the core property of the problem: For what values of $t,\alpha \in (0,\infty)$ is the sequence $\lfloor t\alpha^n\rfloor$ complete?

Equations

• Erdos349.IsGoodPair t α = IsAddComplete (Set.range fun (n : ℕ) => ⌊t * α ^ n⌋)

theorem Erdos349.erdos_349 : {(t, α) : ℝ × ℝ | 0 < t ∧ 0 < α ∧ IsGoodPair t α} = sorry

For what values of $t,\alpha \in (0,\infty)$ is the sequence $\lfloor t\alpha^n\rfloor$ complete (that is, all sufficiently large integers are the sum of distinct integers of the form $\lfloor t\alpha^n\rfloor$)?

theorem Erdos349.complete_for_alpha_in_Ioo_one_to_goldenRatio (t α : ℝ) (ht : 0 < t) (hα : α ∈ Set.Ioo 1 ((1 + √5) / 2)) : IsGoodPair t α

It seems likely that the sequence is complete for all for all $t>0$ and all $1 < \alpha < \frac{1+\sqrt{5}}{2}$.

theorem Erdos349.exists_t_for_k_disjoint_segments (k : ℕ) : ∃ t ∈ Set.Ioo 0 1, ∃ (ι : Type), ↑k ≤ Set.univ.encard ∧ ∃ (I : ι → Set ℝ), (∀ (i : ι), 2 ≤ (I i).encard ∧ (I i).Nonempty ∧ IsConnected (I i)) ∧ Pairwise (Function.onFun Disjoint I) ∧ ⋃ (i : ι), I i ⊆ {α : ℝ | α > 0 ∧ IsGoodPair t α}

For any $k$ there exists some $t_k\in (0,1)$ such that the set of $\alpha$ such that the sequence $\lfloor t_k\alpha^n\rfloor$ is complete consists of at least $k$ disjoint line segments.

theorem Erdos349.erdos_349.variants.floor_3_halves_odd : sorry ↔ {n : ℕ | Odd ⌊(3 / 2) ^ n⌋}.Infinite

Is it true that the terms of the sequence $\lfloor (3/2)^n\rfloor$ are odd infinitely often and even infinitely often?

theorem Erdos349.erdos_349.variants.floor_3_halves_even : sorry ↔ {n : ℕ | Even ⌊(3 / 2) ^ n⌋}.Infinite

Is it true that the terms of the sequence $\lfloor (3/2)^n\rfloor$ are even infinitely often?

theorem Erdos349.alpha_gt_two_not_isGoodPair (t α : ℝ) (ht : 0 < t) (hα : 2 < α) : ¬IsGoodPair t α

For $\alpha > 2$ and any $t > 0$, the sequence $\lfloor t\alpha^n\rfloor$ is not additively complete; equivalently $(t, \alpha)$ is not a "good pair". A partial result on the open Erdős Problem 349: it complements complete_for_alpha_in_Ioo_one_to_goldenRatio.

The proof is recorded via the formal_proof mechanism rather than written inline, as it exceeds the repository's proof-length guideline.

theorem Erdos349.alpha_le_one_not_isGoodPair (t α : ℝ) (ht : 0 < t) (hα0 : 0 < α) (hα1 : α ≤ 1) : ¬IsGoodPair t α

For $0 < \alpha \le 1$ and any $t > 0$, $(t, \alpha)$ is not a good pair: every term $\lfloor t\alpha^n\rfloor$ lies in the finite interval $[0, \lfloor t\rfloor]$ (since $\alpha^n \le 1$), so every subset sum is bounded by the constant $\sum_{i \in [0,\lfloor t\rfloor]} i$, and no large integer can be a subset sum. A partial result on the open Erdős Problem 349, complementing the $2 < \alpha$ and integer-coefficient cases.

theorem Erdos349.exists_finset_sum_two_pow (k : ℕ) : ∃ (E : Finset ℕ), k = ∑ i ∈ E, 2 ^ i

Binary expansion. Every natural number $k$ is a sum of distinct powers of two: there is a finite set $E$ of exponents with $k = \sum_{i \in E} 2^i$. Proved by strong induction: subtract the largest power $2^m \le k$, recurse on the remainder.

theorem Erdos349.one_two_isGoodPair : IsGoodPair 1 2

The pair $(1, 2)$ is good. The powers of two $\lfloor 1\cdot 2^n\rfloor = 2^n$ form an additively complete set: every $k \ge 1$ is a finite sum of distinct powers of two.

theorem Erdos349.dyadic_two_isGoodPair (k : ℕ) : IsGoodPair (1 / 2 ^ k) 2

The dyadic fiber at $\alpha = 2$. For every $k$, the pair $(1/2^k, 2)$ is good: the sequence $\lfloor 2^n / 2^k\rfloor$ is additively complete because at index $n = m + k$ it equals the exact power $2^m$, so its range contains all powers of two, which already form an additively complete set. Uses monotonicity IsAddComplete.mono.

theorem Erdos349.int_coeff_ge_two_not_isGoodPair (t : ℤ) (ht : 2 ≤ t) (α : ℤ) : ¬IsGoodPair ↑t ↑α

Integer leading coefficient $t \ge 2$ blocks completeness. For every integer base $\alpha$, the pair $(t, \alpha)$ with integer $t \ge 2$ is not good: $\lfloor t\alpha^n\rfloor = t\alpha^n$ is a multiple of $t$, so every subset sum is too, but two consecutive large integers cannot both be multiples of $t$. Generalizes the parity obstruction ($t = 2$). A partial result on Erdős Problem 349.

theorem Erdos349.integer_isGoodPair_iff (t α : ℤ) (ht : 1 ≤ t) (hα : 1 ≤ α) : IsGoodPair ↑t ↑α ↔ t = 1 ∧ α = 2

Erdős Problem 349, complete characterization on positive integer pairs. For integers $t \ge 1$, $\alpha \ge 1$, the pair $(t, \alpha)$ is good (i.e. $\lfloor t\alpha^n\rfloor$ is additively complete) iff $(t, \alpha) = (1, 2)$. Assembles the four partial results: $(1,2)$ is good, $\alpha \le 1$ fails, $2 < \alpha$ fails (alpha_gt_two_not_isGoodPair), and integer $t \ge 2$ fails.