Round-six lemma `lsU_runs`

Proved

NLogN.KFUU.R6Crt.lsU_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.R6CrtSet):

theorem NLogN.KFUU.R6Crt.lsU_runs (sig neg : Bool) (Q u n m : ℕ) (hQd : Q = 2 ^ u) (T : Shape) (hu : 1 ≤ u)
    (hm : 1 ≤ m) (hmn : 2 * m ≤ n) (hT : ∀ a ∈ T, 1 ≤ a) (w Z : ℕ) (hZ3 : 3 ≤ 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 : List Item) (h0 : t.G 0 = ints xs ++ R)
    {L2 LP LB LD LI LH RSP : List Item}
    (h2 : t.G rU2 = .int ((Q : ℕ) : ℤ) :: L2)
    (hP : t.G gP = .int ((Q ^ (n - m) : ℕ) : ℤ) :: LP)
    (hB : t.G gB = .int ((Q ^ (m - 1) * vol T : ℕ) : ℤ) :: LB)
    (hD : t.G gD = .int ((Q ^ (m - 1) : ℕ) : ℤ) :: LD)
    (hI : t.G gI = .int ((n - m : ℕ) : ℤ) :: LI)
    (hH : t.G rH = .int ((m : ℕ) : ℤ) :: LH)
    (hSP : t.G oSP = ints (List.replicate n ((Q : ℕ) : ℤ)) ++ RSP) :
    IRuns I iprog (lsU sig neg) t
      (t.upd 0 (ints (pull (SH n Q T) (SH n Q T) (lsetK Q n m sig (muV Q neg) m) 0 xs) ++ R))
      (cLs n (vol (SH n Q T)) Q w Z m)

Context. CRT reversal §5: one rotation set (lsU) and one composite swap (swpU) in IL

lsU sig neg: push Q, μ = Q-1 (neg) or 1, and the start values from the global registers; run m iterations of rotIt sig (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 first and the last m digits (swS with u' = u·m, 2^{u'} = Q^m). swpU_runs: the data becomes pull … (bsw n m) xs.

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.lsU_runs (sig neg : Bool) (Q u n m : ℕ) (hQd : Q = 2 ^ u) (T : Shape) (hu : 1 ≤ u)
    (hm : 1 ≤ m) (hmn : 2 * m ≤ n) (hT : ∀ a ∈ T, 1 ≤ a) (w Z : ℕ) (hZ3 : 3 ≤ 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 : List Item) (h0 : t.G 0 = ints xs ++ R)
    {L2 LP LB LD LI LH RSP : List Item}
    (h2 : t.G rU2 = .int ((Q : ℕ) : ℤ) :: L2)
    (hP : t.G gP = .int ((Q ^ (n - m) : ℕ) : ℤ) :: LP)
    (hB : t.G gB = .int ((Q ^ (m - 1) * vol T : ℕ) : ℤ) :: LB)
    (hD : t.G gD = .int ((Q ^ (m - 1) : ℕ) : ℤ) :: LD)
    (hI : t.G gI = .int ((n - m : ℕ) : ℤ) :: LI)
    (hH : t.G rH = .int ((m : ℕ) : ℤ) :: LH)
    (hSP : t.G oSP = ints (List.replicate n ((Q : ℕ) : ℤ)) ++ RSP) :
    IRuns I iprog (lsU sig neg) t
      (t.upd 0 (ints (pull (SH n Q T) (SH n Q T) (lsetK Q n m sig (muV Q neg) m) 0 xs) ++ R))
      (cLs n (vol (SH n Q T)) Q w Z m) := 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.lsU_runs`, Solutions/R6CrtSet.lean (lines 85–201) of the round-six development.

View graph