phT_fsp (KFG: the phase table by doubling (task B, part 1))

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

theorem NLogN.KFG.phT_fsp (s : IState HS) (f : Fin HS → List ℤ) (K off u : ℕ) (aE : ℕ → ℕ)
    (pre seg : List GI) (l : List ℤ) (hpre : pre.length = off) (hseg : seg.length = 2 ^ K)
    (h0 : f 0 = gflat pre ++ (gflat seg ++ l)) (hC : ClT f) {w : ℕ} (hbp : NLogN.KFB.GB w pre)
    (hbs : NLogN.KFB.GB w seg) (Z : ℕ) (hZ : zsz ((4 * (off + 2 ^ K) : ℕ) : ℤ) ≤ Z) :
    FSp (phT K off u aE) (encK s f)
      (encK s (Function.update f 0 (gflat pre ++ (gflat (mulL (tbl u aE K) seg) ++ l))))
      (cPhT w K off Z)

Context. The lemma belongs to the part KFG: the phase table by doubling (task B, part 1): The phase i^{u + Σ_t aE t · bit_t q} of entry q < 2^K is produced as a table of exponents mod 4 on stack xA, built by K doubling steps: T ↦ T ++ map (· + aE t mod 4) T. The doubling step on a table of length M costs O(M) + O(Z), so the whole table costs O(2^K) + O(K Z) (geometric sum), i.e. O(1) per table entry.

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.