Fine Lemma 12 for the bit network with the canonical item size: no Bb hypothesis; the cost is ≤ K' (V + 1)…

Fine Lemma 12 for the bit network with the canonical item size: no Bb hypothesis; the cost is ≤ K' (V + 1) u^τ (τ = 1 − 2^{−50}) for every u ≥ 1 and all positive shapes.

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

theorem NLogN.KFB.lemma12_fine_canon :
    ∃ T q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∃ K : ℝ, 0 ≤ K ∧
      ∀ (u : ℕ) (Pre G Suf : Shape), 1 ≤ u →
      (∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
      ∀ (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)

Context. The lemma belongs to the part KFB §0: fine Lemma 12 with the canonical item-size bound: lemma12_fine (KFEBit) bounds the cost by K ((V+1) u^τ + (u+1)^cE (Bb+2)²) for every item size bound Bb ≥ zsz (T (q² V + 1)²). Here we take the minimal admissible Bb and absorb the overhead term: since u + 1 ≤ zsz V, Bb = O(zsz V), and (zsz V)^k ≤ C_k · V (polylog_le_lin), the overhead is ≤ C (V + 1).

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.