The two-stream pass qop (fine cost): with G in register rG and 2·G·S in rN (S = 2·B1·|Ms| entries per…

The two-stream pass qop (fine cost): with G in register rG and 2·G·S in rN (S = 2·B1·|Ms| entries per group), the first G·S Gaussian entries of stack 0 are replaced by qopL Ms B1 G zs.

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

theorem NLogN.KFB.qop_fsp (s : IState HS) (w B1 G : ℕ) (Ms : List M2G) (hM : ∀ M ∈ Ms, M.Ok)
    (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ)
    (hlen : G * (2 * B1 * Ms.length) ≤ zs.length)
    (h0 : f 0 = gflat zs ++ l) (hS : Scr f) (hc : Cnt s f B1) (hA : f qA = []) (hG : f cG = [])
    {LG LN : List Item} (hrG : (encK s f).G rG = .int (G : ℤ) :: LG)
    (hrN : (encK s f).G rN = .int ((2 * (G * (2 * B1 * Ms.length)) : ℕ) : ℤ) :: LN)
    (hb : NLogN.KFB.GB w zs) :
    FSp (qop Ms) (encK s f)
      (encK s (Function.update f 0
        (gflat (qopL Ms B1 G zs ++ zs.drop (G * (2 * B1 * Ms.length))) ++ l)))
      (cQop w B1 Ms.length G)

Context. The lemma belongs to the part KFB: the two-stream pass qop (fine cost): On a Gaussian array viewed as consecutive blocks [u ‖ v] of two streams of B1 entries each, qop Ms applies the small 2 × 2 Gaussian matrix M_p = Ms[p mod L] (L = |Ms|) to block p: (u, v) ↦ (M₀₀ u + M₀₁ v, M₁₀ u + M₁₁ v) entrywise. With a single matrix this is a selected-bit kernel on a field [2] (the C kernel (25) scaled by 2, a phase on the selected half, a sign); with the period [1, X] it is a CNOT whose control is the field just before.

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.