One input (round six, `inP_phase6`)

Proved

IntMul.Kappa.R6.inP_phase6

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

complexity-theoryinteger-multiplicationkappa-improvement

One input.

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

theorem IntMul.Kappa.R6.inP_phase6 (C : BigCtx6 ix Isym tab extM Q D) (t : IState HS) (hR : Q.Base t) (x : ℕ)
    (hx : x < 2 ^ Q.n) (LA : List Item) (hA : t.G ARGM = .int (x : ℤ) :: LA) :
    ∃ (zs : List GI) (U : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ) (c : ℕ),
      IRuns Isym (IL.kTableP tab extM) (inP6 ix) t
        ((t.upd ARGM LA).upd 0 (ints (gflat zs) ++ t.G 0)) c ∧
      RepPad Q.p (Q.sB D) (Q.tB D) zs U ∧
      GB (Q.p + 2 + (2 * (D + 1) * Q.α ^ 2 + 1)) zs ∧
      ‖U - 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 ∧
      (c : ℝ) ≤ kIn6 C

Context. Round-six machine: the source transform and one input

The frozen KFMChain / KFMBig4 / KFMBig5 / KFMBig6 at the round-six parameters:

lemma20_6, source_call6, w_small6: Lemma 20 and one source transform with the exact per-axis maps AxisMaps6 (only A, B, hA, hB, hid are used);
ftil_phase6: A-lines; chirp; B₀-lines; ×2^γ;
Ix6, BigCtx6: the fixed data and the context of one size;
digW_runs6, inP_phase6: one input.

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.inP_phase6 (C : BigCtx6 ix Isym tab extM Q D) (t : IState HS) (hR : Q.Base t) (x : ℕ)
    (hx : x < 2 ^ Q.n) (LA : List Item) (hA : t.G ARGM = .int (x : ℤ) :: LA) :
    ∃ (zs : List GI) (U : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ) (c : ℕ),
      IRuns Isym (IL.kTableP tab extM) (inP6 ix) t
        ((t.upd ARGM LA).upd 0 (ints (gflat zs) ++ t.G 0)) c ∧
      RepPad Q.p (Q.sB D) (Q.tB D) zs U ∧
      GB (Q.p + 2 + (2 * (D + 1) * Q.α ^ 2 + 1)) zs ∧
      ‖U - 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 ∧
      (c : ℝ) ≤ kIn6 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.inP_phase6`, Solutions/R6MFt.lean (lines 354–426) of the round-six development.

View graph