The segment loop. n iterations; afterwards rA holds a + segAcc … n

The segment loop. n iterations; afterwards rA holds a + segAcc … n.

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

theorem NLogN.KFL.segLoop_fsp {K : ℕ} (hK : 1 ≤ K) {T : Ex HS} {tf : ℤ → ℤ → ℤ} {Bb : ℕ}
    (hT : SegT T tf Bb) (s : IState HS) (F : Fin HS → List ℤ) (hF : F rC = [])
    (a u v w : ℤ) (hu : 0 ≤ u) (hv : 0 ≤ v) (hw : 0 < w)
    (n : ℕ) (hub : zsz u ≤ Bb) (hvb : zsz v ≤ Bb) (hKb : zsz ((2 : ℤ) ^ K) ≤ Bb)
    (hnb : zsz (n : ℤ) ≤ Bb) (hbig : |a| + 2 * w * 2 ^ (n * K) < 2 ^ Bb) :
    FSp (segLoop K n T) (encK s (segF F K tf a u v w 0)) (encK s (segF F K tf a u v w n))
      (cLp n (cSegIt T Bb) Bb)

Context. The lemma belongs to the part KFL §3: the segment loop (register programs): All per-record / per-block arithmetic of Lemma 13 is a loop over the n segments j_i = ρ + iK: with u, v the two chunk values shifted by 2^ρ, w = 2^ρ,

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.