RowUP: the uniform Lemma 13 row addition, as the code (rowCodeU q).ren id (gL E) in every extension…

RowUP: the uniform Lemma 13 row addition, as the code (rowCodeU q).ren id (gL E) in every extension KFM.kTable ext (no extra procedures), with constant Kc + 8·10^12.

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

theorem NLogN.KFX.rowUP : KFW.RowUP

Context. The lemma belongs to the part KFX §7: RowUP, the uniform Lemma 13 row addition: rowCodeU q (over l12prog) implements Pm i j in SImplQ form for every admissible parameter set read from the background registers 36 … 45 (rowQ). The Lemma 13 cost ⌈bnd⌉ plus the header cost cHd is absorbed into bnd with the constant Kc + 8·10^12, and ceil_bnd_le turns it into the RowU form. The code is placed in KFM.kTable ext by relabelling the l12prog calls (kTable_l12); no extra procedures are needed (nR = 0).

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.