Round-six lemma `mainU_runs`

Proved

NLogN.KFUU.R6Crt.mainU_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.R6CrtMain):

theorem NLogN.KFUU.R6Crt.mainU_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 : ℕ) (hQd : Q = 2 ^ u) (T : Shape) (hu : 1 ≤ u) (hn : 2 ≤ 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)
    {L2 LP LB LD LI LH RSP LUm LQm LMd LBB LW : List Item}
    (h2 : t.G rU2 = .int ((Q : ℕ) : ℤ) :: L2)
    (hP : t.G gP = .int ((Q ^ (n - n / 2) : ℕ) : ℤ) :: LP)
    (hB : t.G gB = .int ((Q ^ (n / 2 - 1) * vol T : ℕ) : ℤ) :: LB)
    (hDg : t.G gD = .int ((Q ^ (n / 2 - 1) : ℕ) : ℤ) :: LD)
    (hI : t.G gI = .int ((n - n / 2 : ℕ) : ℤ) :: LI)
    (hH : t.G rH = .int ((n / 2 : ℕ) : ℤ) :: LH)
    (hSP : t.G oSP = ints (List.replicate n ((Q : ℕ) : ℤ)) ++ RSP)
    (hUm : t.G gUm = .int ((u * (n / 2) : ℕ) : ℤ) :: LUm)
    (hQm : t.G gQm = .int ((Q ^ (n / 2) : ℕ) : ℤ) :: LQm)
    (hMd : t.G gMd = .int ((Q ^ (n - 2 * (n / 2)) : ℕ) : ℤ) :: LMd)
    (hBr : t.G rB = .int ((c2 : ℕ) : ℤ) :: LBB) (hW : t.G rW = .int (w : ℤ) :: LW) :
    IRuns I iprog (mainU eSw dS Dsc) t
      (t.upd 0 (ints (pull (SH n Q T) (SH n Q T) (word Q n) 0 xs) ++ R))
      (cMain τ K Q u n w Z c2 (vol (SH n Q T)))

Context. CRT reversal §6: the nine phases of the additive-swap reversal

mainU = L(-σ) S L(σ) L(-1) S L(1) S L(σ) L(-1) (execution order; L(±σ) = lsU true ·, L(±1) = lsU false ·, S = swpU). mainU_runs: on data xs of shape SH n Q T it computes pull … (word Q n) xs, i.e. (by word_rev) the reversal of the n main digits.

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.mainU_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 : ℕ) (hQd : Q = 2 ^ u) (T : Shape) (hu : 1 ≤ u) (hn : 2 ≤ 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)
    {L2 LP LB LD LI LH RSP LUm LQm LMd LBB LW : List Item}
    (h2 : t.G rU2 = .int ((Q : ℕ) : ℤ) :: L2)
    (hP : t.G gP = .int ((Q ^ (n - n / 2) : ℕ) : ℤ) :: LP)
    (hB : t.G gB = .int ((Q ^ (n / 2 - 1) * vol T : ℕ) : ℤ) :: LB)
    (hDg : t.G gD = .int ((Q ^ (n / 2 - 1) : ℕ) : ℤ) :: LD)
    (hI : t.G gI = .int ((n - n / 2 : ℕ) : ℤ) :: LI)
    (hH : t.G rH = .int ((n / 2 : ℕ) : ℤ) :: LH)
    (hSP : t.G oSP = ints (List.replicate n ((Q : ℕ) : ℤ)) ++ RSP)
    (hUm : t.G gUm = .int ((u * (n / 2) : ℕ) : ℤ) :: LUm)
    (hQm : t.G gQm = .int ((Q ^ (n / 2) : ℕ) : ℤ) :: LQm)
    (hMd : t.G gMd = .int ((Q ^ (n - 2 * (n / 2)) : ℕ) : ℤ) :: LMd)
    (hBr : t.G rB = .int ((c2 : ℕ) : ℤ) :: LBB) (hW : t.G rW = .int (w : ℤ) :: LW) :
    IRuns I iprog (mainU eSw dS Dsc) t
      (t.upd 0 (ints (pull (SH n Q T) (SH n Q T) (word Q n) 0 xs) ++ R))
      (cMain τ K Q u n w Z c2 (vol (SH n Q T))) := 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.mainU_runs`, Solutions/R6CrtMain.lean (lines 38–111) of the round-six development.

View graph