Pairwise coprime odd numbers in short windows

Proved

J6Sieve.exists_coprime_in_windows

by xuanji · Oct 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

Let $d, X, H \in \mathbb N$ and let $A_0, \dots, A_{d-1}$ be natural numbers with $A_i + H \le X$ . If $H$ exceeds the explicit sieve bound $\mathrm{sieveBound}(d, X)$ , then one can choose odd numbers $s_i$ with $A_i < s_i \le A_i + H$ that are pairwise coprime:

\exists s,\ \big(\forall i,\ s_i \text{ odd},\ A_i < s_i \le A_i + H\big) \wedge \big(\forall i \ne j,\ \gcd(s_i, s_j) = 1\big).

The numbers $s_i$ serve as pairwise coprime moduli for the CRT steps of the round-six stack; the proof is a Brun pure sieve combined with a greedy choice.

In Lean:

theorem J6Sieve.exists_coprime_in_windows (d X H : ℕ) (A : Fin d → ℕ) (hA : ∀ i, A i + H ≤ X)
    (hH : sieveBound d X < H) :
    ∃ s : Fin d → ℕ, (∀ i, Odd (s i) ∧ A i < s i ∧ s i ≤ A i + H) ∧
      Pairwise (fun i j => Nat.Coprime (s i) (s j))

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs1

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Sieve
open Finset

Formal statement

theorem J6Sieve.exists_coprime_in_windows (d X H : ℕ) (A : Fin d → ℕ) (hA : ∀ i, A i + H ≤ X)
    (hH : sieveBound d X < H) :
    ∃ s : Fin d → ℕ, (∀ i, Odd (s i) ∧ A i < s i ∧ s i ≤ A i + H) ∧
      Pairwise (fun i j => Nat.Coprime (s i) (s j)) := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `J6Sieve.exists_coprime_in_windows`, Solutions/J6Sieve.lean (lines 77–93) of the round-six development.

View graph