The padded B̃₀ axis step

The padded B̃₀ axis step.

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

theorem NLogN.KFY.bap0AxQ_all (M : MulSpec) (p s t α m kb Bi Bo mm Φ Bacc Q Bq : ℕ)
    (hM : MulBnd M mm Φ) (H : BapHyp p s t α kb Bi Bo mm Bacc Q) (HT : TabHypB p s t α Bq)
    (hα : 1 ≤ α) (HQ : AxQA t m Bi Bo Q)
    (st : IState HS) (L : List (ℤ × ℤ)) (Rest : List Item) (hR : BapRegsQ p s t α m kb st)
    (hD : st.G NLogN.GL.gD = gints L ++ Rest) (hL : L.length = m * t) (hLB : NLogN.GL.GB Bi L) :
    bap0AxQ.run st = st.upd NLogN.GL.gD (gints (b0OutQ p s t α L) ++ Rest) ∧
      bap0AxQ.ok M st ∧ bap0AxQ.cost M st ≤ bap0AxCostQ p s t α m mm Φ Bacc Q Bq ∧
      (b0OutQ p s t α L).length = m * t ∧ NLogN.GL.GB Bo (b0OutQ p s t α L)

Context. The lemma belongs to the part KFY 5: the B₀ line pass on one axis (bap0AxQ).

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.