Source labels openChecked July 26, 2026

Bugeaud Collection of Conjectures and Open Questions: Lacunary Sequences in Real Number Fields

Mathematical statement

Problem 10.5 ("moreover" clause). With the same hypotheses as problem_10_5, the sequence $(t_n)$ can be chosen so that, for any real $\xi$ not in $\mathbb{K}$ , each subinterval of $[0, 1]$ of length $\varepsilon$ contains a limit point of the sequence $(\{\xi t_n\})_{n \ge 1}$ . This is strictly stronger than problem_10_5: the limsup bound is the special case at the subinterval $[1 - \varepsilon, 1]$ .

Statement source: Books statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

problem_10_5_moreover

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem problem_10_5_moreover (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ K]    {ε : ℝ} (hε : 0 < ε) :    ∃ t : ℕ → K, (∀ n, 0 < (t n : ℝ)) ∧      IsLacunaryReal (fun k => (t k : ℝ)) ∧      ∀ ξ : ℝ, ξ ∉ K → ∀ a, a ∈ Set.Icc (0 : ℝ) (1 - ε) →        ∃ y ∈ Set.Icc a (a + ε),          MapClusterPt y atTop (fun n => Int.fract (ξ * (t n : ℝ))) := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization