An `E₁`-approximation of `2^p S'` is an `FPApprox` of any line map fitted to `Sapprox` (`fp_of_sexact`)

Proved

J6A.fp_of_sexact

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

complexity-theoryinteger-multiplicationkappa-improvement

An E₁-approximation of 2^p S' is an FPApprox of any line map fitted to Sapprox.

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

theorem J6A.fp_of_sexact (p s t α : ℕ) [NeZero s] [NeZero t] (hα : 2 ≤ α) (hαp : α ^ 2 ≤ p)
    (Aa : (ℕ → ℤ × ℤ) → (ℕ → ℤ × ℤ)) (E₁ : ℝ)
    (hAa : ∀ U, InDisc p U → ∀ k,
      ‖gC (Aa U k) - 2 ^ p * Sexact s t α (fun i => gC (U i) / 2 ^ p) k‖ ≤ E₁)
    (L : (ZMod s → ℂ) →L[ℂ] (ZMod t → ℂ))
    (hL : ∀ U, InDisc p U → ∀ k : ZMod t,
      ‖gC (Sapprox p s t α U k.val) - 2 ^ p * L (fun j => gC (U j.val) / 2 ^ p) k‖
        ≤ 6 * sWidth p α + 4)
    (hE : 0.55 * 2 ^ p + E₁ ≤ 2 ^ p) :
    FPApprox p Aa (NLogN.KFM.liftL L) (E₁ + 12 * sWidth p α + 8)

Context. A lines (PR #5 block chirp), part 3: per-axis FPApprox

Sexact_resS: S'(u)_k = ½ · resS(u)_k.
Sexact_norm: ‖S'(u)_k‖ ≤ 0.55 · sup ‖u‖ (from resS_norm_le_tight, α ≥ 2).
fp_of_sexact: any fixed-point map Aa within E₁ of 2^p S' is an FPApprox of the lifted line map liftL L, for every L fitted to Sapprox within 6m+4 (the FitSpec6 clause), with error E₁ + 12m + 8, provided 0.55·2^p + E₁ ≤ 2^p.
chirpA_fp: the instance Aa = chirpA.

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_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 Mathlib
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 Complex
open IntMul.HvdH

Formal statement

theorem J6A.fp_of_sexact (p s t α : ℕ) [NeZero s] [NeZero t] (hα : 2 ≤ α) (hαp : α ^ 2 ≤ p)
    (Aa : (ℕ → ℤ × ℤ) → (ℕ → ℤ × ℤ)) (E₁ : ℝ)
    (hAa : ∀ U, InDisc p U → ∀ k,
      ‖gC (Aa U k) - 2 ^ p * Sexact s t α (fun i => gC (U i) / 2 ^ p) k‖ ≤ E₁)
    (L : (ZMod s → ℂ) →L[ℂ] (ZMod t → ℂ))
    (hL : ∀ U, InDisc p U → ∀ k : ZMod t,
      ‖gC (Sapprox p s t α U k.val) - 2 ^ p * L (fun j => gC (U j.val) / 2 ^ p) k‖
        ≤ 6 * sWidth p α + 4)
    (hE : 0.55 * 2 ^ p + E₁ ≤ 2 ^ p) :
    FPApprox p Aa (NLogN.KFM.liftL L) (E₁ + 12 * sWidth p α + 8) := 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 `J6A.fp_of_sexact`, Solutions/J6AMath3.lean (lines 56–100) of the round-six development.

View graph