A kernel pass is a `PassOK` step (round six, `kpass_ok`)

A kernel pass is a PassOK step.

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

theorem J6Seg.Ax.kpass_ok {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {eF eB e eUp eDn : Fin Pp}
    {ρ : Fin 19 → Fin HS} {dT dF dA : Fin HS} {C₀ Cp : ℝ} {tabOf : ℕ → List ℤ}
    {Pre : List GI → Prop} {g : ℕ → List GI → List GI} {Ck : ℝ} {desc : List ℤ}
    (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 : ℕ)
    (hSet : SetupBody6 Isym tbl eUp eDn ρ dA desc
      (kerRegs w w' f pre nc post (tabsT tabOf nc)) Cp)
    (hρA : ∀ i, ρ i ≠ dA) (hA0 : dA ≠ 0) (hTA : dT ≠ dA)
    (hB : 1 ≤ B) (hpost : 1 ≤ post)
    (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)
    (hg : ∀ q < nc, ∀ x, Pre x → x.length = 2 ^ f → (g q x).length = 2 ^ f ∧ GB w' (g q x))
    (hTB : ∀ q < nc, Bnd B (tabOf q)) (hTL : ∀ q < nc, (tabOf q).length ≤ Lmax) :
    PassOK Isym tbl (kpSt eUp eDn ρ dT dF eF eB e) dA desc
      (fun L => L.length = pre * nc * (2 ^ f * post) ∧ GB w L ∧
        ∀ b < pre * nc, ∀ c < post, Pre (lineAt (2 ^ f) post L b c))
      (kerPass (2 ^ f) post (pre * nc) (fun b => g (b % nc)))
      (2 * Cp + (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 axis program (AxisU6), part 2: a kernel pass as a PassOK step

kpSt eUp eDn ρ dT dF eF eB e = call eUp; kerW ρ dT dF eF eB e; call eDn: the set-up of the register file kerRegs … from the descriptor (SetupBody6, B5), the kernel-pass wrapper (kerW_run, B2) with a row kernel (RowBody6), the tear-down.

kpass_ok: under the hypotheses of kerW_run (the row facts given by lineAt, the rows of the array), the step is PassOK for kerPass (2^f) post (pre·nc) (fun b => g (b % nc)), at cost 2 Cp + (the kerW_run bound).

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