rpt_runs (KFT §0: a counted repetition with a literal count)

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

theorem NLogN.KFT.rpt_runs {A C D : Fin HS} (hAC : A ≠ C) (hAD : A ≠ D) (hCD : C ≠ D) (hAK : A ≠ sK)
    (hCK : C ≠ sK) (hCK2 : C ≠ sK2) (hCY : C ≠ uY) (hCB : C ≠ uB)
    (n : ℕ) (T : ℕ → IState HS)
    (hTA : ∀ k, (T k).G A = (T 0).G A) (hTC : ∀ k, (T k).G C = (T 0).G C)
    (hTD : ∀ k, (T k).G D = (T 0).G D)
    (b : IStmt HS Pp) (c : ℕ)
    (hb : ∀ k < n, ∀ LA LC LD, IRuns I iprog b (cf3 (T k) A C D LA LC LD)
      (cf3 (T (k + 1)) A C D LA LC LD) c) :
    IRuns I iprog (rpt A C D n b) (T 0) (T n) (n * (c + 64) + 60 + cRpt n)

Context. The lemma belongs to the part KFT §0: a counted repetition with a literal count: rpt A C D n b: push the literal n on A, turn it into n marks on C (KFC pro, linear cUL n), run b once per mark (uloop, 64 per iteration), clean up (epi) and drop n. rpt_runs: if b takes T k to T (k+1) whatever A, C, D hold, then rpt takes T 0 to T n at cost n (c + 64) + cRpt n, cRpt n = O(n + 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.