Round-six lemma `tabBodyR_fsp`

Proved

IntMul.Kappa.R6.IL2C.tabBodyR_fsp

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

theorem IntMul.Kappa.R6.IL2C.tabBodyR_fsp {T : Ex HS} {tf : ℤ → ℤ → ℤ} {Bb : ℕ} {Tm Rv : ℤ} (hT : SegTR T tf Bb Tm Rv)
    (sgn : ℤ) (hs : sgn = 1 ∨ sgn = -1) {Q d1 d2 n : ℕ} {ru rv rw w0 : ℤ}
    (hv : TVal Q d1 d2 ru rv rw w0 Tm n Bb)
    (s : IState HS) (G : Fin HS → List ℤ) (hp : TPar (encK s G) Q d1 d2 ru rv rw w0 Rv n)
    (N : ℕ) (hN : 1 ≤ N) (zN : zsz (N : ℤ) ≤ Bb)
    {LP : List ℤ} (hGq : G KFL.rP = (N : ℤ) :: LP) (hGc : G IntMul.Kappa.R6.IL2C.rC = []) :
    FSp (tabBodyR sgn T) (encK s G)
      (encK s (Function.update (Function.update G 14
        ((tabE sgn tf ru rv rw w0 d1 d2 Q n (N - 1) : ℤ) :: G 14)) KFL.rP (((N : ℤ) - 1) :: LP)))
      (cTabR T Bb n)

Context. Round six, compact controls (I2C): uniform offset tables and rotations

tabGenR sgn T pushes on stack 14 the table p ↦ (sgn · segSum tf ru rv rw w0 (p/d1) (p/d2) n) mod Q (p = P-1, …, 0), all parameters on registers: 1: P, 2: Q, 3: d1, 5: d2, 6: ru, 7: rv, 8: rw, 9: w0, 10: n, 11: R (the term T may read R). rotR pushes the parameters, runs the table generator and the record rotation KFC.rotF (rotR_runs).

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 AModel NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul NLogN.RS

Formal statement

theorem IntMul.Kappa.R6.IL2C.tabBodyR_fsp {T : Ex HS} {tf : ℤ → ℤ → ℤ} {Bb : ℕ} {Tm Rv : ℤ} (hT : SegTR T tf Bb Tm Rv)
    (sgn : ℤ) (hs : sgn = 1 ∨ sgn = -1) {Q d1 d2 n : ℕ} {ru rv rw w0 : ℤ}
    (hv : TVal Q d1 d2 ru rv rw w0 Tm n Bb)
    (s : IState HS) (G : Fin HS → List ℤ) (hp : TPar (encK s G) Q d1 d2 ru rv rw w0 Rv n)
    (N : ℕ) (hN : 1 ≤ N) (zN : zsz (N : ℤ) ≤ Bb)
    {LP : List ℤ} (hGq : G KFL.rP = (N : ℤ) :: LP) (hGc : G IntMul.Kappa.R6.IL2C.rC = []) :
    FSp (tabBodyR sgn T) (encK s G)
      (encK s (Function.update (Function.update G 14
        ((tabE sgn tf ru rv rw w0 d1 d2 Q n (N - 1) : ℤ) :: G 14)) KFL.rP (((N : ℤ) - 1) :: LP)))
      (cTabR T Bb n) := 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.tabBodyR_fsp`, Solutions/R6IL2CTab.lean (lines 138–337) of the round-six development.

View graph