toUL_runs (KFC: linear-time binary → unary conversion)

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

theorem NLogN.KFC.toUL_runs {A X : Fin HS} (hAK : A ≠ uK) (hXK : X ≠ uK) (hXR : X ≠ uR) (hXY : X ≠ uY)
    (hXB : X ≠ uB) (s : IState HS) (n : ℕ) (LA : List Item) (hA : s.G A = .int n :: LA)
    (hX : NM (s.G X)) :
    IRuns I iprog (toUL A X) s (s.upd X (marks n ++ s.G X)) (cUL n)

Context. The lemma belongs to the part KFC: linear-time binary → unary conversion: toUL A X pushes n marks on X (n ≥ 0 the integer on top of A) in time O(n + zsz n): the bits of n are peeled off with split by the ruler 2 (cost O(1) each, since split costs O(m) for the ruler 2^m), then the unary count is rebuilt from the most significant bit by doubling (dbl, cost O(c) for count c; the doublings sum to O(n)).

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.