Carries out

Carries out.

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

theorem NLogN.KFT.carI_spec (b B : ℕ) (hb : 1 ≤ b) (zs : List GI) (hre : ∀ z ∈ zs, 0 ≤ z.1)
    (hB : NLogN.KFB.GB B zs) (s : IState HS) (R0 : List Item) (h0 : s.G 0 = ints (gflat zs) ++ R0) :
    IRuns I iprog (carI b zs.length) s (s.upd 0 (.int (carOut b zs : ℤ) :: R0)) (cCar b B zs.length)

Context. The lemma belongs to the part KFT §2: carries out: carI b N: stack 0 holds the Gaussian array gflat zs (N entries, real parts c_j ≥ 0, imaginary parts discarded) on top of R0. Phase 1 runs the radix-2^b carry scan t := y + c_j, digit t mod 2^b, carry t / 2^b (one add and one split by the ruler 2^b per entry; the carry stays below 2^B). Phase 2 assembles the digits from the top with cat (O(b) each) starting from the sentinel carry + 1, while 2^{bN} is built by shl; one final add removes the sentinel. Result on stack 0: the integer Σ_j c_j 2^{bj} (valN), i.e. ∑_{h<N} c_h Q^h of RF.carry_digits with Q = 2^b (valN_eq_sum). Cost O((N + 1)(B + b + 1)) for GB B zs.

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.