axA_all (KFY 12: one axis of the `A` pass)

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

theorem NLogN.KFY.axA_all (M : MulSpec) (X : Fin HS) (Kc : ℝ) (hXok : KFM.TrOk X zw zm) (hX0 : X ≠ 0)
    {n : ℕ} (hn : IntMul.OpenAI.Glue.n0 ≤ n) (k : ℕ) (hk : k < IntMul.OpenAI.Glue.dP n)
    (u : IState HS) (Xs : List KFB.GI) (R0 RD LP LA LE LD LZ LL LW L55 : List Item)
    (h0 : u.G 0 = ints (KFB.gflat Xs) ++ R0) (hD : u.G NLogN.KFY.dS = .int (KFM.srcN n k : ℤ) :: RD)
    (hP : u.G NLogN.KFY.yP = .int (IntMul.OpenAI.Glue.pP n : ℤ) :: LP) (hA : u.G yA = .int (IntMul.OpenAI.Glue.αP n : ℤ) :: LA)
    (hE : u.G KFM.zEl = .int (IntMul.OpenAI.Glue.ℓP n : ℤ) :: LE) (hDd : u.G KFM.zD = .int (IntMul.OpenAI.Glue.dP n : ℤ) :: LD)
    (hZ : u.G KFM.zDp = .int (KFM.dpN n : ℤ) :: LZ) (hL : u.G yL = .int (IntMul.OpenAI.Glue.LP n : ℤ) :: LL)
    (hW : u.G NLogN.KFY.yW = .int (HvdH.sWidth (IntMul.OpenAI.Glue.pP n) (IntMul.OpenAI.Glue.αP n) : ℤ) :: LW)
    (h55 : u.G cX = .int ((IntMul.OpenAI.Glue.dP n : ℤ) - k) :: L55)
    (hXs : Xs.length = (List.ofFn (KFM.tB n)).prod) (hGB : KFB.GB (IntMul.OpenAI.Glue.pP n + 2) Xs)
    (Bo mm Φ Bacc Q Bq : ℕ) (hM : MulBnd M mm Φ)
    (H : SapHyp (IntMul.OpenAI.Glue.pP n) (KFM.srcN n k) (2 ^ (IntMul.OpenAI.Glue.ℓP n - 1 + NLogN.KFY.bN n k)) (IntMul.OpenAI.Glue.αP n)
      (IntMul.OpenAI.Glue.pP n + 2) Bo mm Bacc Q)
    (HT : TabHyp (IntMul.OpenAI.Glue.pP n) (KFM.srcN n k) (2 ^ (IntMul.OpenAI.Glue.ℓP n - 1 + NLogN.KFY.bN n k)) (IntMul.OpenAI.Glue.αP n) Bq)
    (HQ : AxQA (2 ^ (IntMul.OpenAI.Glue.ℓP n - 1 + NLogN.KFY.bN n k)) (2 ^ (IntMul.OpenAI.Glue.LP n - (IntMul.OpenAI.Glue.ℓP n - 1 + NLogN.KFY.bN n k)))
      (IntMul.OpenAI.Glue.pP n + 2) Bo Q)
    (A B : ℕ) (hb : AxBnd n A B) :
    (axA X Kc).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)
          (sapL (IntMul.OpenAI.Glue.pP n) (KFM.srcN n k) (2 ^ (IntMul.OpenAI.Glue.ℓP n - 1 + NLogN.KFY.bN n k)) (IntMul.OpenAI.Glue.αP n)) Xs)) ++ R0) ∧
      (axA X Kc).ok M u ∧
      (axA X Kc).cost M u ≤ axAC Kc n k B 20
        (⌈trBound Kc (IntMul.OpenAI.Glue.pP n + 2) (IntMul.OpenAI.Glue.ℓP n - 1) (IntMul.OpenAI.Glue.dP n) ((List.ofFn (KFM.tB n)).prod)⌉₊ +
          trOver (IntMul.OpenAI.Glue.pP n + 2) (IntMul.OpenAI.Glue.ℓP n - 1) (IntMul.OpenAI.Glue.dP n))
        (sapAxCostQ (IntMul.OpenAI.Glue.pP n) (KFM.srcN n k) (2 ^ (IntMul.OpenAI.Glue.ℓP n - 1 + NLogN.KFY.bN n k)) (IntMul.OpenAI.Glue.αP n)
          (2 ^ (IntMul.OpenAI.Glue.LP n - (IntMul.OpenAI.Glue.ℓP n - 1 + NLogN.KFY.bN n k))) mm Φ Bacc Q Bq)

Context. The lemma belongs to the part KFY 12: one axis of the A pass.

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.