Fine Lemma 12 for the bit network, polylogarithmic overhead: the cost is ≤ K ((V + 1) u^τ + (zsz V)^cE (Bb…

Fine Lemma 12 for the bit network, polylogarithmic overhead: the cost is ≤ K ((V + 1) u^τ + (zsz V)^cE (Bb + 2)²), i.e. K (V+1) u^τ + O(polylog V) for the admissible Bb = O(log V).

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

theorem NLogN.KFE.lemma12_fine_polylog :
    ∃ T q₀ cE : ℕ, ∀ 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 (progF ((bitQC NetProp7.ind₀).toCircuit 1) (edgeTplQ (bitQC NetProp7.ind₀)))
        (l12F 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) * (u : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50) +
          (zsz ((vol (binShape Pre G Suf (2 ^ u)) : ℕ) : ℤ) : ℝ) ^ cE * ((Bb : ℝ) + 2) ^ 2)

Context. The lemma belongs to the part KFE: fine Lemma 12, 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.