Digits in

Digits in. Stack tX holds x < 2^{bM}; afterwards tX is popped and stack 0 carries gflat (digG b e M S x) on top of its old contents.

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

theorem NLogN.KFT.digI_spec (b e M S x : ℕ) (hx : x < 2 ^ (b * M)) (s : IState HS) (LX : List Item)
    (hX : s.G tX = .int (x : ℤ) :: LX) :
    IRuns I iprog (digI b e M S) s
      ((s.upd tX LX).upd 0 (ints (gflat (digG b e M S x)) ++ s.G 0)) (cDig b e M S)

Context. The lemma belongs to the part KFT §1: digits in: digI b e M S: with x ≥ 0, x < 2^{bM} on stack tX, it cuts the M radix-2^b digits a_j = ⌊x / 2^{bj}⌋ mod 2^b off x (one split by the ruler 2^b each, cost O(b) independently of the size of the rest), and leaves on stack 0 the Gaussian array digG b e M S x = [(a_0 2^e, 0), …, (a_{M-1} 2^e, 0), (0,0), …] of S entries (gflat form), i.e. the scaled input coefficients a_j 2^{p-b-2} of §9.2.3 padded to S entries (e = p-b-2). Cost O(M (b + e + 1) + S + 1), all loop counters unary.

Formalization Note. This lemma belongs to the item-language (IL) layer of the integer-multiplication-kappa campaign: tape-level programs (register programs over 64 item stacks of the NLogN multitape framework, definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8) that implement the data-movement primitives of the OpenAI preprint Integer multiplication below $n\log n$ (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine $O(1)$-per-element costs, Gaussian record primitives, Proposition 14 pieces) with exact list denotations from the array-model bundles IntMul_Kappa_K_Defs* and explicit cost bounds. All names refer to the definition bundles up to IntMul_Kappa_K_Defs18.