The integer bound `L₁ L₂ ≤ (ℓ + q + 7)(4q + 12)` (`log_nat`)

Proved

NLogN.KFV.P18M.log_nat

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

complexity-theoryinteger-multiplicationkappa-improvement

The integer bound L₁ L₂ ≤ (ℓ + q + 7)(4q + 12).

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

theorem NLogN.KFV.P18M.log_nat (P ℓ q : ℕ) (hP7 : 7 ≤ P) (hℓP : ℓ ≤ P) (hq1 : 2 ^ q ≤ P) (hq2 : P < 2 ^ (q + 1)) :
    (zsz ((2 * (kb P ℓ * 2 ^ ℓ + 2) + 1 : ℕ) : ℤ) + 2) *
      (zsz (((zsz ((2 * (kb P ℓ * 2 ^ ℓ + 2) + 1 : ℕ) : ℤ) + 2) ^ 4 : ℕ) : ℤ) + 1) ≤
      (ℓ + q + 7) * (4 * q + 12)

Context. KFM Log18a: the logarithmic factor of the Kronecker products (Log18Need)

With P = p = 6b and q = ⌊log₂ P⌋: kb < 2^{q+3}, so m + 1 < 2^{q+ℓ+5} and L₁ = zsz(m+1) + 2 ≤ ℓ + q + 7 ≤ 3P; then L₁⁴ < 2^{4q+11} and L₂ ≤ 4q + 12. Since q ≤ log₂ P and q ≤ ln P / ln 2 < 2 ln P, L₁ L₂ ≤ 84 (ℓ + log₂ P + 1)(ln P + 1). Main result: log18Need : KFV.Log18Need (c = 84, no extra threshold).

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
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_SApprox
import Definitions.Def_IntMul_HvdH_DiagApprox
import Definitions.Def_IntMul_HvdH_EApprox
import Definitions.Def_IntMul_HvdH_JApprox
import Definitions.Def_IntMul_HvdH_BApprox
import Definitions.Def_IntMul_HvdH_FPApprox
import Definitions.Def_IntMul_HvdH_MachineRef

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFV NLogN.KFV.P18M
set_option maxHeartbeats 1000000
open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFM

Formal statement

theorem NLogN.KFV.P18M.log_nat (P ℓ q : ℕ) (hP7 : 7 ≤ P) (hℓP : ℓ ≤ P) (hq1 : 2 ^ q ≤ P) (hq2 : P < 2 ^ (q + 1)) :
    (zsz ((2 * (kb P ℓ * 2 ^ ℓ + 2) + 1 : ℕ) : ℤ) + 2) *
      (zsz (((zsz ((2 * (kb P ℓ * 2 ^ ℓ + 2) + 1 : ℕ) : ℤ) + 2) ^ 4 : ℕ) : ℤ) + 1) ≤
      (ℓ + q + 7) * (4 * q + 12) := 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.KFV.P18M.log_nat`, Solutions/KFMLog18a.lean (lines 21–62) of the round-six development.

View graph