The entries of the kernel (round six, `aKerL_getD`)

The entries of the kernel.

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

theorem J6A.aKerL_getD (w2 bk win Q : ℕ) (aTab rTab cTab : List ℤ) (x : List (ℤ × ℤ))
    (hx : w2 ≤ x.length) (ha : w2 ≤ aTab.length) (hr : w2 + bk ≤ rTab.length)
    (hc : bk ≤ cTab.length) (a r : ℕ → ℤ) (haa : ∀ i < w2, aTab.getD i 0 = 2 ^ Q * a i)
    (hrr : ∀ e < w2 + bk, rTab.getD e 0 = 2 ^ Q * r e) {κ : ℕ} (hκ : κ < bk) :
    (aKerL w2 bk win Q aTab rTab cTab x).getD κ (0, 0) =
      (J6Seg.fmul Q (cTab.getD κ 0) (kSum w2 a r (fun i => (x.getD i (0, 0)).1) κ),
        J6Seg.fmul Q (cTab.getD κ 0) (kSum w2 a r (fun i => (x.getD i (0, 0)).2) κ))

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