The compact Lemma 13 code runs (round six, `l13C_runs`)

The compact Lemma 13 code runs as the row addition.

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

theorem IntMul.Kappa.R6.IL2C.l13C_runs {Ksw : ℝ} (hKsw : 0 ≤ Ksw) {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1}
    {τ : ℝ} (H : IntMul.Kappa.R6.IL2C.SwOK tab l12 τ Ksw) {N0 N1 N2 N3 K f ρ G R w : ℕ} {px py : Fin 3} {fl : ℤ}
    (hp : IntMul.Kappa.R6.IL2C.RP N0 N1 N2 N3 K f ρ G px py) (hR : 1 ≤ R) (hfl : 0 < fl ↔ px < py)
    (I : List Sym) (t : IState HS) (zs : List GI) (R0 : List Item)
    (hE : CEnv t (layR N0 N1 N2 N3 (f * K) G (f - 1) px py) K ρ G (f - 1) (ρ + (f - 1) * K)
      (R * (2 * (w + 1))) fl)
    (hN : ∃ L, t.G sN = .int ((2 * (vol (rect N0 N1 N2 N3 (f * K)) * R) : ℕ) : ℤ) :: L)
    (hW : ∃ L, t.G sW = .int (w : ℤ) :: L)
    (hg0 : t.G 0 = ints (gflat zs) ++ R0) (hl : zs.length = vol (rect N0 N1 N2 N3 (f * K)) * R)
    (hGB : GB w zs) :
    ∃ c, IRuns I tab (l13C l12) t
        (t.upd 0 (ints (gflat (permRecs (rect N0 N1 N2 N3 (f * K))
          (rowAddAddr K ρ f px py) R zs)) ++ R0)) c ∧
      (c : ℝ) ≤ cL13 Ksw τ N0 N1 N2 N3 K f ρ G R w px py

Context. Round six, compact controls (I2C): the compact Lemma 13 code

• layR: the record layout of a row addition (T, U in the top of N0, the bit-control field Bk at stride 1 in the bottom of N3, X, Y the slots px, py), layR_ok, layR_kval.
• midC: the compact phase (only when n = f - 1 > 0) and the top bit; midC_step: it is the record pull stepP (TlS ∘ flipS).
• l13C: to bits, midC, from bits; l13C_runs: it is the row addition permRecs (rect …) (rowAddAddr K ρ f px py).

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).