A row addition (round six, `stepH_row`)

A row addition on the node roles.

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

theorem IntMul.Kappa.R6.IL3H.stepH_row {rowC : IStmt HS Pp} {aK : ℕ → ℝ} {τ : ℝ} {G : ℕ}
    (hRow : RowUCG c.m τ Isym tbl rowC aK G) (hG24 : σ vG = some (G : ℤ))
    (hN : NodeRH c σ K t S0 r H E e B) (hQ : ∀ s, Q s → Agree σ s) (hhi : hi ≤ H)
    (hm : 1 ≤ c.m) (hF : 1 ≤ E / c.m) (hW : 1 ≤ c.Wr)
    (hK6 : 6 ≤ K) (hr : 1 ≤ r) (Z : ℕ) (hZG : 4 * Z * (Z + 2) ≤ 2 ^ G)
    (hGK : 16 * Z * (Z + 2) * 2 ^ G ≤ 2 ^ K) (hS : 1 ≤ S0)
    (hBn : 1 ≤ B / c.W) (hKe : K * (c.m * (E / c.m) - 1) ≤ e) (het : e - e % K + K ≤ t)
    (hdB : 2 ^ (2 * ((E / c.m - 1) * G)) ∣ B / c.W) (hdS : 2 ^ ((E / c.m - 1) * G) ∣ S0)
    (hZ : zsz ((16 * (c.Wr * (nN (B / c.W) t S0 * r)) : ℕ) : ℤ) ≤ Z) (Bz : ℕ)
    (hBz : zsz ((E / c.m + K + e + t + S0 + B / c.W + r + H + c.m : ℕ) : ℤ) ≤ Bz)
    (hGz : zsz (G : ℤ) ≤ Bz)
    (w : Fin c.Wr) (i j : Fin c.m) (hij : i ≠ j) :
    ∃ cost : ℕ → ℕ,
      RImplQ Isym tbl Q lo hi r (nN (B / c.W) t S0) (stH c.m K e (E / c.m) S0)
        ((RStep.rowAdd w i j hij : RStep (Fin c.Wr) c.m).den (1 : Op (Fin (E / c.m))))
        (wrapQ c.Wr w.val wL w1 (withPushI (rowPushH i.val j.val) rowC)) 0 (0 + (0 + 2) * c.Wr)
        (cWrapQ c.Wr (nN (B / c.W) t S0 * r) Z 0 0
          (fun x => cFrame 13 1 Bz + cost x + (13 * (2 * Bz + 2) + 1))) ∧
      ∀ x, x ≤ H → (cost x : ℝ) ≤ aK K * ((nN (B / c.W) t S0 : ℕ) : ℝ) *
        ((r : ℝ) * (H + 1) * (((E / c.m : ℕ) : ℝ) + 1) ^ τ + (KFR.PsiR r Z H : ℝ))

Context. Round six, item language (I3): the local steps of a node

A node on E bits (F = E / m) acts on W + T role streams of nN (B/W) t S₀ records, bits Fin m × Fin F at the positions IL3F.posR m K e F, strides stH. Parametric copies of the frozen KFWStep1/2/3/5 step lemmas (P8Lift.Wc → W + T, mC → m, mC^k → F):

• stepH_gate (atoms), stepH_perm (role permutation), stepH_phase (with epsOK_tabM, the m-generic epsOK_tab), stepH_fixG (a ±1 role diagonal as phase steps), stepH_row (from RowUCG, a row interface with a general coefficient aK K).

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*).