The kernel-pass wrapper (round six, `kerW_run`)

The kernel-pass wrapper.

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

theorem J6Seg.kerW_run {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {eF eB e : Fin Pp}
    {ρ : Fin 19 → Fin HS} {dT dF : Fin HS} {C₀ : ℝ} {tabOf : ℕ → List ℤ}
    {Pre : List GI → Prop} {g : ℕ → List GI → List GI} {Ck : ℝ}
    (hR : RegOK ρ dT dF) (hFine : FineBody6 Isym tbl eF eB dF C₀)
    (hRow : RowBody6 Isym tbl e dT tabOf Pre g Ck)
    (w w' f pre nc post B Lmax : ℕ) (hB : 1 ≤ B) (hpost : 1 ≤ post)
    (s : IState HS) (F : Fin HS → List ℤ) (L : List GI) (l R0 : List ℤ) (φ : ℕ → ℕ → List GI)
    (hF0 : F 0 = gflat L ++ l) (hFT : F dT = [])
    (h0 : F (ρ 0) = [(w : ℤ)]) (h1 : F (ρ 1) = [(w' : ℤ)]) (h2 : F (ρ 2) = [(f : ℤ)])
    (h3 : F (ρ 3) = [((pre * nc : ℕ) : ℤ)]) (h4 : F (ρ 4) = [(post : ℤ)])
    (h5 : F (ρ 5) = [(pre : ℤ)]) (h6 : F (ρ 6) = [(nc : ℤ)])
    (h7 : F (ρ 7) = [((2 * 2 ^ f : ℕ) : ℤ)])
    (h8 : F (ρ 8) = [((2 * (pre * nc * post * 2 ^ f) : ℕ) : ℤ)])
    (h9 : F (ρ 9) = [((tabsT tabOf nc).length : ℤ)])
    (h10 : F (ρ 10) = tabsT tabOf nc ++ R0)
    (hscr : ∀ i : Fin 19, 11 ≤ i.val → i.val ≤ 17 → F (ρ i) = [])
    (hzw : zsz (w : ℤ) ≤ B) (hzw' : zsz (w' : ℤ) ≤ B) (hzf : zsz (f : ℤ) ≤ B)
    (hzA : zsz ((pre * nc : ℕ) : ℤ) ≤ B) (hzp : zsz (post : ℤ) ≤ B)
    (hzpre : zsz (pre : ℤ) ≤ B) (hznc : zsz (nc : ℤ) ≤ B)
    (hzm : zsz ((2 * 2 ^ f : ℕ) : ℤ) ≤ B) (hzN : zsz ((2 * (pre * nc * post * 2 ^ f) : ℕ) : ℤ) ≤ B)
    (hzT : zsz ((tabsT tabOf nc).length : ℤ) ≤ B) (hzL : zsz (Lmax : ℤ) ≤ B) (hw'B : w' ≤ B)
    (hL : LRep (pre * nc) (2 ^ f) post L φ)
    (hPre : ∀ b < pre * nc, ∀ c < post, Pre (φ b c))
    (hg : ∀ q < nc, ∀ x, Pre x → x.length = 2 ^ f → (g q x).length = 2 ^ f ∧ GB w' (g q x))
    (hGB : GB w L)
    (hTB : ∀ q < nc, Bnd B (tabOf q)) (hTL : ∀ q < nc, (tabOf q).length ≤ Lmax) :
    ∃ c : ℕ, IRuns Isym tbl (kerW ρ dT dF eF eB e) (encK s F)
        (encK s (update F 0 (gflat (kerPass (2 ^ f) post (pre * nc) (fun b => g (b % nc)) L) ++ l)))
        c ∧
      (c : ℝ) ≤ C₀ * cFine w f (pre * nc) post + C₀ * cFine w' f (pre * nc) post +
        (kerC ⌊Ck⌋₊ B (2 ^ f) post Lmax nc (tabsT tabOf nc).length pre
          (2 * (pre * nc * post * 2 ^ f)) : ℝ)

Context. B-line IL, B2: kerW_run (the kernel-pass wrapper computes kerPass)

See J6SegILKer4 for the program and J6SegILKer1 for the register conventions.

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