The network (register counts, under the invariant)

The network (register counts, under the invariant).

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

theorem NLogN.KFD.netCF_runs {G0 : Fin HS → List Item} (Φ : M → List (ZMod 2) → List (ZMod 2))
    (Pr : M → Prop)
    (hΦl : ∀ X, Pr X → ∀ ys : List (ZMod 2), ys.length = v → (Φ X ys).length = v)
    (hE : ∀ X, Pr X → ∀ ys : List (ZMod 2), ys.length = v → ∀ (t : IState HS) (R : List Item),
      NLogN.KIL.Inv G0 t →
      IRuns I iprog (E X) (t.upd 0 (ints (enc2 ys) ++ R)) (t.upd 0 (ints (enc2 (Φ X ys)) ++ R))
        (cE X))
    (s : IState HS) (hs : NLogN.KIL.Inv G0 s) (rest : List ℤ) {Bb : ℕ} (hB : TabB W v Bb) (hv1 : 1 ≤ v)
    (Mout : Fin W → M) :
    ∀ (gates : List (NGate (Fin W) (ZMod 2) M)) (lab : Fin W → M) (Y : Fin W → Fin v → ZMod 2)
      (f : Fin HS → List ℤ), FramesOK Pr gates lab Mout →
      (∀ r, Prot r → f r = []) → RegS s f W v →
      f 0 = tabR 0 W (tabOf Y) ++ rest → f 21 = [] →
      IRuns I iprog (netCF E Mout lab gates) (encK s f)
        (encK s (Function.update f 0
          (tabR 0 W (tabOf (netRunF (funΦ v Φ) gates lab Mout Y)) ++ rest)))
        (netCIF cE (W * v) Bb Mout lab gates)

Context. The lemma belongs to the part KFD: the fine network of one level: KIL5Net's framesU_runs, gateCU_runs, netCU_runs for the fine table code (applyCF, fcode rebuildCU, KFDTab). Every frame change costs cE X + cCF (W·v) Bb, every gate cRebuildF W (W·v) Bb + 1; cCF V Bb = O(V) + O((Bb+2)^2).

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.