Round-six lemma `rotIt_runs`

Proved

NLogN.KFUU.R6Crt.rotIt_runs

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

theorem NLogN.KFUU.R6Crt.rotIt_runs (sig : Bool) (Q u n m : ℕ) (hQd : Q = 2 ^ u) (T : Shape) (μ : ℕ) (hu : 1 ≤ u)
    (hmn : 2 * m ≤ n) (hμ : μ < Q) (hT : ∀ a ∈ T, 1 ≤ a) (w Z : ℕ)
    (hVZ : zsz ((vol (SH n Q T) : ℕ) : ℤ) ≤ Z)
    (xs : List ℤ) (hlen : xs.length = vol (SH n Q T)) (hb : Bnd w xs)
    (t : IState HS) (R LP LB LD LI : List Item) {k : ℕ} (hk : k < m)
    {LQ LM L2 RSP : List Item}
    (hQ : t.G oQ = .int ((Q : ℕ) : ℤ) :: LQ) (hMu : t.G oMu = .int (μ : ℤ) :: LM)
    (h2 : t.G rU2 = .int ((Q : ℕ) : ℤ) :: L2)
    (hSP : t.G oSP = ints (List.replicate n ((Q : ℕ) : ℤ)) ++ RSP) :
    IRuns I iprog (rotIt sig) (lsSt Q n m T sig μ t R LP LB LD LI xs k)
      (lsSt Q n m T sig μ t R LP LB LD LI xs (k + 1)) (cIt n (vol (SH n Q T)) Q w Z)

Context. CRT reversal §4: one rotation set and one composite swap in IL

rotIt sig: one digit-selector rotation (rotDU) and the register advance P_t ← P_t·Q, vol C ← vol C / Q, D ← D/Q (sig) or D·Q, t ← t+1.
lsU sig neg: the rotation set L(±σ) / L(±1): push Q, μ = Q-1 (neg) or 1, and the start values from the global registers, run m = ⌊n/2⌋ iterations (rptX on rH), pop. lsU_runs: the data xs (shape SH n Q T) becomes pull … (lsetK Q n m sig μ m) xs.
swpU: the composite Lemma 12 swap of the blocks x, y (swS with u' = u·m, 2^{u'} = Q^m). swpU_runs: the data becomes pull … (bsw n m) xs.

Global registers (set by the prologue of p2E): gQm = Q^m, gP = Q^{n-m}, gB = Q^{m-1} · vol T, gD = Q^{m-1}, gI = n - m, gUm = u·m, gMd = Q^{n-2m}; rH = m, rB = vol T / 2, oSP holds n copies of Q.

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_Defs14

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFUU NLogN.KFUU.R6Crt
open IntMul NLogN.KIL NLogN.KFB NLogN.KFC NLogN.KFT NLogN.KFU AModel AModelL12 NLogN.KFUU
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}

Formal statement

theorem NLogN.KFUU.R6Crt.rotIt_runs (sig : Bool) (Q u n m : ℕ) (hQd : Q = 2 ^ u) (T : Shape) (μ : ℕ) (hu : 1 ≤ u)
    (hmn : 2 * m ≤ n) (hμ : μ < Q) (hT : ∀ a ∈ T, 1 ≤ a) (w Z : ℕ)
    (hVZ : zsz ((vol (SH n Q T) : ℕ) : ℤ) ≤ Z)
    (xs : List ℤ) (hlen : xs.length = vol (SH n Q T)) (hb : Bnd w xs)
    (t : IState HS) (R LP LB LD LI : List Item) {k : ℕ} (hk : k < m)
    {LQ LM L2 RSP : List Item}
    (hQ : t.G oQ = .int ((Q : ℕ) : ℤ) :: LQ) (hMu : t.G oMu = .int (μ : ℤ) :: LM)
    (h2 : t.G rU2 = .int ((Q : ℕ) : ℤ) :: L2)
    (hSP : t.G oSP = ints (List.replicate n ((Q : ℕ) : ℤ)) ++ RSP) :
    IRuns I iprog (rotIt sig) (lsSt Q n m T sig μ t R LP LB LD LI xs k)
      (lsSt Q n m T sig μ t R LP LB LD LI xs (k + 1)) (cIt n (vol (SH n Q T)) Q w Z) := 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 `NLogN.KFUU.R6Crt.rotIt_runs`, Solutions/R6CrtLoop.lean (lines 118–243) of the round-six development.

View graph