Jacobsthal's problem ([I78])

Iwaniec's application of the linear sieve: if m consecutive integers are each divisible by one of r ≥ 2 given primes, then m ≪ (r log r)². The shifted sieve ([I78, Lemma 1], Jacobsthal/ShiftedSieve.lean) transfers the Rosser weights for the first r primes to any r primes; Jacobsthal/Reduction.lean combines it with linearSieveEstimate.

This port preserves the dependency closure of the corollary. The upstream repository also formalizes other results of [I78], which are outside this import's scope.

The sieve definitions, statements and proofs were produced by AI agents under Jason Davies's supervision. The vendored strong PNT proofs come from PrimeNumberTheoremAnd and its contributors; their upstream revision is recorded in the project card and each vendor module.

theorem IwaniecLinearSieve.iwaniecBound : ∃ (C : ℝ), ∀ (S : Finset ℕ), (∀ p ∈ S, Nat.Prime p) → 2 ≤ S.card → ∀ (x : ℤ) (m : ℕ), (∀ k < m, ∃ p ∈ S, ↑p ∣ x + ↑k) → ↑m ≤ C * (↑S.card * Real.log ↑S.card) ^ 2

Iwaniec's theorem ([I78, Corollary]): if m consecutive integers are each divisible by one of r ≥ 2 given primes, then m ≪ (r log r)².