The greedy step, with abstract parameters (`step_core`)

Proved

J6Sieve.step_core

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

complexity-theoryinteger-multiplicationkappa-improvement

The greedy step, with abstract parameters.

The following holds (Lean statement, in the scope of module Solutions.J6SieveStep):

theorem J6Sieve.step_core (z Ω k m H A : ℕ) (Q : Finset ℕ) (hzΩn : z = 4 * (Ω + 1))
    (hk : z < 2 ^ k) (hmk : m = 4 * k + 3) (hQp : ∀ q ∈ Q, q.Prime)
    (hQz : ∀ q ∈ Q, q ∉ P z) (hQc : Q.card ≤ Ω + 1)
    (hH : 2 * z * (Ω + 2) * (m + 2) * z ^ (m + 1) < H) :
    ∃ n, A < n ∧ n ≤ A + H ∧ rough z n ∧ ∀ q ∈ Q, ¬ q ∣ n

Context. J6Sieve, part 3: one greedy step

If Q is a set of at most Ω + 1 primes, all > z = 4(Ω+1), and H exceeds the explicit bound, then every interval (A, A+H] contains a z-rough integer divisible by no element of Q.

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.step_core (z Ω k m H A : ℕ) (Q : Finset ℕ) (hzΩn : z = 4 * (Ω + 1))
    (hk : z < 2 ^ k) (hmk : m = 4 * k + 3) (hQp : ∀ q ∈ Q, q.Prime)
    (hQz : ∀ q ∈ Q, q ∉ P z) (hQc : Q.card ≤ Ω + 1)
    (hH : 2 * z * (Ω + 2) * (m + 2) * z ^ (m + 1) < H) :
    ∃ n, A < n ∧ n ≤ A + H ∧ rough z n ∧ ∀ q ∈ Q, ¬ q ∣ n := 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.step_core`, Solutions/J6SieveStep.lean (lines 76–185) of the round-six development.

View graph