The fine uniform offset-table generator

The fine uniform offset-table generator.

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

theorem NLogN.KFD.genPU_fsp {Q b : ℕ} (hQ0 : 0 < Q) (hQ : zsz ((2 * Q : ℕ) : ℤ) ≤ b)
    (ac : List (ℕ × ℕ)) (hac : ∀ p ∈ ac, 1 ≤ p.1 ∧ p.2 < Q)
    (t : IState HS) (LA LC LM LAM LN : List Item)
    (hA : t.G sSA = ints (ac.reverse.map fun p => (p.1 : ℤ)) ++ LA)
    (hC : t.G sSC = ints (ac.reverse.map fun p => (p.2 : ℤ)) ++ LC)
    (hM : t.G sSM = ints (stgM ac.reverse []) ++ LM)
    (hAM : t.G sSAM = ints (stgAM ac.reverse []) ++ LAM)
    (hN : t.G sNQ = .int (-(Q : ℤ)) :: LN) :
    FSp (genPU ac.length) t
      (((((t.upd 14 (ints (NLogN.KIL.tbl Q ac) ++ t.G 14)).upd sSA LA).upd sSC LC).upd sSM LM).upd sSAM LAM)
      ((1 + 1) * 2000 * (b + 2) + stCostF b ac.reverse [])

Context. The lemma belongs to the part KFD: the fine offset-table generator: Fine specifications of KIL2's genP stages and KIL4's uniform generator genPU (programs unchanged). All entries are residues < Q, so every element operation costs O(b) with the local bound zsz (2Q) ≤ b; loop counts enter only linearly (cLp N c N, since zsz N ≤ N). genPU_fsp: cost ≤ 10^9 · (n + 1) · (vol A + 1) · (b + 2), where vol A is the number of table entries (blocks). No global size bound is needed.

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.