The truncation and its frame (round six, `cTr_U`)

Proved

NLogN.KFW.cTr_U

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

complexity-theoryinteger-multiplicationkappa-improvement

The truncation and its frame.

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

theorem NLogN.KFW.cTr_U {n Z w2 E : ℕ} (hn : 1 ≤ n) (hZ : Z ≤ Zr) (hZr : Zr + 2 ≤ r) (hw : w2 ≤ H + 2)
    (hE : E ≤ H) (hEZ : zsz (E : ℤ) ≤ Z) :
    cTrP E Z + 400 * (cTrunc w2 E (2 * (n * r)) Z + 0) + (2 * (2 * (E + Z + 1) + 2) + 1) ≤
      (10 ^ 9 * (eL.size + 2)) * (n * Yu r Zr H)

Context. KFW C-layer 17: the local cost pieces in the unit U = Yu r Zr H

Every frame, test, S_D pass, scalar kernel, truncation and padding move costs at most a fixed multiple of U or of n U (n = P 2^{K D} S records).

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

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFW
open IntMul NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN Complex Butterfly
variable {r Zr H : ℕ}

Formal statement

theorem NLogN.KFW.cTr_U {n Z w2 E : ℕ} (hn : 1 ≤ n) (hZ : Z ≤ Zr) (hZr : Zr + 2 ≤ r) (hw : w2 ≤ H + 2)
    (hE : E ≤ H) (hEZ : zsz (E : ℤ) ≤ Z) :
    cTrP E Z + 400 * (cTrunc w2 E (2 * (n * r)) Z + 0) + (2 * (2 * (E + Z + 1) + 2) + 1) ≤
      (10 ^ 9 * (eL.size + 2)) * (n * Yu r Zr H) := 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.KFW.cTr_U`, Solutions/KFWC17.lean (lines 111–166) of the round-six development.

View graph