`ℓ ≥ C (log₂ b + 1)^2` for large `n` (round six, `ell_big`)
ProvedIntMul.Kappa.R6.ell_bigℓ ≥ C (log₂ b + 1)^2 for large n.
The following holds (Lean statement, in the scope of module Solutions.R6SMath):
theorem IntMul.Kappa.R6.ell_big (P : Prm) (hP : P.Ok) (C : ℕ) :
∃ n₁ : ℕ, ∀ n, n₁ ≤ n → C * (Nat.log 2 (bP6 n) + 1) ^ 2 ≤ ℓP6 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_K_Defs33 import Definitions.Def_IntMul_Kappa_R6_Defs1 import Mathlib import Definitions.Def_IntMul_HvdH_M_Defs8 import Definitions.Def_IntMul_MultitapeModel import Definitions.Def_IntMul_HvdH_Numeric import Definitions.Def_IntMul_HvdH_ExpApprox import Definitions.Def_IntMul_HvdH_Twiddle import Definitions.Def_IntMul_HvdH_RealExp import Definitions.Def_IntMul_HvdH_MachineRef import Definitions.Def_IntMul_HvdH_SApprox import Definitions.Def_IntMul_HvdH_DiagApprox import Definitions.Def_IntMul_HvdH_EApprox import Definitions.Def_IntMul_HvdH_JApprox import Definitions.Def_IntMul_HvdH_BApprox import Definitions.Def_IntMul_HvdH_FPApprox import Definitions.Def_IntMul_KappaFramework import Definitions.Def_IntMul_KappaJainData 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.ell_big (P : Prm) (hP : P.Ok) (C : ℕ) :
∃ n₁ : ℕ, ∀ n, n₁ ≤ n → C * (Nat.log 2 (bP6 n) + 1) ^ 2 ≤ ℓP6 P n := by sorry