# A quadratic bound for Jacobsthal’s function

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A quadratic bound for Jacobsthal's function](../../preprints/A-quadratic-bound-for-Jacobsthals-function-September-25-2026/paper.pdf)

## Scope

Let $h(k)$ be the least interval length that guarantees an integer coprime to any prescribed positive modulus with at most $k$ distinct prime factors. The formalization proves the paper's strengthened Jacobsthal bound $h(k)\le Ck^2/(\log\log(3k))^2$ for one absolute $C>0$ and every $k\ge1$. Intervals may begin at any signed integer. The earlier quadratic bound is also retained as a separate statement; the optimal order of growth is not determined.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Quadratic Jacobsthal bound | [Jacobsthal.lean](../ComparatorChallenges/Jacobsthal.lean) |
| Jacobsthal bound with an iterated-logarithm saving | [JacobsthalImproved.lean](../ComparatorChallenges/JacobsthalImproved.lean) |