The phase pass implements the diagonal phase

The phase pass implements the diagonal phase.

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

theorem NLogN.KFN.sImpl_phase {ι : Type*} [Fintype ι] [DecidableEq ι] (r S t B u : ℕ) (pos : ι → ℕ)
    (hpos : ∀ i, pos i < t) (a' : ι → ℕ) (hr : 0 < r) (hS : 0 < S) (hB : 1 ≤ B) (Z : ℕ)
    (hZ : zsz ((4 * (B * (S * r * 2 ^ t) + S * r + B + 1) : ℕ) : ℤ) ≤ Z) :
    SImpl r (fun i => 2 ^ pos i * S) (B * 2 ^ t * S)
      (Matrix.diagonal fun x => I ^ (u + ∑ i, a' i * (x i).val))
      (phL (S * r) t B u (aEof pos a')) 0 0 (fun w => cPhL w (B * (S * r * 2 ^ t)) t B Z)

Context. The lemma belongs to the part KFN: the phase pass as a selected-bit operator: For selected bits i : ι at record strides 2^{pos i} · S (pos i < t) on B · 2^t · S records of r entries, the phase pass phL (S r) t B u (aEof pos a') implements the diagonal x ↦ i^{u + Σ_i a'_i x_i} (sImpl_phase), exactly (no scale, no width change), at cost cPhL, linear in the data.

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_Defs20.