The rotation of `Y` with the term `T ∈ {tmA, tmB}` (`rotY_RS`)

Proved

IntMul.Kappa.R6.IL2C.rotY_RS

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

complexity-theoryinteger-multiplicationkappa-improvement

The rotation of Y with the term T ∈ {tmA, tmB}.

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

theorem IntMul.Kappa.R6.IL2C.rotY_RS {T : Ex HS} {tf : ℤ → ℤ → ℤ}
    (hT : SegTR T tf (zsz ((l.M * Br : ℕ) : ℤ) + 3) (2 * (2 : ℤ) ^ G) ((2 : ℤ) ^ G))
    (hfok : fok (tabGenR 1 T) = true)
    (hsz : ((rotPlR eYP (.reg kQL) eYB (eYd kSU) (eYd kST) (.reg kRR) (.reg kRR) (.reg kK2)
      (.reg kR2) (.reg IntMul.Kappa.R6.IL2C.kN) (.reg kRR)).map fun p => p.2.size + 1).sum ≤ 200) :
    RecStep I tab (rotR 1 T eYP (.reg kQL) eYB (eYd kSU) (eYd kST) (.reg kRR) (.reg kRR)
        (.reg kK2) (.reg kR2) (.reg IntMul.Kappa.R6.IL2C.kN) (.reg kRR)) (fun t => CEnv t l K ρ G n q Br fl) l.M Br
      (IntMul.Kappa.R6.IL2C.rotP l.QL l.sY (tabE 1 tf ((2 : ℤ) ^ G) ((2 : ℤ) ^ G) ((2 : ℤ) ^ K) ((2 : ℤ) ^ ρ)
        (l.sU / (l.QL * l.sY)) (l.sT / (l.QL * l.sY)) l.QL n))
      (cR T l n Br (l.M / (l.QL * l.sY)) l.QL l.sY)

Context. Round six, compact controls (I2C): the compact phase as record steps

The ten table rotations (rotYA, rotYB on Y; rotS, rotC, rotL ±1 on Bk) and the twelve Lemma 12 swaps (swT, swU: the compact fields T, U with Bk) of the compact program, with all parameters read from the registers of CEnv, as RecSteps:

phaseC_step: one phase is l.stepP phInv;
psiC_step: phase, load, phase, unload is l.stepP Psi;
compactC_step: followed by the correction it is l.stepP TlS (exactly).

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
variable {I : List Sym} {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ}
  {l : Lay} {K ρ G n L q Br : ℕ} {fl : ℤ}
variable (hP : PhOK l K ρ G n L Br)
include hP

Formal statement

theorem IntMul.Kappa.R6.IL2C.rotY_RS {T : Ex HS} {tf : ℤ → ℤ → ℤ}
    (hT : SegTR T tf (zsz ((l.M * Br : ℕ) : ℤ) + 3) (2 * (2 : ℤ) ^ G) ((2 : ℤ) ^ G))
    (hfok : fok (tabGenR 1 T) = true)
    (hsz : ((rotPlR eYP (.reg kQL) eYB (eYd kSU) (eYd kST) (.reg kRR) (.reg kRR) (.reg kK2)
      (.reg kR2) (.reg IntMul.Kappa.R6.IL2C.kN) (.reg kRR)).map fun p => p.2.size + 1).sum ≤ 200) :
    RecStep I tab (rotR 1 T eYP (.reg kQL) eYB (eYd kSU) (eYd kST) (.reg kRR) (.reg kRR)
        (.reg kK2) (.reg kR2) (.reg IntMul.Kappa.R6.IL2C.kN) (.reg kRR)) (fun t => CEnv t l K ρ G n q Br fl) l.M Br
      (IntMul.Kappa.R6.IL2C.rotP l.QL l.sY (tabE 1 tf ((2 : ℤ) ^ G) ((2 : ℤ) ^ G) ((2 : ℤ) ^ K) ((2 : ℤ) ^ ρ)
        (l.sU / (l.QL * l.sY)) (l.sT / (l.QL * l.sY)) l.QL n))
      (cR T l n Br (l.M / (l.QL * l.sY)) l.QL l.sY) := 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.rotY_RS`, Solutions/R6IL2CPhase.lean (lines 190–270) of the round-six development.

View graph