The rest of `cP2E` (`rest_le`)

Proved

NLogN.KFUU.R6Crt.rest_le

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

complexity-theoryinteger-multiplicationkappa-improvement

The rest of cP2E.

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

theorem NLogN.KFUU.R6Crt.rest_le (h d w Z VT p T : ℕ) (hVT : VT = 2 * T) (hw : w = p + 2) (hp : 6 ≤ p)
    (hZ : Z ≤ 3 * p) (hdh : d + 1 ≤ 2 ^ h)
    (hT : (d + 2) * (CU * (Z + 1) ^ 2 + 5 * Z + 10 ^ 4) ≤ T) :
    cRest h d w Z VT ≤ 10 ^ 13 * ((d + 1) * T * p)

Context. CRT reversal §11: the cost arithmetic

cFwdE_nat, cBwdE_nat: the cost of phiFE / phiBE is at most the frozen natCost (the part of KFUU's Φ other than its phase-2 swaps) plus cP2E.
cP2E_split: cP2E = rest + 3 ⌈cSwNτ …⌉.
T0_le, rest_le: with V_T = 2T, w = p + 2, d + 1 ≤ 2^h and T large, both nat parts are O((d+1) T p).
swapE_le: one composite swap costs ≤ 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*).

Preamble

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

import Definitions.Def_IntMul_Kappa_R6_Defs14

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFUU NLogN.KFUU.R6Crt
open IntMul NLogN.KIL NLogN.KFB NLogN.KFC NLogN.KFT NLogN.KFU AModel AModelL12 NLogN.KFUU

Formal statement

theorem NLogN.KFUU.R6Crt.rest_le (h d w Z VT p T : ℕ) (hVT : VT = 2 * T) (hw : w = p + 2) (hp : 6 ≤ p)
    (hZ : Z ≤ 3 * p) (hdh : d + 1 ≤ 2 ^ h)
    (hT : (d + 2) * (CU * (Z + 1) ^ 2 + 5 * Z + 10 ^ 4) ≤ T) :
    cRest h d w Z VT ≤ 10 ^ 13 * ((d + 1) * T * p) := 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 `NLogN.KFUU.R6Crt.rest_le`, Solutions/R6CrtCost.lean (lines 124–202) of the round-six development.

View graph