The header cost is absorbed by 8·10^12 times the Lemma 13 bracket. -/ theorem cHd_le_bnd (Kc : ℝ) {K f n r…

The header cost is absorbed by 8·10^12 times the Lemma 13 bracket. -/ theorem cHd_le_bnd (Kc : ℝ) {K f n r w : ℕ} (hn : 1 ≤ n) (hf : 1 ≤ f) : KFR.bnd Kc K f n r w + (cHd (zsz (2 * ((n * r : ℕ) : ℤ) * ((w : ℤ) + 1))) : ℝ) ≤ KFR.bnd (Kc + 8 * 10 ^ 12) K f n r w := by rw [bnd_add] set X : ℝ := (zsz (2 * ((n * r : ℕ) : ℤ) * ((w : ℤ) + 1)) : ℝ) with hXd have hX0 : 0 ≤ X := Nat.cast_nonneg _ have hc : (cHd (zsz (2 * ((n * r : ℕ) : ℤ) * ((w : ℤ) + 1))) : ℝ) = 10 ^ 12 * (X + 2) ^ 3 := by simp only [cHd, Nat.cast_mul, Nat.cast_pow, Nat.cast_add, Nat.cast_ofNat, hXd] rw [hc] have h1 : (X + 2) ^ 3 ≤ 8 * (X + 1) ^ 3 := by nlinarith [sq_nonneg (X + 1)] have hn' : (1 : ℝ) ≤ n := by exact_mod_cast hn have h2 : (X + 1) ^ 3 ≤ (n : ℝ) * (X + 1) ^ 3 := le_mul_of_one_le_left (by positivity) hn' have hA : 0 ≤ ((n * r : ℕ) : ℝ) * (w + 1) * (((f * K : ℕ) : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50) + 1) := by positivity have hm : 0 ≤ min 1 (80 * ((f : ℝ) - 1) * 2⁻¹ ^ K) := le_min (by norm_num) (by have : (1 : ℝ) ≤ f := by exact_mod_cast hf have : (0 : ℝ) ≤ 2⁻¹ ^ K := by positivity nlinarith) have hC : 0 ≤ min 1 (80 * ((f : ℝ) - 1) * 2⁻¹ ^ K) * (n : ℝ) * (X + 1) * ((r : ℝ) * (w + 1) + X + 1) := by positivity nlinarith /-! ## RowU for the code rowCodeU q, in any table containing l12prog

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

theorem NLogN.KFX.rowU_of {q : ℕ} {Kc : ℝ} (H13 : L13U q Kc) (hKc : 0 < Kc) {Pp : ℕ}
    {tbl : Fin Pp → IStmt HS Pp} {g : Fin 1 → Fin Pp} (hprog : ∀ j, tbl (g j) = (l12prog j).ren id g)
    (Isym : List Sym) : RowU Isym tbl ((rowCodeU q).ren id g) (Kc + 8 * 10 ^ 12)

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.