The word is the reversal of the first `n` digits (round six, `word_rev`)

Proved

NLogN.KFUU.R6Crt.word_rev

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

complexity-theoryinteger-multiplicationkappa-improvement

The word is the reversal of the first n digits.

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

theorem NLogN.KFUU.R6Crt.word_rev {T : Shape} (hQ : 2 ≤ Q) {b : List ℕ} (hb : Valid (SH n Q T) b) :
    word Q n b = KFU.revH n b

Context. CRT reversal §2: the address algebra of the additive-swap reversal

Addresses of the shape SH n Q T = replicate n Q ++ T (the n main digits of size Q, then an arbitrary tail T). With m = n / 2, x = digits [0, m), y = digits [n-m, n):

shr Q i k μ — digit i := digit i − μ · digit k (mod Q): the pull map of one digit-selector rotation rotDU (rotG_shr);
lsetK … sig μ m — the m shears of one rotation set (target n-m+j, control ctl sig m j = σ j or j);
bsw n m — exchange of the digit blocks x and y (one composite Lemma 12 swap).

word_rev: L(-σ) ∘ S ∘ L(σ) ∘ L(-1) ∘ S ∘ L(1) ∘ S ∘ L(σ) ∘ L(-1) = revH n on valid addresses (as a composite pull map; see jain6/crt/DESIGN.md). The proof computes the digits in ZMod Q block by block.

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 AModel NLogN.KFUU
variable {Q n m : ℕ}

Formal statement

theorem NLogN.KFUU.R6Crt.word_rev {T : Shape} (hQ : 2 ≤ Q) {b : List ℕ} (hb : Valid (SH n Q T) b) :
    word Q n b = KFU.revH n b := 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.word_rev`, Solutions/R6CrtAlg.lean (lines 344–448) of the round-six development.

View graph