Lemma 12 as a uniform item-language program, for the bit network (m = 10⁶, W = W_b, τ = 1 − 2^{−50}): the…

Lemma 12 as a uniform item-language program, for the bit network (m = 10⁶, W = W_b, τ = 1 − 2^{−50}): the program l12I q m W_b, run with the uniform Prop. 11 code of the bit network as procedure table, interchanges the two [2^u] fields of every bit array of shape Pre ++ [2^u] ++ G ++ [2^u] ++ Suf, at cost ≤ K (V + 1) (Bb + 2)² u^τ.

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

theorem NLogN.KIL.lemma12_il :
    ∃ T q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∃ K : ℝ, 0 ≤ K ∧
      ∀ (u : ℕ) (Pre G Suf : Shape) (Bb : ℕ), 1 ≤ u →
      (∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
      zsz ((T * (q ^ 2 * vol (binShape Pre G Suf (2 ^ u)) + 1) ^ 2 : ℕ) : ℤ) ≤ Bb → 1 ≤ Bb →
      ∀ (I : List Sym) (s : IState HS) (F : Fin HS → List ℤ) (xs : List (ZMod 2))
        (LP LG LS LU : List ℤ),
      F kP = (vol Pre : ℤ) :: LP → F kG = (vol G : ℤ) :: LG → F NLogN.KIL.kS = (vol Suf : ℤ) :: LS →
      F aU = (u : ℤ) :: LU → F 0 = enc2 xs →
      F 8 = [] → F 9 = [] → F 10 = [] → F 11 = [] → F 15 = [] → F 20 = [] → F 21 = [] →
      F 23 = [] → F 24 = [] →
      xs.length = vol (binShape Pre G Suf (2 ^ u)) →
      ∃ c : ℕ, IRuns I (progU ((bitQC NetProp7.ind₀).toCircuit 1) (edgeTplQ (bitQC NetProp7.ind₀)))
        (l12I q (100 ^ 3) (Fintype.card (NetScalar.Wr NetProp7.ind₀))) (encK s F)
        (encK s (Function.update F 0 (enc2 (AModel.pull (binShape Pre G Suf (2 ^ u))
          (binShape Pre G Suf (2 ^ u)) (swapPos Pre.length (Pre.length + 1 + G.length)) 0 xs))))
        c ∧
        (c : ℝ) ≤ K * ((vol (binShape Pre G Suf (2 ^ u)) : ℝ) + 1) * ((Bb : ℝ) + 2) ^ 2 *
          (u : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50)

Context. The lemma belongs to the part KIL6: Lemma 12 as an item-language program, unconditional versions.

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.