Round-six lemma `dotP_spec`

Proved

J6Seg.JK.dotP_spec

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

theorem J6Seg.JK.dotP_spec {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M Xb Φm) (hX : XOK X)
    (s : IState HS) {lp lp1 Lc : List ℤ} (hPX : F PX = []) (hrP : F rP = 2 ^ P :: lp)
    (hrP1 : F rP1 = 2 ^ (P + 1) :: lp1) (hCD : F CD = []) (hTMP : F TMP = [])
    (hT : F dTJ = cs ++ R) (hTT : F J6Seg.JK.TT = T0) (hXa : F X = acc) (hS : F SUM = S0 :: Ls)
    (hCNT : F CNT = (cs.length : ℤ) :: Lc)
    (hca : cs.length ≤ acc.length) (hcB : Bnd Xb cs) (haB : Bnd Xb acc)
    (hXB : 2 * Xb + 3 ≤ Bx) (hPB : P + 3 ≤ Bx) (hcl : zsz (cs.length : ℤ) ≤ Bc) (hBc : Bc ≤ Bx)
    (hSk : ∀ k ≤ cs.length, zsz (S0 + dotF P (cs.take k) acc) ≤ Bx) :
    MSp M (dotP X) (encK s F)
      (encK s (update (update (update F dTJ R) J6Seg.JK.TT (cs.reverse ++ T0)) SUM
        ((S0 + dotF P cs acc) :: Ls)))
      ((cs.length + 1) * uC Φm Bx Bc)

Context. B-line IL, the J kernel (B4), part 4: the dot loop as a whole, loops with varying bodies

MSp.repS: the counted loop through managed states with an iteration-dependent body cost (∑ k < N, c k);
dotP_spec: dotP X adds dotF P cs acc to SUM, consumes |cs| table entries onto TT and restores X, at cost (|cs| + 1) · uC;
the a-priori bounds of the fixed-point dot products (fmul_abs_lt, dotF_take_abs_le).

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_Defs66

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.JK
open IntMul NLogN NLogN.KIL Function Finset
variable {P : ℕ} {F : Fin HS → List ℤ} {X : Fin HS} {cs acc R T0 : List ℤ} {S0 : ℤ} {Ls : List ℤ}

Formal statement

theorem J6Seg.JK.dotP_spec {M : MulSpec} {Xb Φm Bx Bc : ℕ} (hMB : MulBnd M Xb Φm) (hX : XOK X)
    (s : IState HS) {lp lp1 Lc : List ℤ} (hPX : F PX = []) (hrP : F rP = 2 ^ P :: lp)
    (hrP1 : F rP1 = 2 ^ (P + 1) :: lp1) (hCD : F CD = []) (hTMP : F TMP = [])
    (hT : F dTJ = cs ++ R) (hTT : F J6Seg.JK.TT = T0) (hXa : F X = acc) (hS : F SUM = S0 :: Ls)
    (hCNT : F CNT = (cs.length : ℤ) :: Lc)
    (hca : cs.length ≤ acc.length) (hcB : Bnd Xb cs) (haB : Bnd Xb acc)
    (hXB : 2 * Xb + 3 ≤ Bx) (hPB : P + 3 ≤ Bx) (hcl : zsz (cs.length : ℤ) ≤ Bc) (hBc : Bc ≤ Bx)
    (hSk : ∀ k ≤ cs.length, zsz (S0 + dotF P (cs.take k) acc) ≤ Bx) :
    MSp M (dotP X) (encK s F)
      (encK s (update (update (update F dTJ R) J6Seg.JK.TT (cs.reverse ++ T0)) SUM
        ((S0 + dotF P cs acc) :: Ls)))
      ((cs.length + 1) * uC Φm Bx Bc) := 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.JK.dotP_spec`, Solutions/J6SegILJKer4.lean (lines 95–179) of the round-six development.

View graph