The zero-padded record product with `Δ = 0` gives the Toeplitz sums (round six, `kmulD_toep`)

Proved

J6Seg.kmulD_toep

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

complexity-theoryinteger-multiplicationkappa-improvement

The zero-padded record product with Δ = 0 gives the Toeplitz sums.

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

theorem J6Seg.kmulD_toep {r : ℕ} (c : List ℤ) (z : List (ℤ × ℤ)) (hc : z.length ≤ c.length)
    (hr : 2 * z.length ≤ r + 1) {j : ℕ} (hj : j < z.length) :
    (kmulD r 0 (padG r z) (realG r z.length c)).getD j (0, 0) =
      ((convL c (z.map Prod.fst)).getD j 0, (convL c (z.map Prod.snd)).getD j 0)

Context. B3 (chunk kernel), part 1: the Gaussian stages as list maps

The chunk kernel on a Gaussian row is liftG (chunkK q). Here it is rewritten in the form the IL computes:

liftG_comp, liftG_append: liftG commutes with composition / concatenation of length-preserving maps;
dgG c z: the diagonal stage on pairs (liftG (dgL P c) = dgG P c);
kmulD_toep: the zero-padded Kronecker record product with Δ = 0 gives the exact lower-triangular Toeplitz sums convL of both parts (2 n ≤ r + 1);
lwG, upG: the Toeplitz stages on pairs from kmulD (liftG (lwL P c) = lwG, …);
blkG, chunkG: the block solve and the chunk kernel on pairs (liftG (chunkL …) = chunkG …).

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_Defs62

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg
open Finset
open IntMul NLogN NLogN.KFV
variable (P : ℕ)

Formal statement

theorem J6Seg.kmulD_toep {r : ℕ} (c : List ℤ) (z : List (ℤ × ℤ)) (hc : z.length ≤ c.length)
    (hr : 2 * z.length ≤ r + 1) {j : ℕ} (hj : j < z.length) :
    (kmulD r 0 (padG r z) (realG r z.length c)).getD j (0, 0) =
      ((convL c (z.map Prod.fst)).getD j 0, (convL c (z.map Prod.snd)).getD j 0) := 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 `J6Seg.kmulD_toep`, Solutions/J6SegKr1.lean (lines 178–229) of the round-six development.

View graph