Round-six lemma `dmN_runs`

Proved

NLogN.KFM.dmN_runs

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

complexity-theoryinteger-multiplicationkappa-improvement

An 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.KFMTabQ):

theorem NLogN.KFM.dmN_runs (X Y Z : Fin HS) (hXY : X ≠ Y) (hXZ : X ≠ Z) (hYZ : Y ≠ Z) (hX : NC X)
    (hY : NC Y) (hZ : NC Z) (L : List ℤ) (B : ℕ)
    (hB : ∀ x ∈ L, zsz x ≤ B) (s : IState HS) (RX : List Item) (h0 : s.G X = ints L ++ RX) :
    IRuns I iprog (rpt pA pC pD L.length (dmB X Y Z)) s
      (((s.upd X RX).upd Y (ints L.reverse ++ s.G Y)).upd Z (ints L.reverse ++ s.G Z))
      (L.length * (410 * (B + 1) + 64) + 60 + cRpt L.length)

Context. KFM 9d: the d-axis chirp array — outer products of the axis tables

chirpArr Δ d s t is the row-major array (last axis innermost) of the chirp entries chirpEnt Δ s t j, built by d outer products oprod Δ A B = [Q_Δ(a b) | a ∈ A, b ∈ B] starting from [1]:

chirpArr_get: entry flatIx j of chirpArr is chirpEnt Δ s t j (the Q_Δ-product of the d axis-table factors, KFMTabM);
chirpArr_err: it is within d (8T² + 2) 2^{-Δ} of RC.chirp s t j;
chirpArr_near: every entry is within that distance of a point of the unit disc, so all entries have Δ + 2-bit components (NearU.bnd).

The IL program is chirpP (below), one level levP per axis: axG (axis table), then for each entry a of the current array a replicate / copy / gmulP / move-out round (obB).

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 Definitions.Def_IntMul_MultitapeModel
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_RealExp

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFM
open IntMul NLogN.KFC NLogN.KFB NLogN.KFT NLogN.KIL
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}

Formal statement

theorem NLogN.KFM.dmN_runs (X Y Z : Fin HS) (hXY : X ≠ Y) (hXZ : X ≠ Z) (hYZ : Y ≠ Z) (hX : NC X)
    (hY : NC Y) (hZ : NC Z) (L : List ℤ) (B : ℕ)
    (hB : ∀ x ∈ L, zsz x ≤ B) (s : IState HS) (RX : List Item) (h0 : s.G X = ints L ++ RX) :
    IRuns I iprog (rpt pA pC pD L.length (dmB X Y Z)) s
      (((s.upd X RX).upd Y (ints L.reverse ++ s.G Y)).upd Z (ints L.reverse ++ s.G Z))
      (L.length * (410 * (B + 1) + 64) + 60 + cRpt L.length) := 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.KFM.dmN_runs`, Solutions/KFMTabQ.lean (lines 235–281) of the round-six development.

View graph