Round-six lemma `dupKE`

Proved

J6A.DP.Sp.dupKE

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

complexity-theoryinteger-multiplicationkappa-improvement

dupK with a general count.

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

theorem J6A.DP.Sp.dupKE {X Y Z C : Fin HS} (hXY : X ≠ Y) (hXZ : X ≠ Z) (hYZ : Y ≠ Z) (hXC : X ≠ C)
    (hYC : Y ≠ C) (hZC : Z ≠ C) (hX5 : X.val < 56) (hY5 : Y.val < 56) (hZ5 : Z.val < 56)
    (hC5 : C.val < 56) (s : IState HS) (f : Fin HS → List ℤ) (n : Ex HS) (hnc : n.Clean)
    (L l : List ℤ) (hfX : f X = L ++ l) (hfC : f C = []) (Bb : ℕ) (hL : Bnd Bb L)
    (hno : n.ok (encK s f)) (hnl : n.Lin) (hnb : n.Bnd (encK s f) Bb)
    (hn : n.eval (encK s f) = L.length) :
    Sp (NLogN.KIL.dupKE X Y Z C n) (encK s f)
      (encK s (Function.update (Function.update (Function.update f X l) Y (L.reverse ++ f Y)) Z
        (L.reverse ++ f Z)))
      ((n.size + 1) * 2000 * (Bb + 2) + L.length * ((1 + 1) * 2000 * (Bb + 2) +
        (1 + 1) * 2000 * (Bb + 2) + (2 * Bb + 2) + 8000 * (Bb + 2) + 30) + 32)

Context. A lines, IL side 11: the copy step dupL 32

Sp.dupKE: dupK with a general count expression;
cpBody T T2 C r: from T = G.reverse, push G onto stack 0 (via T2) and restore T; rpt k b: k copies of b in sequence;
dupP: read pre, post, t of the descriptor on dA into the register file, compute 2·pre·t·post, move the array to T, push it back 32 times, drop T, leave the register file.

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_RealExp
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_SApprox
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_HvdH_MachineRef
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_KappaJainData

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul NLogN NLogN.KIL NLogN.RS IntMul.HvdH

Formal statement

theorem J6A.DP.Sp.dupKE {X Y Z C : Fin HS} (hXY : X ≠ Y) (hXZ : X ≠ Z) (hYZ : Y ≠ Z) (hXC : X ≠ C)
    (hYC : Y ≠ C) (hZC : Z ≠ C) (hX5 : X.val < 56) (hY5 : Y.val < 56) (hZ5 : Z.val < 56)
    (hC5 : C.val < 56) (s : IState HS) (f : Fin HS → List ℤ) (n : Ex HS) (hnc : n.Clean)
    (L l : List ℤ) (hfX : f X = L ++ l) (hfC : f C = []) (Bb : ℕ) (hL : Bnd Bb L)
    (hno : n.ok (encK s f)) (hnl : n.Lin) (hnb : n.Bnd (encK s f) Bb)
    (hn : n.eval (encK s f) = L.length) :
    Sp (NLogN.KIL.dupKE X Y Z C n) (encK s f)
      (encK s (Function.update (Function.update (Function.update f X l) Y (L.reverse ++ f Y)) Z
        (L.reverse ++ f Z)))
      ((n.size + 1) * 2000 * (Bb + 2) + L.length * ((1 + 1) * 2000 * (Bb + 2) +
        (1 + 1) * 2000 * (Bb + 2) + (2 * Bb + 2) + 8000 * (Bb + 2) + 30) + 32) := 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 `J6A.DP.Sp.dupKE`, Solutions/J6AIL11.lean (lines 27–84) of the round-six development.

View graph