The frozen part (`T0_le`)

Proved

NLogN.KFUU.R6Crt.T0_le

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

complexity-theoryinteger-multiplicationkappa-improvement

The frozen part.

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

theorem NLogN.KFUU.R6Crt.T0_le (w d h VT VS PM Bb p T : ℕ) (hVT : VT = 2 * T) (hw : w = p + 2) (hp : 6 ≤ p)
    (hVS : VS ≤ VT) (hsz : h + Nat.size VS + 3 ≤ 2 * p) (hBb : Bb + 2 ≤ p)
    (hPM : PM * 2 ^ h ≤ 2 * T) (hdh : d + 1 ≤ 2 ^ h) (hpT : p ≤ T) :
    (d + 1) * cScan VT w + (d + 1) * (h + w + Nat.size VS + 1) ^ 2 + d * cRb d w VS PM Bb ≤
      10 ^ 6 * ((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_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

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

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

Formal statement

theorem NLogN.KFUU.R6Crt.T0_le (w d h VT VS PM Bb p T : ℕ) (hVT : VT = 2 * T) (hw : w = p + 2) (hp : 6 ≤ p)
    (hVS : VS ≤ VT) (hsz : h + Nat.size VS + 3 ≤ 2 * p) (hBb : Bb + 2 ≤ p)
    (hPM : PM * 2 ^ h ≤ 2 * T) (hdh : d + 1 ≤ 2 ^ h) (hpT : p ≤ T) :
    (d + 1) * cScan VT w + (d + 1) * (h + w + Nat.size VS + 1) ^ 2 + d * cRb d w VS PM Bb ≤
      10 ^ 6 * ((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.T0_le`, Solutions/R6CrtCost.lean (lines 74–122) of the round-six development.

View graph