The single-bit swap (round six, `topSw_step`)

Proved

IntMul.Kappa.R6.IL2C.topSw_step

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

complexity-theoryinteger-multiplicationkappa-improvement

The single-bit swap of Y's bit q with X's bit q (X below Y).

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

theorem IntMul.Kappa.R6.IL2C.topSw_step {Ksw : ℝ} (H : IntMul.Kappa.R6.IL2C.SwOK tab l12 τ Ksw) (hT : TopOK l L q Br) {k : ℕ} (hk : 0 < k)
    (hYX : l.sY = l.sX * l.QL * k) :
    RecStep I tab (topSw l12) (fun t => CEnv t l K ρ G n q Br fl) l.M Br
      (swP 2 (l.sY * 2 ^ q) (l.sX * 2 ^ q)) (Ksw * (((l.M * Br : ℕ) : ℝ) + 1))

Context. Round six, compact controls (I2C): the top selected bit and the record-step calculus

Tl_xor: the ideal toggle is y ⊕ (x ∧ selM n); with the top bit q = ρ + n K flipped as well (flipS q) the composite step is the slot row addition phi g (Fpp K ρ (n+1) px py) (tlflip_phi).
flip_pull, swflip: the last-bit table rotation (directly when X is above Y, between two swaps of single bits otherwise) is the record pull l.stepP (flipS q).
RecStep: a program acting on the record array flR recs M as recs ∘ π, with sequencing, branching and skip.
CEnv: the registers of the compact program; topC_step: the top-bit code as a RecStep.

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_Defs21

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2C
open NLogN NLogN.KFL NLogN.KIL NLogN.KFD NLogN.KFW NLogN.KFX IntMul NLogN.RS NLogN.KFW.RS AModel AModelL12 Butterfly
variable {I : List Sym} {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ}
  {l : Lay} {K ρ G n q L Br : ℕ} {fl : ℤ}

Formal statement

theorem IntMul.Kappa.R6.IL2C.topSw_step {Ksw : ℝ} (H : IntMul.Kappa.R6.IL2C.SwOK tab l12 τ Ksw) (hT : TopOK l L q Br) {k : ℕ} (hk : 0 < k)
    (hYX : l.sY = l.sX * l.QL * k) :
    RecStep I tab (topSw l12) (fun t => CEnv t l K ρ G n q Br fl) l.M Br
      (swP 2 (l.sY * 2 ^ q) (l.sX * 2 ^ q)) (Ksw * (((l.M * Br : ℕ) : ℝ) + 1)) := 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 `IntMul.Kappa.R6.IL2C.topSw_step`, Solutions/R6IL2CTop.lean (lines 503–555) of the round-six development.

View graph