Round-six lemma `T5_runsP`

Proved

NLogN.KFZ.T5_runsP

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.R6ZProc):

theorem NLogN.KFZ.T5_runsP (A : List GI) (hA : A.length = 2 ^ (h + 1)) (wA : ℕ) (hAB : GB wA A)
    (z w tb ta tt ti : List ℤ) :
    IRuns I (IntMul.Kappa.R6.IL.kTableP tab ext) (NLogN.KFZ.T5 E) (encK s (NLogN.KFZ.St F0 p h d σ K [] z (gflat A ++ w) tb ta tt ti))
      (encK s (NLogN.KFZ.St F0 p h d σ K [] (gflat (A.map (KFH.gtr (gV p h d))) ++ z) w tb ta tt ti))
      (cPush 4 B + ((2 * cMvX (2 * A.length) wA + (cItem (2 * A.length)
        (3000 * (wA + gV p h d + 3)) (2 * wA + 1) + 2 * cCnt (2 * A.length))) + cPop 4 B))

Context. Round six, chirp: the table phases in the parametric table

The frozen KFZWrap / KFZProc table lemmas with kTable ext replaced by IntMul.Kappa.R6.IL.kTableP tab ext (the proofs only use the FM multiplier, IntMul.Kappa.R6.IL.kTableP_mulOK). Names get a P suffix.

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
import Definitions.Def_IntMul_HvdH_SApprox
import Definitions.Def_IntMul_HvdH_MachineRef
import Definitions.Def_IntMul_HvdH_DiagApprox
import Definitions.Def_IntMul_HvdH_EApprox
import Definitions.Def_IntMul_HvdH_JApprox
import Definitions.Def_IntMul_HvdH_BApprox
import Definitions.Def_IntMul_HvdH_FPApprox
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_Kappa_R6_Defs13

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFZ
open IntMul NLogN.KIL NLogN.KFB NLogN.KFM
variable {E : ℕ} (tab : Fin 1 → IStmt HS 1) (ext : Fin E → IStmt HS (7 + E)) {I : List Sym} (s : IState HS)
  (F0 : Fin HS → List ℤ) {p h d σ K B : ℕ} (hB : RB p h d σ K B)
include hB

Formal statement

theorem NLogN.KFZ.T5_runsP (A : List GI) (hA : A.length = 2 ^ (h + 1)) (wA : ℕ) (hAB : GB wA A)
    (z w tb ta tt ti : List ℤ) :
    IRuns I (IntMul.Kappa.R6.IL.kTableP tab ext) (NLogN.KFZ.T5 E) (encK s (NLogN.KFZ.St F0 p h d σ K [] z (gflat A ++ w) tb ta tt ti))
      (encK s (NLogN.KFZ.St F0 p h d σ K [] (gflat (A.map (KFH.gtr (gV p h d))) ++ z) w tb ta tt ti))
      (cPush 4 B + ((2 * cMvX (2 * A.length) wA + (cItem (2 * A.length)
        (3000 * (wA + gV p h d + 3)) (2 * wA + 1) + 2 * cCnt (2 * A.length))) + cPop 4 B)) := 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.KFZ.T5_runsP`, Solutions/R6ZProc.lean (lines 239–280) of the round-six development.

View graph