Round-six lemma `swpU_runs`

Proved

NLogN.KFUU.R6Crt.swpU_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.swpU_runs {eSw : Fin P} {dS : Fin HS} {K : ℝ} (hK : SwOKτ τ I iprog eSw dS K)
    (hdS : dS ≠ 0) {Dsc : Fin HS} (hD : Dsc = 18 ∨ Dsc = 19) (hDd : Dsc ≠ dS)
    (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) (c2 : ℕ) (hc2 : vol T = c2 * 2) (w Z : ℕ)
    (hZ3 : 3 ≤ Z) (zw : zsz (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 : List Item) (h0 : t.G 0 = ints xs ++ R)
    {LUm LQm LMd LB LW : List Item}
    (hUm : t.G gUm = .int ((u * m : ℕ) : ℤ) :: LUm)
    (hQm : t.G gQm = .int ((Q ^ m : ℕ) : ℤ) :: LQm)
    (hMd : t.G gMd = .int ((Q ^ (n - 2 * m) : ℕ) : ℤ) :: LMd)
    (hB : t.G rB = .int ((c2 : ℕ) : ℤ) :: LB) (hW : t.G rW = .int (w : ℤ) :: LW) :
    ∃ c : ℕ, IRuns I iprog (swpU eSw dS Dsc) t
      (t.upd 0 (ints (pull (SH n Q T) (SH n Q T) (bsw n m) 0 xs) ++ R)) c ∧
      (c : ℝ) ≤ cSwNτ τ K w (u * m) [1, Q ^ m, Q ^ (n - 2 * m), Q ^ m, c2] + 40 * cU Z

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.swpU_runs {eSw : Fin P} {dS : Fin HS} {K : ℝ} (hK : SwOKτ τ I iprog eSw dS K)
    (hdS : dS ≠ 0) {Dsc : Fin HS} (hD : Dsc = 18 ∨ Dsc = 19) (hDd : Dsc ≠ dS)
    (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) (c2 : ℕ) (hc2 : vol T = c2 * 2) (w Z : ℕ)
    (hZ3 : 3 ≤ Z) (zw : zsz (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 : List Item) (h0 : t.G 0 = ints xs ++ R)
    {LUm LQm LMd LB LW : List Item}
    (hUm : t.G gUm = .int ((u * m : ℕ) : ℤ) :: LUm)
    (hQm : t.G gQm = .int ((Q ^ m : ℕ) : ℤ) :: LQm)
    (hMd : t.G gMd = .int ((Q ^ (n - 2 * m) : ℕ) : ℤ) :: LMd)
    (hB : t.G rB = .int ((c2 : ℕ) : ℤ) :: LB) (hW : t.G rW = .int (w : ℤ) :: LW) :
    ∃ c : ℕ, IRuns I iprog (swpU eSw dS Dsc) t
      (t.upd 0 (ints (pull (SH n Q T) (SH n Q T) (bsw n m) 0 xs) ++ R)) c ∧
      (c : ℝ) ≤ cSwNτ τ K w (u * m) [1, Q ^ m, Q ^ (n - 2 * m), Q ^ m, c2] + 40 * cU 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.swpU_runs`, Solutions/R6CrtSet.lean (lines 210–302) of the round-six development.

View graph