The Lemma 13 cost in the `RowHyp` form (round six, `ceil_bnd_le`)

Proved

NLogN.KFR.ceil_bnd_le

by xuanji · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

The Lemma 13 cost in the RowHyp form.

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

theorem NLogN.KFR.ceil_bnd_le {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) ^ τ50 + (PsiR r Z w : ℝ))

Context. KFR: the bridge Lem13ILP iprog → RowHyp … τ50

PsiR r Z w = 2 (Z + zsz (w+1) + 2)^3 + ⌊r (w+1) zsz (w+1) / (Z+2)⌋ + 2 (monotone, ≥ Z+2).
ceil_bnd_le: when 80 Z (Z+2) ≤ 2^K and f ≤ Z, the Lemma 13 cost ⌈bnd⌉ is at most (Kc (K+2) + 1) · n · (r (w+1) (f+1)^τ50 + PsiR r Z w). The guard term min 1 (80 (f-1) 2^{-K}) is at most 1/(Z+2), which absorbs the zsz factors of the correction cost into O(r (w+1)) plus r (w+1) zsz(w+1)/(Z+2) (inside PsiR).
rowHyp_of_lem13: Lem13ILP iprog → ∃ Kc > 0, ∀ K m r Z, 6 ≤ K → 3 ≤ m → 1 ≤ r → 80 Z (Z+2) ≤ 2^K → RowHyp Isym iprog K m r Z (PsiR r Z) (Kc (K+2) + 1) τ50.

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

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFR
open IntMul NLogN.RS AModel NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH Complex P8Lift Butterfly NLogN.KFN

Formal statement

theorem NLogN.KFR.ceil_bnd_le {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) ^ τ50 + (PsiR r Z w : ℝ)) := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `NLogN.KFR.ceil_bnd_le`, Solutions/KFRBridge.lean (lines 51–186) of the round-six development.

View graph