Round-six lemma `chirp_sigma`

Proved

J6A.chirp_sigma

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6A.chirp_sigma (p s t α H : ℕ) (hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α) (hp : 3 ≤ p)
    (hH : H ≤ 2 * sWidth p α) (hθ : 300 * (t - s) ≤ s) :
    Real.exp (Real.pi * (s * (t - s) * H ^ 2 : ℕ) / ((t ^ 2 * α ^ 2 : ℕ) : ℝ)) ≤ 2 ^ (p / 2)

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_SApprox
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_HvdH_MachineRef

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open Complex
open IntMul.HvdH

Formal statement

theorem J6A.chirp_sigma (p s t α H : ℕ) (hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α) (hp : 3 ≤ p)
    (hH : H ≤ 2 * sWidth p α) (hθ : 300 * (t - s) ≤ s) :
    Real.exp (Real.pi * (s * (t - s) * H ^ 2 : ℕ) / ((t ^ 2 * α ^ 2 : ℕ) : ℝ)) ≤ 2 ^ (p / 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 `J6A.chirp_sigma`, Solutions/J6AMath5.lean (lines 45–89) of the round-six development.

View graph