A uniform leaf: push the parameters pl (read from registers of the background), run the uniform register…

A uniform leaf: push the parameters pl (read from registers of the background), run the uniform register program U, pop. The non-uniform O (with U.sub σ a header refinement of it) runs on the background with the pushed values.

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

theorem NLogN.KFW.leafPush {pl : List (Fin HS × Ex HS)} {U O : RS} {σ : Fin HS → Option ℤ} {X : ℕ}
    (hσ : SClean σ) (hw : NoW σ U) (hO : HRef O (RS.sub σ U) X) (hfo : KFD.fok O = true)
    (s : IState HS) (f : Fin HS → List ℤ) (Bb : ℕ)
    (hpl : PushOK (encK s f) Bb pl) (hv : ∀ q ∈ pl, zsz (q.2.eval (encK s f)) ≤ Bb)
    (h0 : (0 : Fin HS) ∉ pl.map Prod.fst) (hnd : (pl.map Prod.fst).Nodup)
    (hfe : ∀ q ∈ pl, f q.1 = [])
    (hag : ∀ i v, σ i = some v → (i, v) ∈ evalP (encK s f) pl)
    (ys : List ℤ) {c : ℕ}
    (H : FSp O (encK (pushSt s (evalP (encK s f) pl)) f)
      (encK (pushSt s (evalP (encK s f) pl)) (Function.update f 0 ys)) c) :
    IRuns I iprog (withPushI pl (fcode U)) (encK s f) (encK s (Function.update f 0 ys))
      (pushCost Bb pl + 400 * (c + X) + (pl.length * (2 * Bb + 2) + 1))

Context. The lemma belongs to the part KFW: header refinement, uniform leaves, parameters in the background.

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