The A pass

The A pass.

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

theorem NLogN.KFY.passA_all (M : MulSpec) (X : Fin HS) (Kc : ℝ) (hXok : KFM.TrOk X zw zm) (hX0 : X ≠ 0)
    (hw : cX ∉ (axA X Kc).writes)
    {n : ℕ} (hn : IntMul.OpenAI.Glue.n0 ≤ n) [∀ i, NeZero (KFM.sB n i)] [∀ i, NeZero (KFM.tB n i)]
    (Mx : KFM.AxisMaps (d := IntMul.OpenAI.Glue.dP n) (IntMul.OpenAI.Glue.pP n) (IntMul.OpenAI.Glue.αP n) (KFM.sB n) (KFM.tB 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)
    (hzs : ArrInv n zs)
    (Bo mm Φ Bacc Q Bq : ℕ) (hM : MulBnd M mm Φ)
    (HA : ∀ k < IntMul.OpenAI.Glue.dP n, SapHyp (IntMul.OpenAI.Glue.pP n) (KFM.srcN n k) (tN n k) (IntMul.OpenAI.Glue.αP n)
      (IntMul.OpenAI.Glue.pP n + 2) Bo mm Bacc Q ∧ TabHyp (IntMul.OpenAI.Glue.pP n) (KFM.srcN n k) (tN n k) (IntMul.OpenAI.Glue.αP n) Bq ∧
      AxQA (tN n k) (NLogN.KFY.mN n k) (IntMul.OpenAI.Glue.pP n + 2) Bo Q)
    (A B : ℕ) (hb : AxBnd n A B) (hWB : zsz (((IntMul.OpenAI.Glue.pP n + 1) * (IntMul.OpenAI.Glue.pP n + 1) * (IntMul.OpenAI.Glue.αP n + 1) : ℕ) : ℤ) ≤ B)
    (hlA : IntMul.OpenAI.Glue.ℓP n ≤ A) (hdlA : IntMul.OpenAI.Glue.dP n * IntMul.OpenAI.Glue.ℓP n ≤ A)
    (CA : ℕ) (hCA : ∀ k < IntMul.OpenAI.Glue.dP n, 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) (tN n k) (IntMul.OpenAI.Glue.αP n) (NLogN.KFY.mN n k) mm Φ Bacc Q Bq) ≤ CA) :
    (progA X Kc).run s = s.upd 0 (ints (KFB.gflat
        (tensorGo (mapsA (IntMul.OpenAI.Glue.pP n) (IntMul.OpenAI.Glue.αP n) (KFM.sB n) (KFM.tB n)) (List.ofFn (KFM.tB n)) zs))
        ++ R0) ∧
      (progA X Kc).ok M s ∧
      (progA X Kc).cost M s ≤ passC (IntMul.OpenAI.Glue.dP n) B
        ((IntMul.OpenAI.Glue.pP n + 1) * 29 * 10 ^ 7 * (B + 2) ^ 2 + 4 * 10 ^ 7 * (B + 2) ^ 2) CA

Context. The lemma belongs to the part KFY 16: the A pass and the B₀ pass: The arrays keep the invariant length = ∏ t_i, DiscL p (which gives GB (p + 2)), using an M : AxisMaps (disc_sapL, disc_b0Pad).

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.