Prove2Me

The product (round six, `mul_phase6`)

Proved
IntMul.Kappa.R6.mul_phase6

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

complexity-theoryinteger-multiplicationkappa-improvement

The product.

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

theorem IntMul.Kappa.R6.mul_phase6 (C : BigCtx6 ix Isym tab extM Q D) (t : IState HS) (hR : Q.Base t) (x y : ℕ)
    (hx : x < 2 ^ Q.n) (hy : y < 2 ^ Q.n) (hA : t.G ARGM = [.int (y : ℤ), .int (x : ℤ)])
    (h0 : t.G 0 = []) (hW : t.G pW = []) :
    ∃ (zsZ : List GI) (Z Ux Uy : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ) (c : ℕ),
      IRuns Isym (IL.kTableP tab extM) (mulP6 ix) t
        (((t.upd ARGM []).upd pW []).upd 0 (ints (gflat zsZ))) c ∧
      RepPad Q.p (Q.sB D) (Q.tB D) zsZ Z ∧ GB (wU6 Q D) zsZ ∧
      ‖Z - Rperm (Q.sB D) (Q.tB D) (dftM (Q.sB D) (cnj (QA Q.p (Ux * Uy))))‖ ≤ Q.Es * hp Q.p ∧
      ‖Ux - Rperm (Q.sB D) (Q.tB D)
        (dftM (Q.sB D) (fun k => (2 : ℂ)⁻¹ ^ (Q.b + 2) * ubar6 C x k))‖ ≤ Q.Es * hp Q.p ∧
      ‖Uy - Rperm (Q.sB D) (Q.tB D)
        (dftM (Q.sB D) (fun k => (2 : ℂ)⁻¹ ^ (Q.b + 2) * ubar6 C y k))‖ ≤ Q.Es * hp Q.p ∧
      (c : ℝ) ≤ kMul6 C

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.mul_phase6 (C : BigCtx6 ix Isym tab extM Q D) (t : IState HS) (hR : Q.Base t) (x y : ℕ)
    (hx : x < 2 ^ Q.n) (hy : y < 2 ^ Q.n) (hA : t.G ARGM = [.int (y : ℤ), .int (x : ℤ)])
    (h0 : t.G 0 = []) (hW : t.G pW = []) :
    ∃ (zsZ : List GI) (Z Ux Uy : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ) (c : ℕ),
      IRuns Isym (IL.kTableP tab extM) (mulP6 ix) t
        (((t.upd ARGM []).upd pW []).upd 0 (ints (gflat zsZ))) c ∧
      RepPad Q.p (Q.sB D) (Q.tB D) zsZ Z ∧ GB (wU6 Q D) zsZ ∧
      ‖Z - Rperm (Q.sB D) (Q.tB D) (dftM (Q.sB D) (cnj (QA Q.p (Ux * Uy))))‖ ≤ Q.Es * hp Q.p ∧
      ‖Ux - Rperm (Q.sB D) (Q.tB D)
        (dftM (Q.sB D) (fun k => (2 : ℂ)⁻¹ ^ (Q.b + 2) * ubar6 C x k))‖ ≤ Q.Es * hp Q.p ∧
      ‖Uy - Rperm (Q.sB D) (Q.tB D)
        (dftM (Q.sB D) (fun k => (2 : ℂ)⁻¹ ^ (Q.b + 2) * ubar6 C y k))‖ ≤ Q.Es * hp Q.p ∧
      (c : ℝ) ≤ kMul6 C := 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.mul_phase6`, Solutions/R6MMul.lean (lines 93–190) of the round-six development.

View graph