The configured chirp map is an `FPApprox` of every fitted line map (round six, `chirpC_fp`)

Proved

J6A.chirpC_fp

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

complexity-theoryinteger-multiplicationkappa-improvement

The configured chirp map is an FPApprox of every fitted line map.

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

theorem J6A.chirpC_fp (p s t α H : ℕ) [NeZero s] [NeZero t] (hst : s ≤ t) (hα : 2 ≤ α)
    (hαp : α ^ 2 ≤ p) (hH : 1 ≤ H) (hH2 : H ≤ 2 * sWidth p α) (hθ : 300 * (t - s) ≤ s)
    (hp : 3 ≤ p) (hWp : 12 * (H + sWidth p α + 3) ≤ 2 ^ (p / 2))
    (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) :
    FPApprox p (chirpC p s t α H) (NLogN.KFM.liftL L) (12 * sWidth p α + 11)

Context. A lines (PR #5 block chirp), part 5: the configured chirp map

Precision P = 2p, output exponent σ = ⌊p/2⌋, half-block 1 ≤ H ≤ 2m (m = sWidth p α), window half-width W = H + m + 3.

chirpA_congr: chirpA reads only [0, s).
chirp_sigma: exp(π s(t-s)H²/(t²α²)) ≤ 2^{⌊p/2⌋} once 300 (t-s) ≤ s.
chirpC_fp: chirpC is an FPApprox of liftL L within 12 m + 11 for every line map L fitted to Sapprox within 6m+4 (the FitSpec6 clause).

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_Defs61

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6A
open Complex
open IntMul.HvdH

Formal statement

theorem J6A.chirpC_fp (p s t α H : ℕ) [NeZero s] [NeZero t] (hst : s ≤ t) (hα : 2 ≤ α)
    (hαp : α ^ 2 ≤ p) (hH : 1 ≤ H) (hH2 : H ≤ 2 * sWidth p α) (hθ : 300 * (t - s) ≤ s)
    (hp : 3 ≤ p) (hWp : 12 * (H + sWidth p α + 3) ≤ 2 ^ (p / 2))
    (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) :
    FPApprox p (chirpC p s t α H) (NLogN.KFM.liftL L) (12 * sWidth p α + 11) := 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.chirpC_fp`, Solutions/J6AMath5.lean (lines 91–131) of the round-six development.

View graph