The kernel on the gathered window computes `chirpC` (round six, `aKer_chirp`)

The kernel on the gathered window computes chirpC.

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

theorem J6A.aKer_chirp (p s t α H b win : ℕ) (hH : 1 ≤ H) (U : ℕ → ℤ × ℤ) (x : List (ℤ × ℤ))
    (hxl : 2 * WA p α H ≤ x.length)
    (hx : ∀ i < 2 * WA p α H, x.getD i (0, 0) =
      U ((jcB s t H (kkA H b) - WA p α H + i) % (s : ℤ)).toNat)
    {κ : ℕ} (hκ : κ < 2 * H) :
    (aKerL (2 * WA p α H) (2 * H) win (QA p) (aTabA p s t α H b)
        (rTabA p s t α H b) (cTabA p s t α H b) x).getD κ (0, 0) =
      chirpC p s t α H U (kkA H b + κ)

Context. A lines, IL side 1: the per-block kernel as a list function

aKerL w2 bk win Q aTab rTab cTab x (row x of length win, the gathered window):

All three stages use the one rounding exponent Q (the IL kernel has one rP register); the tables aTab, rTab are stored scaled by 2^Q, so the first two stages are exact:

1. scale: y = dgG Q aTab (x.take w2) (aTab_i = 2^Q a_i: exact products a_i x_i);
2. correlate: z = lwG Q (2n) rTab (padG n y) with n = w2 + bk (rTab_e = 2^Q r_e: exact lower Toeplitz sums, one record product);
3. extract z[w2 .. w2 + bk) and rescale: dgG Q cTab (one rounding rs Q per entry);
4. pad with zeros to win.

• aKerL_getD: the entries of aKerL as fixed-point products of the explicit window sums.
• The tables of block b of an A line: aTabA, rTabA, cTabA.
• aKer_chirp: on the gathered window of block b, aKerL with these tables gives the chirpC outputs k = b·bk + κ, κ < bk.

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*).