Round-six lemma `crt_big`
ProvedIntMul.Kappa.R6.crt_bigAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.R6CrtNeed):
theorem IntMul.Kappa.R6.crt_big (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → CrtBig P n
Context. CRT reversal §12: CrtNeed6
crtNeed6 : ∀ P, P.Ok → CrtNeed6 P.
The table is mTab4 tab ext₁ ext0 ext0 ext0 own with ext₁ the table of IL.SwapNeedτ tab P.τ
and own = [phiFE, phiBE] (KFUU's uniform Φ, Φ⁻¹ with the reversal revE, whose phase 2 uses
three composite swaps of h⌊d/2⌋-bit digits and six digit-selector rotation sets instead of
KFUU's ⌊d/2⌋ single-digit swaps). RowUCP is not used.
Cost: c ≤ C₀ · T p · Ncost6 with A = 0, from
- the frozen part (
natCost,O((d+1) T p)onced + 1 ≤ 2^h), - the rest of
p2E(O((d+1) T p)onced + 1 ≤ 2^handT ≥ poly(b)), - three composite swaps, each
≤ K (4 T p ℓ (d ln p)^τ + 96 T p).
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_Defs15 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open IntMul IntMul.Kappa IntMul.Kappa.R6 open IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFM AModel NLogN.KFUU NLogN.KFUU.R6Crt NLogN.KFU
theorem IntMul.Kappa.R6.crt_big (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → CrtBig P n := by sorry