tabGen_fsp (KFL §5: the offset tables of the rotations (22))

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

theorem NLogN.KFL.tabGen_fsp {K ρ f : ℕ} (hK : 1 ≤ K) (hρK : ρ < K) (hf : 1 ≤ f) {d0 d1 Q : ℕ}
    (hd0 : 0 < d0) (hd1 : 0 < d1) (hQ : 0 < Q) (l : Line) (hs : l.sgn = 1 ∨ l.sgn = -1)
    (hb : l.b = 0 ∨ l.b = 1) {Bb : ℕ} (hB2 : 2 ≤ Bb) (hbig : 4 * 2 ^ (f * K) < 2 ^ Bb)
    (zd0 : zsz (d0 : ℤ) ≤ Bb) (zd1 : zsz (d1 : ℤ) ≤ Bb) (hQM : Q ≤ 2 ^ (f * K))
    (P : ℕ) (zP : zsz (P : ℤ) ≤ Bb)
    (s : IState HS) (F : Fin HS → List ℤ) (hq : F NLogN.KFL.rq = []) (hc : F rC = []) :
    FSp (tabGen K ρ f d0 d1 Q P l.sgn l.b) (encK s F)
      (encK s (Function.update F 14
        ((List.range P).map (fun p => (tabA K ρ f d0 d1 Q l p : ℤ)) ++ F 14)))
      (cTabGen K f l.b P Bb)

Context. The lemma belongs to the part KFL §5: the offset tables of the rotations (22).

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.