One source transform (round six, `source_call6`)

Proved

IntMul.Kappa.R6.source_call6

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

complexity-theoryinteger-multiplicationkappa-improvement

One source transform, per call (frozen source_call).

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

theorem IntMul.Kappa.R6.source_call6 (p α : ℕ) (s t : Fin (D + 1) → ℕ) [∀ i, NeZero (s i)] [∀ i, NeZero (t i)]
    (M : AxisMaps6 α s t) (ht : ∀ i, Even (t i)) (ζ : ℂ)
    (hζ : ζ ^ t (Fin.last D) = -1)
    {Mrt : (((i : Fin (D + 1)) → ZMod (t i)) → ℂ) → (((i : Fin (D + 1)) → ZMod (t i)) → ℂ) →
      (((i : Fin (D + 1)) → ZMod (t i)) → ℂ)}
    {θt θit at' bt : ((i : Fin (D + 1)) → ZMod (t i)) → ℂ} (εA εB Er : ℝ)
    (hMrt : ∀ f g, Grid p f → Grid p g → ‖f‖ ≤ 1 → ‖g‖ ≤ 1 → ‖Mrt f g - mrX t f g‖ ≤ Er * hp p)
    (hθ : Phases p (twX t ζ) θt) (hθi : Phases p (fun j => (twX t ζ j)⁻¹) θit)
    (ha : Phases p (fun j => (starRingEnd ℂ) (chirp s t j)) at') (hb' : Phases p (chirp s t) bt)
    (hbg : Grid p bt) (hεA : εA * hp p ≤ 1 / 10) (hEr : Er * hp p ≤ 1 / 10)
    {u : ((i : Fin (D + 1)) → ZMod (s i)) → ℂ} {w : ((i : Fin (D + 1)) → ZMod (t i)) → ℂ}
    {v : ((i : Fin (D + 1)) → ZMod (s i)) → ℂ}
    (hu : ‖u‖ ≤ 1 / 2) (hw : ‖w - tensCLM (kerA M.A) u‖ ≤ εA * hp p)
    (hv : ‖v - tensCLM (kerB M.B) (chirpT p (mcT p Mrt θt θit) bt at' w)‖ ≤ εB * hp p) :
    ‖w‖ ≤ 6 / 10 ∧ ‖chirpT p (mcT p Mrt θt θit) bt at' w‖ ≤ 1 ∧
      Grid p (chirpT p (mcT p Mrt θt θit) bt at' w) ∧
      ‖(2 : ℂ) ^ (2 * (D + 1) * α ^ 2) • v - Rperm s t (dftM s u)‖ ≤
        (2 : ℝ) ^ (2 * (D + 1) * α ^ 2) * ((εA + (Er + 22) + εB) * hp p)

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Definitions.Def_IntMul_MultitapeModel
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_SApprox
import Definitions.Def_IntMul_HvdH_MachineRef
import Definitions.Def_IntMul_HvdH_DiagApprox
import Definitions.Def_IntMul_HvdH_EApprox
import Definitions.Def_IntMul_HvdH_JApprox
import Definitions.Def_IntMul_HvdH_BApprox
import Definitions.Def_IntMul_HvdH_FPApprox
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_Kappa_R6_Defs23

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 {D : ℕ}

Formal statement

theorem IntMul.Kappa.R6.source_call6 (p α : ℕ) (s t : Fin (D + 1) → ℕ) [∀ i, NeZero (s i)] [∀ i, NeZero (t i)]
    (M : AxisMaps6 α s t) (ht : ∀ i, Even (t i)) (ζ : ℂ)
    (hζ : ζ ^ t (Fin.last D) = -1)
    {Mrt : (((i : Fin (D + 1)) → ZMod (t i)) → ℂ) → (((i : Fin (D + 1)) → ZMod (t i)) → ℂ) →
      (((i : Fin (D + 1)) → ZMod (t i)) → ℂ)}
    {θt θit at' bt : ((i : Fin (D + 1)) → ZMod (t i)) → ℂ} (εA εB Er : ℝ)
    (hMrt : ∀ f g, Grid p f → Grid p g → ‖f‖ ≤ 1 → ‖g‖ ≤ 1 → ‖Mrt f g - mrX t f g‖ ≤ Er * hp p)
    (hθ : Phases p (twX t ζ) θt) (hθi : Phases p (fun j => (twX t ζ j)⁻¹) θit)
    (ha : Phases p (fun j => (starRingEnd ℂ) (chirp s t j)) at') (hb' : Phases p (chirp s t) bt)
    (hbg : Grid p bt) (hεA : εA * hp p ≤ 1 / 10) (hEr : Er * hp p ≤ 1 / 10)
    {u : ((i : Fin (D + 1)) → ZMod (s i)) → ℂ} {w : ((i : Fin (D + 1)) → ZMod (t i)) → ℂ}
    {v : ((i : Fin (D + 1)) → ZMod (s i)) → ℂ}
    (hu : ‖u‖ ≤ 1 / 2) (hw : ‖w - tensCLM (kerA M.A) u‖ ≤ εA * hp p)
    (hv : ‖v - tensCLM (kerB M.B) (chirpT p (mcT p Mrt θt θit) bt at' w)‖ ≤ εB * hp p) :
    ‖w‖ ≤ 6 / 10 ∧ ‖chirpT p (mcT p Mrt θt θit) bt at' w‖ ≤ 1 ∧
      Grid p (chirpT p (mcT p Mrt θt θit) bt at' w) ∧
      ‖(2 : ℂ) ^ (2 * (D + 1) * α ^ 2) • v - Rperm s t (dftM s u)‖ ≤
        (2 : ℝ) ^ (2 * (D + 1) * α ^ 2) * ((εA + (Er + 22) + εB) * hp p) := 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.source_call6`, Solutions/R6MFt.lean (lines 51–96) of the round-six development.

View graph