The sieve window condition holds for large `n` (`winOK_eventually`)
ProvedIntMul.Kappa.R6.winOK_eventuallyThe sieve window condition holds for large n.
The following holds (Lean statement, in the scope of module Solutions.R6SMath):
theorem IntMul.Kappa.R6.winOK_eventually (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → WinOK6 P n
Context. Round-six setup, part 1: the sources by search, and the counted parameters
The setup machine picks the source s_j of axis j by scanning the candidates
c = A_j + x (A_j = t_j - 2 w_j, x = w_j, w_j - 1, …, 1) and keeping the last one coprime to
2 ∏_{i<j} s_i (pick, src6). The sieve (J6SieveStep.step) shows that a coprime candidate
exists once w_j > sieveBound d r (exists_cop), which holds for large n
(ell_big: ℓ ≥ C (log₂ b + 1)^2 eventually). Then src6 satisfies SrcOK6
(src6_ok).
The parameters d, L, α are computed by the machine as counts (d_count6, L_count6,
α_count6).
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_R6_Defs63 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open IntMul IntMul.Kappa IntMul.Kappa.R6 open IntMul NLogN NLogN.KFM Finset
theorem IntMul.Kappa.R6.winOK_eventually (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → WinOK6 P n := by sorry