The `A` kernel v2 in IL (round six, `aK2_runs`)

The A kernel v2 in IL.

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

theorem J6Seg.KR.AK.aK2_runs {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
    {w2 bk win Q pk b φ1 φ2 B BH : ℕ}
    (hΦ1 : ∀ x y : ℤ, zsz x ≤ B → zsz y ≤ B → M.Φ x y ≤ φ1)
    (hΦ2 : ∀ x y : ℤ, zsz x ≤ b * (2 * (w2 + bk)) + 2 → zsz y ≤ b * (2 * (w2 + bk)) + 2 →
      M.Φ x y ≤ φ2)
    (hb : 1 ≤ b) (hn1 : 1 ≤ w2 + bk) (hbig : 2 * (2 * (w2 + bk)) * 2 ^ (2 * pk) < 2 ^ (b - 1))
    (hw2 : w2 ≤ win) (hbk : bk ≤ win)
    {aTab rTab cTab : List ℤ} (hal : aTab.length = w2) (hrl : rTab.length = w2 + bk)
    (hcl : cTab.length = bk)
    {Ka Kr Kc X0 : ℤ} (hKa : 0 ≤ Ka) (hKr : 0 ≤ Kr) (hKc : 0 ≤ Kc) (hX0 : 0 ≤ X0)
    (hta : TB (2 ^ Q * Ka) aTab) (htr : TB (2 ^ Q * Kr) rTab) (htc : TB (2 ^ Q * Kc) cTab)
    (hea : 2 ^ Q * Ka ≤ 2 ^ pk) (her : 2 ^ Q * Kr ≤ 2 ^ pk) (hec : 2 ^ Q * Kc ≤ 2 ^ pk)
    (he0 : X0 ≤ 2 ^ pk) (he1 : Ka * X0 + 1 ≤ 2 ^ pk)
    (he2 : ((w2 + bk : ℕ) : ℤ) * Kr * (Ka * X0 + 1) + 1 ≤ 2 ^ pk)
    (he3 : Kc * (((w2 + bk : ℕ) : ℤ) * Kr * (Ka * X0 + 1) + 1) + 1 ≤ 2 ^ pk)
    (hBz : 2 * (pk + 1) + 2 ≤ B) (hBb : b + 4 ≤ B) (hPB : Q + 3 ≤ B)
    (hBc : zsz ((2 * win + 2 * (w2 + bk) : ℕ) : ℤ) ≤ B)
    (hBH : ∀ v ∈ aHdr2 w2 bk win Q pk b, zsz v ≤ BH)
    (s : IState HS) (F : Fin HS → List ℤ) (x : List GI) (l : List ℤ)
    (hF : ∀ j, j ≠ 0 → j ≠ J6Seg.KR.dT → F j = []) (hdT : F J6Seg.KR.dT = aKTab2 w2 bk win Q pk b aTab rTab cTab)
    (h0 : F 0 = gflat x ++ l) (hxl : x.length = win) (hx : AB X0 x) :
    IRuns I iprog (aKprog2 pM) (encK s F)
      (encK s (Function.update F 0 (gflat (J6A.aKerL w2 bk win Q aTab rTab cTab x) ++ l)))
      (cAK2 w2 bk win pk b φ1 φ2 B BH)

Context. A lines, IL side 5b: the run of the A kernel v2

aK2_runs: as aK_runs, with the v2 table aKTab2 … (small header) on dT, the program aKprog2 pM and the cost cAK2 …; the header bound BH is over aHdr2 only (every entry O(Q + pk + b) bits), the two Kronecker constants live only inside the row (bound BkA).

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