The entries of the chunk tables (round six, `tabsT_tabQ2_bnd`)

Proved

J6Seg.PreT.tabsT_tabQ2_bnd

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

complexity-theoryinteger-multiplicationkappa-improvement

The entries of the chunk tables are below 2^(BW A + P + pk + b + 2).

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

theorem J6Seg.PreT.tabsT_tabQ2_bnd {P R sN tN lam aN A pk b : ℕ} (hl : 1 ≤ lam) (hA : 2 ≤ A)
    (hlA : lam ≤ 2 ^ A) (TB : J6Seg.PreT.TabB P R sN tN aN lam A) (hbA : b ≤ 2 ^ A) (nc : ℕ) :
    NLogN.Bnd (BW A + P + pk + b + 2) (tabsT (tabQ2 P R sN tN lam aN pk b) nc)

Context. B-line IL, pre-tables (B5′), part 29: size facts of the chunk-store output

For T = tabsT (tabQ2 P R s t λ α pk b) nc (the list chunkStore2_sp builds):

tabsT_tabQ2_length: |T| ≤ nc · (9 + 10 λ);
tabsT_tabQ2_bnd: NLogN.Bnd (BW A + P + pk + b + 2) T (under TabB … A, λ ≤ 2^A, 2 ≤ A).

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_R6_Defs68

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PreT
open IntMul NLogN NLogN.KIL J6Seg

Formal statement

theorem J6Seg.PreT.tabsT_tabQ2_bnd {P R sN tN lam aN A pk b : ℕ} (hl : 1 ≤ lam) (hA : 2 ≤ A)
    (hlA : lam ≤ 2 ^ A) (TB : J6Seg.PreT.TabB P R sN tN aN lam A) (hbA : b ≤ 2 ^ A) (nc : ℕ) :
    NLogN.Bnd (BW A + P + pk + b + 2) (tabsT (tabQ2 P R sN tN lam aN pk b) nc) := 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 `J6Seg.PreT.tabsT_tabQ2_bnd`, Solutions/J6SegILPre29.lean (lines 46–98) of the round-six development.

View graph