The rounding passes (round six, `finA_runs6`)

Proved

IntMul.Kappa.R6.finA_runs6

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

complexity-theoryinteger-multiplicationkappa-improvement

The rounding passes.

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

theorem IntMul.Kappa.R6.finA_runs6 {I : List Sym} (hQ : QOk Q) (hD : Q.d = D + 1)
    (t : IState HS) (hR : Q.Base t) (zsZ : List GI)
    (hl : zsZ.length = 2 ^ Q.L) (h0 : t.G 0 = ints (gflat zsZ)) (hg : GB (wU6 Q D) zsZ) :
    IRuns I (IL.kTableP tab extM) finA t
      (t.upd 0 (ints (gflat ((zsZ.map NLogN.KFM.gconj).map fun z =>
        (rndV Q.p Q.b Q.S z.1, rndV Q.p Q.b Q.S z.2)))))
      (kFinA6 Q D)

Context. Round-six machine: the product and the rounding passes

The frozen KFMBig7 / KFMBig8 at the round-six parameters.

mul_phase6: both inputs, the Gaussian product, conjugation and the third transform.
finA_runs6: conj; ×S; ×S; ×2^{2b+4}; round_p.

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_Defs16

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6
open AModel AModelL12 IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFT NLogN.RS IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.RC IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFM Complex NLogN.KFZ
variable {E : ℕ} {ix : Ix6 (7 + E)} {Isym : List Sym} {tab : Fin 1 → IStmt HS 1}
  {extM : Fin E → IStmt HS (7 + E)} {Q : Q6} {D : ℕ}
  [instS : ∀ i, NeZero (Q.sB D i)] [instT : ∀ i, NeZero (Q.tB D i)]

Formal statement

theorem IntMul.Kappa.R6.finA_runs6 {I : List Sym} (hQ : QOk Q) (hD : Q.d = D + 1)
    (t : IState HS) (hR : Q.Base t) (zsZ : List GI)
    (hl : zsZ.length = 2 ^ Q.L) (h0 : t.G 0 = ints (gflat zsZ)) (hg : GB (wU6 Q D) zsZ) :
    IRuns I (IL.kTableP tab extM) finA t
      (t.upd 0 (ints (gflat ((zsZ.map NLogN.KFM.gconj).map fun z =>
        (rndV Q.p Q.b Q.S z.1, rndV Q.p Q.b Q.S z.2)))))
      (kFinA6 Q D) := 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.finA_runs6`, Solutions/R6MMul.lean (lines 220–303) of the round-six development.

View graph