Lemma 13, register-driven: the denotation and the cost pieces (KFL.l13_runs for l13U)

Lemma 13, register-driven: the denotation and the cost pieces (KFL.l13_runs for l13U).

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

theorem NLogN.KFX.l13U_runs {q : ℕ} {Ksw Kc : ℝ} (hKsw : 0 ≤ Ksw) (hKc : 0 ≤ Kc) (HSw : SwEOK q Ksw)
    (HC : CorrUOK Kc) (hne : px ≠ py) (hK6 : 6 ≤ K) (hp : PPos N0 N1 N2 N3 K f ρ R)
    (I : List Sym) (t : IState HS) (hA : Agree (σMR N0 N1 N2 N3 K f ρ R w px py) t)
    (zs : List GI) (R0 : List Item) (h0 : t.G 0 = ints (gflat zs) ++ R0)
    (hl : zs.length = vol (rect N0 N1 N2 N3 (f * K)) * R) (hGB : NLogN.KFB.GB w zs) :
    ∃ c, IRuns I l12prog (l13U q) t
        (t.upd 0 (ints (gflat (permRecs (rect N0 N1 N2 N3 (f * K))
          (rowAddAddr K ρ f px py) R zs)) ++ R0)) c ∧
      (c : ℝ) ≤ 2000 * (cTo (2 * (vol (rect N0 N1 N2 N3 (f * K)) * R)) w : ℝ) +
        4 * (26 + Ksw * (((NLogN.KFX.gB N0 N1 N2 N3 K f R w).V : ℝ) + 1) *
          ((f * K : ℕ) : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50)) +
        (400 * NLogN.KFL.coreCost Ksw Kc K ρ f (NLogN.KFX.gB N0 N1 N2 N3 K f R w) +
          10 ^ 10 * (((zsz ((NLogN.KFX.gB N0 N1 N2 N3 K f R w).V : ℤ) + 3 : ℕ) : ℝ) + 2) ^ 2) +
        2000 * (cFrom (2 * (vol (rect N0 N1 N2 N3 (f * K)) * R)) w : ℝ)

Context. The lemma belongs to the part KFX §4: the register-driven Lemma 13 core: The fixed code l13U q is KFL.l13code with every size-dependent literal read from the master registers (MReg): w, 2·M·R on 1, 6 (for toBitsU/fromBitsU), the swap flags on 11, 12, and Q = 2^{fK}, B = R·2(w+1), 2^ρ, gx, N0, N1, N2, N3, A = zsz V, 2^K on 13, 15, 16, 17, 18, 19, 46, 47, 48, 49, f, K on 36, 37. The slot swaps preL px py are realized by two optional swaps (optA: swap 0 or 2 by the flag on 11, optB: swap 1 by the flag on 12). l13U_runs is KFL.l13_runs for this code.

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.