One chirp row keeps `GB (p + 2)` (round six, `chirpC_gb`)

Proved

J6A.chirpC_gb

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

complexity-theoryinteger-multiplicationkappa-improvement

One chirp row keeps GB (p + 2).

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

theorem J6A.chirpC_gb (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 : 24 ≤ p) (hWp : 12 * (H + sWidth p α + 3) ≤ 2 ^ (p / 2))
    (U : ℕ → ℤ × ℤ) (hU : ∀ i, zsz (U i).1 ≤ p + 2 ∧ zsz (U i).2 ≤ p + 2) (k : ℕ) :
    zsz (chirpC p s t α H U k).1 ≤ p + 2 ∧ zsz (chirpC p s t α H U k).2 ≤ p + 2

Context. PipeGBA6, part 1: one chirp row keeps GB (p + 2)

chirpC_gb: if every input entry has parts of bit size ≤ p + 2 (so ‖U_i‖ ≤ 4√2 · 2^p), every output entry of chirpC p s t α H has parts of bit size ≤ p + 2: ‖out‖ ≤ 2^p ‖S'(U/2^p)‖ + E ≤ 0.55 · 5.66 · 2^p + 10 < 2^{p+2} (chirpA_err8 with ex = 3, Sexact_norm, the window error E ≤ 8 · 1 + 2 as in chirpC_fp).

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 IntMul.HvdH.SPf
open NLogN (zsz)

Formal statement

theorem J6A.chirpC_gb (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 : 24 ≤ p) (hWp : 12 * (H + sWidth p α + 3) ≤ 2 ^ (p / 2))
    (U : ℕ → ℤ × ℤ) (hU : ∀ i, zsz (U i).1 ≤ p + 2 ∧ zsz (U i).2 ≤ p + 2) (k : ℕ) :
    zsz (chirpC p s t α H U k).1 ≤ p + 2 ∧ zsz (chirpC p s t α H U k).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.chirpC_gb`, Solutions/J6PipeGBA1.lean (lines 32–129) of the round-six development.

View graph