trBlk_all (KFY 6: generic combinators for the line passes)

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

theorem NLogN.KFY.trBlk_all (M : MulSpec) (X : Fin HS) (Kc : ℝ) (rw rm : Fin HS) (hd : TrOk X rw rm)
    (hX0 : X ≠ 0) {n : ℕ} (hn : IntMul.OpenAI.Glue.n0 ≤ n) (w m : ℕ) (t : IState HS) (h : TrRegs t n w m rw rm)
    (zs : List KFB.GI) (l : List Item) (h0 : t.G 0 = ints (KFB.gflat zs) ++ l)
    (hz : zs.length = AModel.vol (shPad (ℓP n - 1) (NLogN.KFM.bsN n m))) (hB : KFB.GB w zs)
    (hh : 1 ≤ ℓP n - 1) (hbs : NLogN.KFM.bsN n m ≠ []) :
    (trBlk X Kc rw rm).run t = t.upd 0 (ints (KFB.gflat (IntMul.HvdH.Ref.transposeL
        ((shPad (ℓP n - 1) (NLogN.KFM.bsN n m)).headD 1) (AModel.vol (shPad (ℓP n - 1) (NLogN.KFM.bsN n m)).tail) zs))
        ++ l) ∧
      (trBlk X Kc rw rm).ok M t ∧
      (trBlk X Kc rw rm).cost M t = 1 + ((descTrP X rw rm).cost (t.upd X (.mark :: t.G X)) +
        (⌈trBound Kc w (ℓP n - 1) (NLogN.KFM.bsN n m).length
          (AModel.vol (shPad (ℓP n - 1) (NLogN.KFM.bsN n m)))⌉₊ + trOver w (ℓP n - 1) (NLogN.KFM.bsN n m).length))

Context. The lemma belongs to the part KFY 6: generic combinators for the line passes.

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.