A row addition on the node roles

A row addition on the node roles.

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

theorem NLogN.KFW.stepQ_row {rowC : IStmt HS Pp} {Kc : ℝ} (hRow : RowU Isym tbl rowC Kc)
    (hN : NodeR σ K t S0 r H k e B Bn) (hQ : ∀ s, Q s → Agree σ s) (hhi : hi ≤ H)
    (hK6 : 6 ≤ K) (hr : 1 ≤ r) (Z : ℕ) (hKZ : 80 * Z * (Z + 2) ≤ 2 ^ K) (hS : 1 ≤ S0)
    (hBn : 1 ≤ Bn) (hKe : K * (mC ^ (k + 1) - 1) ≤ e) (het : e - e % K + K ≤ t)
    (hZ : zsz ((16 * (P8Lift.Wc * (nN Bn t S0 * r)) : ℕ) : ℤ) ≤ Z) (Bz : ℕ)
    (hBz : zsz ((mC ^ k + K + e + t + S0 + Bn + r + H + mC : ℕ) : ℤ) ≤ Bz)
    (w : Fin P8Lift.Wc) (i j : Fin mC) (hij : i ≠ j) :
    ∃ cost : ℕ → ℕ,
      RImplQ Isym tbl Q lo hi r (nN Bn t S0) (stN K e k S0)
        ((P8Lift.RStep.rowAdd w i j hij : P8Lift.RStep (Fin P8Lift.Wc) mC).den
          (Butterfly.tens Cm : Butterfly.Op (Fin (mC ^ k))))
        (wrapQ P8Lift.Wc w.val wL NLogN.KFW.w1 (withPushI (rowPush i j) rowC)) 0 (0 + (0 + 2) * P8Lift.Wc)
        (cWrapQ P8Lift.Wc (nN Bn t S0 * r) Z 0 0
          (fun x => cFrame 10 1 Bz + cost x + (10 * (2 * Bz + 2) + 1))) ∧
      ∀ x, x ≤ H → (cost x : ℝ) ≤ (Kc * (K + 2) + 1) * ((nN Bn t S0 : ℕ) : ℝ) *
        ((r : ℝ) * (H + 1) * ((mC : ℝ) ^ k + 1) ^ τ50 + (KFR.PsiR r Z H : ℝ))

Context. The lemma belongs to the part KFW: pushes of fresh frames, and the uniform row-addition step.

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.