pass_all (KFY 15: a whole line pass (generic in the width program and the axis body))

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

theorem NLogN.KFY.pass_all (M : MulSpec) (wP : RS) (ax : RM) (hw : cX ∉ ax.writes)
    {n : ℕ} (hn : IntMul.OpenAI.Glue.n0 ≤ n) (s : IState HS) (zs : List KFB.GI) (R0 R : List Item)
    (h0 : s.G 0 = ints (KFB.gflat zs) ++ R0)
    (hD : s.G NLogN.KFY.dS = ints (NLogN.KFY.descL (IntMul.OpenAI.Glue.pP n) (IntMul.OpenAI.Glue.αP n) (IntMul.OpenAI.Glue.ℓP n - 1) (IntMul.OpenAI.Glue.dP n) (KFM.dpN n)
      (srcsN n)) ++ R)
    (w Cw : ℕ) (hwP : ∀ (t : IState HS) (LP LA : List Item), t.G NLogN.KFY.yP = .int (IntMul.OpenAI.Glue.pP n : ℤ) :: LP →
      t.G yA = .int (IntMul.OpenAI.Glue.αP n : ℤ) :: LA → RSAll wP t (t.upd NLogN.KFY.yW (.int (w : ℤ) :: t.G NLogN.KFY.yW)) Cw)
    (fs : ℕ → List KFB.GI → List KFB.GI) (P : List KFB.GI → Prop) (hP0 : P zs)
    (hPstep : ∀ k < IntMul.OpenAI.Glue.dP n, ∀ X, P X → P (stepL ((List.ofFn (KFM.tB n)).rotate k) (fs k) X))
    (C : ℕ)
    (Hstep : ∀ k < IntMul.OpenAI.Glue.dP n, ∀ (u : IState HS) (Xs : List KFB.GI)
      (RD LP LA LE LD LZ LL LW L55 : List Item),
      u.G 0 = ints (KFB.gflat Xs) ++ R0 → u.G NLogN.KFY.dS = .int (KFM.srcN n k : ℤ) :: RD →
      u.G NLogN.KFY.yP = .int (IntMul.OpenAI.Glue.pP n : ℤ) :: LP → u.G yA = .int (IntMul.OpenAI.Glue.αP n : ℤ) :: LA →
      u.G KFM.zEl = .int (IntMul.OpenAI.Glue.ℓP n : ℤ) :: LE → u.G KFM.zD = .int (IntMul.OpenAI.Glue.dP n : ℤ) :: LD →
      u.G KFM.zDp = .int (KFM.dpN n : ℤ) :: LZ → u.G yL = .int (IntMul.OpenAI.Glue.LP n : ℤ) :: LL →
      u.G NLogN.KFY.yW = .int (w : ℤ) :: LW → u.G cX = .int ((IntMul.OpenAI.Glue.dP n : ℤ) - k) :: L55 → P Xs →
      ax.run u = ((u.upd yS (.int (KFM.srcN n k : ℤ) :: u.G yS)).upd NLogN.KFY.dS RD).upd 0
          (ints (KFB.gflat (stepL ((List.ofFn (KFM.tB n)).rotate k) (fs k) Xs)) ++ R0) ∧
        ax.ok M u ∧ ax.cost M u ≤ C)
    (A B : ℕ) (hEnv : KFM.CostEnv A B) (hpA : IntMul.OpenAI.Glue.pP n ≤ A) (hαA : IntMul.OpenAI.Glue.αP n ≤ A)
    (hlA : IntMul.OpenAI.Glue.ℓP n ≤ A) (hdlA : IntMul.OpenAI.Glue.dP n * IntMul.OpenAI.Glue.ℓP n ≤ A) (hwA : w ≤ A) (hLA : IntMul.OpenAI.Glue.LP n ≤ A)
    (hsrc : ∀ x ∈ srcsN n, zsz x ≤ B) :
    (passP wP ax).run s = s.upd 0 (ints (KFB.gflat (NLogN.KFY.iterL (List.ofFn (KFM.tB n)) fs (IntMul.OpenAI.Glue.dP n) zs))
        ++ R0) ∧
      (passP wP ax).ok M s ∧ (passP wP ax).cost M s ≤ passC (IntMul.OpenAI.Glue.dP n) B Cw C

Context. The lemma belongs to the part KFY 15: a whole line pass (generic in the width program and the axis body): passP wP ax = rs (proP; wP) ; rep cX (reg zD) ax ; rs epiP.

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.