Round-six lemma `segBodyR_sp`

Proved

IntMul.Kappa.R6.IL2C.segBodyR_sp

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

theorem IntMul.Kappa.R6.IL2C.segBodyR_sp {T : Ex HS} {tf : ℤ → ℤ → ℤ} {Bb : ℕ} {Tm Rv : ℤ} (hT : SegTR T tf Bb Tm Rv)
    (s : IState HS) (F : Fin HS → List ℤ) {ru rv rw : ℤ} {Lu Lv Lw LR : List Item}
    (hRu : (encK s F).G pRu = .int ru :: Lu) (hRv : (encK s F).G pRv = .int rv :: Lv)
    (hRw : (encK s F).G pRw = .int rw :: Lw) (hRR : (encK s F).G IntMul.Kappa.R6.IL2C.pR = .int Rv :: LR)
    (hru : 0 < ru) (hrv : 0 < rv) (hrw : 2 ≤ rw)
    (zru : zsz ru ≤ Bb) (zrv : zsz rv ≤ Bb) (zrw : zsz rw ≤ Bb)
    (a u v w : ℤ) (hu : 0 ≤ u) (hv : 0 ≤ v) (hw : 0 < w)
    (n : ℕ) (hub : zsz u ≤ Bb) (hvb : zsz v ≤ Bb) (hTm : 1 ≤ Tm)
    (hbig : |a| + Tm * w * rw ^ n < 2 ^ Bb)
    (k : ℕ) (hk : k < n) (Ck : List ℤ) :
    Sp (segBodyR T) (encK s (Function.update (IntMul.Kappa.R6.IL2C.segFR F tf ru rv rw a u v w k) IntMul.Kappa.R6.IL2C.rC Ck))
      (encK s (Function.update (IntMul.Kappa.R6.IL2C.segFR F tf ru rv rw a u v w (k + 1)) IntMul.Kappa.R6.IL2C.rC Ck)) (cSegItR T Bb)

Context. Round six, compact controls (I2C): segment loops with three radices

segLoopR T (n iterations, n on register pN): rA += rW · T(rU, rV); rU /= ru; rV /= rv; rW *= rw with the radices ru, rv, rw on the registers pRu, pRv, pRw (left untouched). After the loop rA = a + segSum tf ru rv rw w u v n (segLoopR_fsp). segStepR: push u, v, w, a, loop, assign a function of the accumulator to a target, pop (segStepR_fsp).

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_Defs21

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2C
open NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul NLogN.RS

Formal statement

theorem IntMul.Kappa.R6.IL2C.segBodyR_sp {T : Ex HS} {tf : ℤ → ℤ → ℤ} {Bb : ℕ} {Tm Rv : ℤ} (hT : SegTR T tf Bb Tm Rv)
    (s : IState HS) (F : Fin HS → List ℤ) {ru rv rw : ℤ} {Lu Lv Lw LR : List Item}
    (hRu : (encK s F).G pRu = .int ru :: Lu) (hRv : (encK s F).G pRv = .int rv :: Lv)
    (hRw : (encK s F).G pRw = .int rw :: Lw) (hRR : (encK s F).G IntMul.Kappa.R6.IL2C.pR = .int Rv :: LR)
    (hru : 0 < ru) (hrv : 0 < rv) (hrw : 2 ≤ rw)
    (zru : zsz ru ≤ Bb) (zrv : zsz rv ≤ Bb) (zrw : zsz rw ≤ Bb)
    (a u v w : ℤ) (hu : 0 ≤ u) (hv : 0 ≤ v) (hw : 0 < w)
    (n : ℕ) (hub : zsz u ≤ Bb) (hvb : zsz v ≤ Bb) (hTm : 1 ≤ Tm)
    (hbig : |a| + Tm * w * rw ^ n < 2 ^ Bb)
    (k : ℕ) (hk : k < n) (Ck : List ℤ) :
    Sp (segBodyR T) (encK s (Function.update (IntMul.Kappa.R6.IL2C.segFR F tf ru rv rw a u v w k) IntMul.Kappa.R6.IL2C.rC Ck))
      (encK s (Function.update (IntMul.Kappa.R6.IL2C.segFR F tf ru rv rw a u v w (k + 1)) IntMul.Kappa.R6.IL2C.rC Ck)) (cSegItR T Bb) := 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 `IntMul.Kappa.R6.IL2C.segBodyR_sp`, Solutions/R6IL2CLoop.lean (lines 137–297) of the round-six development.

View graph