A rotation of `Bk` (`Q = QC`, stride `1`, `w0 = 1`, `|tf| ≤ 1`, `rw = 2^G`) (`rotBk_RS`)

Proved

IntMul.Kappa.R6.IL2C.rotBk_RS

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

complexity-theoryinteger-multiplicationkappa-improvement

A rotation of Bk (Q = QC, stride 1, w0 = 1, |tf| ≤ 1, rw = 2^G).

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

theorem IntMul.Kappa.R6.IL2C.rotBk_RS {T : Ex HS} {tf : ℤ → ℤ → ℤ}
    (hT : SegTR T tf (zsz ((l.M * Br : ℕ) : ℤ) + 3) 1 ((2 : ℤ) ^ G))
    (sgn : ℤ) (hs : sgn = 1 ∨ sgn = -1) (hfok : fok (tabGenR sgn T) = true)
    {d1 d2 : ℕ} {ru rv : ℤ} {e1 e2 eu ev ew : Ex HS} (hd1 : 0 < d1) (hd2 : 0 < d2)
    (hru : 0 < ru) (hrv : 0 < rv)
    (zru : zsz ru ≤ zsz ((l.M * Br : ℕ) : ℤ) + 3) (zrv : zsz rv ≤ zsz ((l.M * Br : ℕ) : ℤ) + 3)
    (zd1 : d1 ≤ l.M) (zd2 : d2 ≤ l.M)
    (hsz : ((rotPlR eBP (.reg kQC) (.reg kBr) e1 e2 eu ev ew (.lit 1) (.reg IntMul.Kappa.R6.IL2C.kN) (.reg kRR)).map
      fun p => p.2.size + 1).sum ≤ 200)
    (hlow : ∀ p ∈ rotPlR eBP (.reg kQC) (.reg kBr) e1 e2 eu ev ew (.lit 1) (.reg IntMul.Kappa.R6.IL2C.kN) (.reg kRR),
      KFX.NoLow p.2)
    (E1 : ∀ t, CEnv t l K ρ G n q Br fl → ESp e1 t (zsz ((l.M * Br : ℕ) : ℤ) + 3) (d1 : ℤ))
    (E2 : ∀ t, CEnv t l K ρ G n q Br fl → ESp e2 t (zsz ((l.M * Br : ℕ) : ℤ) + 3) (d2 : ℤ))
    (Eu : ∀ t, CEnv t l K ρ G n q Br fl → ESp eu t (zsz ((l.M * Br : ℕ) : ℤ) + 3) ru)
    (Ev : ∀ t, CEnv t l K ρ G n q Br fl → ESp ev t (zsz ((l.M * Br : ℕ) : ℤ) + 3) rv)
    (Ew : ∀ t, CEnv t l K ρ G n q Br fl → ESp ew t (zsz ((l.M * Br : ℕ) : ℤ) + 3) ((2 : ℤ) ^ G)) :
    RecStep I tab (rotR sgn T eBP (.reg kQC) (.reg kBr) e1 e2 eu ev ew (.lit 1) (.reg IntMul.Kappa.R6.IL2C.kN) (.reg kRR))
      (fun t => CEnv t l K ρ G n q Br fl) l.M Br
      (IntMul.Kappa.R6.IL2C.rotP l.QC 1 (tabE sgn tf ru rv ((2 : ℤ) ^ G) 1 d1 d2 l.QC n))
      (cR T l n Br (l.M / l.QC) l.QC 1)

Context. Round six, compact controls (I2C): the compact phase as record steps

The ten table rotations (rotYA, rotYB on Y; rotS, rotC, rotL ±1 on Bk) and the twelve Lemma 12 swaps (swT, swU: the compact fields T, U with Bk) of the compact program, with all parameters read from the registers of CEnv, as RecSteps:

phaseC_step: one phase is l.stepP phInv;
psiC_step: phase, load, phase, unload is l.stepP Psi;
compactC_step: followed by the correction it is l.stepP TlS (exactly).

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 NLogN.KFW NLogN.KFX IntMul NLogN.RS NLogN.KFW.RS AModel AModelL12
variable {I : List Sym} {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ}
  {l : Lay} {K ρ G n L q Br : ℕ} {fl : ℤ}
variable (hP : PhOK l K ρ G n L Br)
include hP

Formal statement

theorem IntMul.Kappa.R6.IL2C.rotBk_RS {T : Ex HS} {tf : ℤ → ℤ → ℤ}
    (hT : SegTR T tf (zsz ((l.M * Br : ℕ) : ℤ) + 3) 1 ((2 : ℤ) ^ G))
    (sgn : ℤ) (hs : sgn = 1 ∨ sgn = -1) (hfok : fok (tabGenR sgn T) = true)
    {d1 d2 : ℕ} {ru rv : ℤ} {e1 e2 eu ev ew : Ex HS} (hd1 : 0 < d1) (hd2 : 0 < d2)
    (hru : 0 < ru) (hrv : 0 < rv)
    (zru : zsz ru ≤ zsz ((l.M * Br : ℕ) : ℤ) + 3) (zrv : zsz rv ≤ zsz ((l.M * Br : ℕ) : ℤ) + 3)
    (zd1 : d1 ≤ l.M) (zd2 : d2 ≤ l.M)
    (hsz : ((rotPlR eBP (.reg kQC) (.reg kBr) e1 e2 eu ev ew (.lit 1) (.reg IntMul.Kappa.R6.IL2C.kN) (.reg kRR)).map
      fun p => p.2.size + 1).sum ≤ 200)
    (hlow : ∀ p ∈ rotPlR eBP (.reg kQC) (.reg kBr) e1 e2 eu ev ew (.lit 1) (.reg IntMul.Kappa.R6.IL2C.kN) (.reg kRR),
      KFX.NoLow p.2)
    (E1 : ∀ t, CEnv t l K ρ G n q Br fl → ESp e1 t (zsz ((l.M * Br : ℕ) : ℤ) + 3) (d1 : ℤ))
    (E2 : ∀ t, CEnv t l K ρ G n q Br fl → ESp e2 t (zsz ((l.M * Br : ℕ) : ℤ) + 3) (d2 : ℤ))
    (Eu : ∀ t, CEnv t l K ρ G n q Br fl → ESp eu t (zsz ((l.M * Br : ℕ) : ℤ) + 3) ru)
    (Ev : ∀ t, CEnv t l K ρ G n q Br fl → ESp ev t (zsz ((l.M * Br : ℕ) : ℤ) + 3) rv)
    (Ew : ∀ t, CEnv t l K ρ G n q Br fl → ESp ew t (zsz ((l.M * Br : ℕ) : ℤ) + 3) ((2 : ℤ) ^ G)) :
    RecStep I tab (rotR sgn T eBP (.reg kQC) (.reg kBr) e1 e2 eu ev ew (.lit 1) (.reg IntMul.Kappa.R6.IL2C.kN) (.reg kRR))
      (fun t => CEnv t l K ρ G n q Br fl) l.M Br
      (IntMul.Kappa.R6.IL2C.rotP l.QC 1 (tabE sgn tf ru rv ((2 : ℤ) ^ G) 1 d1 d2 l.QC n))
      (cR T l n Br (l.M / l.QC) l.QC 1) := 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.rotBk_RS`, Solutions/R6IL2CPhase.lean (lines 272–326) of the round-six development.

View graph