The final bound (round six, `final_call3`)

Proved

NLogN.KFM.final_call3

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

complexity-theoryinteger-multiplicationkappa-improvement

The final bound, from three per-call source transforms.

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

theorem NLogN.KFM.final_call3 (p b : ℕ) (s t : Fin (D + 1) → ℕ) [∀ i, NeZero (s i)]
    (hcop : ∀ i, Nat.Coprime (s i) (t i)) (Es : ℝ)
    (hEs : Es * hp p ≤ 1 / 100)
    (hB2 : 2 * (2 : ℝ) ^ (2 * b + 4) * (∏ i, (s i : ℝ)) ^ 2 * (3 * Es + 2) * hp p < 1)
    {ubar vbar : ((i : Fin (D + 1)) → ZMod (s i)) → ℂ}
    (hu1 : ‖(fun k => (2 : ℂ)⁻¹ ^ (b + 2) * ubar k)‖ ≤ 1 / 4)
    (hv1 : ‖(fun k => (2 : ℂ)⁻¹ ^ (b + 2) * vbar k)‖ ≤ 1 / 4)
    {U V Z : ((i : Fin (D + 1)) → ZMod (s i)) → ℂ}
    (hU : ‖U - Rperm s t (dftM s (fun k => (2 : ℂ)⁻¹ ^ (b + 2) * ubar k))‖ ≤ Es * hp p)
    (hV : ‖V - Rperm s t (dftM s (fun k => (2 : ℂ)⁻¹ ^ (b + 2) * vbar k))‖ ≤ Es * hp p)
    (hZ : ‖Z - Rperm s t (dftM s (cnj (QA p (U * V))))‖ ≤ Es * hp p) :
    Grid p (QA p (U * V)) ∧ ‖QA p (U * V)‖ ≤ 1 / 2 ∧
    ∀ j, ‖(2 : ℂ) ^ (2 * b + 4) * ((∏ i, (s i : ℝ) : ℝ) : ℂ) *
      (((∏ i, (s i : ℝ) : ℝ) : ℂ) * cnj Z j) - cconv s ubar vbar j‖ < 1 / 2

Context. KFM: the error chain per call

Every procedure of the assembly is specified per call (LineNeed, ChirpNeedR): its output is some list within the error bound, possibly depending on the machine state. So the chain is assembled from the bounds at the actual call points:

source_call: one source transform U = 2^γ ṽ from the computed A-lines output w, chirp output c = C̃(w) (any M̃r with the Prop 18 bound) and B₀-lines output ṽ: ‖U − R F_s u‖ ≤ 2^γ (εA + (Er + 22) + εB) hp (R F_s = 2^γ B₀ Q F_t A, Lemma 20).
final_call3: with three such values U ≈ RF u, V ≈ RF v, Z ≈ RF(conj Q_p(UV)), ‖2^{2b+4} S (S · conj Z_j) − (ū ∗ v̄)_j‖ < 1/2 for every j (pipeline_err3 + final_exact).

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

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFM
open Complex IntMul.OpenAI.RT IntMul.OpenAI.RC NLogN.KFZ
variable {D : ℕ}

Formal statement

theorem NLogN.KFM.final_call3 (p b : ℕ) (s t : Fin (D + 1) → ℕ) [∀ i, NeZero (s i)]
    (hcop : ∀ i, Nat.Coprime (s i) (t i)) (Es : ℝ)
    (hEs : Es * hp p ≤ 1 / 100)
    (hB2 : 2 * (2 : ℝ) ^ (2 * b + 4) * (∏ i, (s i : ℝ)) ^ 2 * (3 * Es + 2) * hp p < 1)
    {ubar vbar : ((i : Fin (D + 1)) → ZMod (s i)) → ℂ}
    (hu1 : ‖(fun k => (2 : ℂ)⁻¹ ^ (b + 2) * ubar k)‖ ≤ 1 / 4)
    (hv1 : ‖(fun k => (2 : ℂ)⁻¹ ^ (b + 2) * vbar k)‖ ≤ 1 / 4)
    {U V Z : ((i : Fin (D + 1)) → ZMod (s i)) → ℂ}
    (hU : ‖U - Rperm s t (dftM s (fun k => (2 : ℂ)⁻¹ ^ (b + 2) * ubar k))‖ ≤ Es * hp p)
    (hV : ‖V - Rperm s t (dftM s (fun k => (2 : ℂ)⁻¹ ^ (b + 2) * vbar k))‖ ≤ Es * hp p)
    (hZ : ‖Z - Rperm s t (dftM s (cnj (QA p (U * V))))‖ ≤ Es * hp p) :
    Grid p (QA p (U * V)) ∧ ‖QA p (U * V)‖ ≤ 1 / 2 ∧
    ∀ j, ‖(2 : ℂ) ^ (2 * b + 4) * ((∏ i, (s i : ℝ) : ℝ) : ℂ) *
      (((∏ i, (s i : ℝ) : ℝ) : ℂ) * cnj Z j) - cconv s ubar vbar j‖ < 1 / 2 := 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 `NLogN.KFM.final_call3`, Solutions/KFMChain.lean (lines 74–115) of the round-six development.

View graph