Round-six lemma `ceil_bnd_le`

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem IntMul.Kappa.R6.IL2.ceil_bnd_le (hτ0 : 0 ≤ τ) (hτ1 : τ ≤ 1) {Kc : ℝ} (hKc : 0 < Kc) {K f n r Z : ℕ} (hK : 1 ≤ K) (hf : 1 ≤ f)
    (hfZ : f ≤ Z) (hKZ : 80 * Z * (Z + 2) ≤ 2 ^ K) (hn : 1 ≤ n)
    (hZ : zsz ((16 * (n * r) : ℕ) : ℤ) ≤ Z) (w : ℕ) :
    (⌈bnd τ Kc K f n r w⌉₊ : ℝ) ≤ (Kc * (K + 2) + 1) * n *
      ((r : ℝ) * (w + 1) * ((f : ℝ) + 1) ^ τ + (KFR.PsiR r Z w : ℝ))

Context. Round six, item language (I2): RowUC, uniform row additions for any m, τ and Lemma 12 table

RowUC m τ Isym tbl rowC Kc is the frozen KFW.RowU (KFWRowIface) with the label dimension mC = 100^3 replaced by m and τ50 = 1 - 2^-50 by τ: the single fixed code rowC implements the row addition Pm i j on the bits Fin m × Fin (m^k) laid out at posR m K e k, parameters [m^k, K, e, t, S0, B, r, H, i, j] in the background registers 36 … 45, at cost ≤ (Kc (K+2) + 1) · n · (r (H+1) (m^k + 1)^τ + PsiR r Z H).

RowUCP m τ tab: a fixed list of procedures and a code with RowUC in every extension IL.kTableP tab ext.

rowUC_of: 16 ≤ m ≤ 10^6 → 0 ≤ τ ≤ 1 → IL.L12Canon tab l12 τ → RowUCP m τ tab (code (rowCodeU l12).ren id (gL E), no extra procedures).

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