Lemma 13 in IL (the corrected statement of KFH_WIP.lem13_iruns, see KFL_WIP): records of R Gaussian…

Lemma 13 in IL (the corrected statement of KFH_WIP.lem13_iruns, see KFL_WIP): records of R Gaussian entries on rect N0 N1 N2 N3 (fK) are moved by rowAddAddr (the packed selected-bit row addition y ← y ⊕ (x ∧ selMask), x = slot px, y = slot py), at cost V (w+1) (L^τ + 1) + M A³ + δ_bad M A (R (w+1) + A) with τ = 1 - 2^{-50}, L = fK, M = vol rect, A = zsz (2 V (w+1)) + 1.

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

theorem NLogN.KFL.lem13_il :
    ∃ (code : ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → Fin 3 → Fin 3 → IStmt HS 1) (Kc : ℝ), 0 < Kc ∧
    ∀ {I : List Sym} (N0 N1 N2 N3 K f ρ R w : ℕ) (px py : Fin 3), px ≠ py → 6 ≤ K → ρ < K →
      1 ≤ f → 1 ≤ N0 → 1 ≤ N1 → 1 ≤ N2 → 1 ≤ N3 → 1 ≤ R →
      ∀ (s : IState HS) (g : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
      g 0 = gflat zs ++ l → zs.length = vol (rect N0 N1 N2 N3 (f * K)) * R → NLogN.KFB.GB w zs →
      ∃ c, IRuns I l12prog (code N0 N1 N2 N3 K f ρ R w px py) (encK s g)
          (encK s (Function.update g 0 (gflat (permRecs (rect N0 N1 N2 N3 (f * K))
            (rowAddAddr K ρ f px py) R zs) ++ l))) c ∧
        (c : ℝ) ≤ Kc * ((zs.length : ℝ) * (w + 1) * (((f * K : ℕ) : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50) + 1) +
          (vol (rect N0 N1 N2 N3 (f * K)) : ℝ) * ((zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1) ^ 3 +
          min 1 (80 * ((f : ℝ) - 1) * 2⁻¹ ^ K) * (vol (rect N0 N1 N2 N3 (f * K)) : ℝ) *
            ((zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1) * ((R : ℝ) * (w + 1) +
              (zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1))

Context. The lemma belongs to the part KFL §18: Lemma 13 in IL: lem13_il (the corrected statement of KFH_WIP.lem13_iruns, see KFL_WIP): integers → bits (toBitsI), the slot canonicalisation by at most two Lemma-12 swaps (swSeq (preL px py)), the packed lines (linesI), the guard-set correction (corrI), the last selected bit (xorStep), the inverse swaps and bits → integers (fromBitsI). The composite is permRecs (rowAddAddr …) (bits_permRecs, pipeline_rixT, Fpp_conj); the cost is of the form (19) with τ = 1 - 2^{-50}.

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