Growth (round six, `blkOK_of`)

Proved

J6Seg.KR.blkOK_of

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

complexity-theoryinteger-multiplicationkappa-improvement

Growth: all stage values of a block bounded.

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

theorem J6Seg.KR.blkOK_of (P : ℕ) {Kt X : ℤ} {lam n pk : ℕ} {di gi gam dd am ap : List ℤ} {z : List GI}
    (hKt : 0 ≤ Kt) (hX : 0 ≤ X) (hz : AB X z) (hzn : z.length = n) (hnl : n ≤ lam)
    (tdi : TB (2 ^ P * Kt) di) (tgi : TB (2 ^ P * Kt) gi) (tga : TB (2 ^ P * Kt) gam)
    (tdd : TB (2 ^ P * Kt) dd) (tam : TB (2 ^ P * Kt) am) (tap : TB (2 ^ P * Kt) ap)
    (hdi : n ≤ di.length) (hgi : n ≤ gi.length) (hga : n ≤ gam.length) (hdd : n ≤ dd.length)
    (ham : n ≤ am.length) (hap : n ≤ ap.length)
    (hpk : Xs ((lam + 1) * Kt + 1) X 7 ≤ 2 ^ pk) :
    blkOK P (2 ^ pk) (2 * n) di gi gam dd am ap z

Context. B3 (chunk kernel), part 6: the chunk on pairs with per-block records, and growth bounds

chunkB, chunkG2: the chunk kernel on pairs, each block of length n with its own record length r = 2n; liftG_chunkL2: liftG (chunkL …) = chunkG2 ….
growth: if the row entries are bounded by X and the tables by 2^P·Kt, every stage value of a block of length n ≤ λ is bounded by Xs ((λ+1)·Kt+1) X 7, where Xs K X i iterates X ↦ K·X+1.

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_Defs64

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.KR
open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFV

Formal statement

theorem J6Seg.KR.blkOK_of (P : ℕ) {Kt X : ℤ} {lam n pk : ℕ} {di gi gam dd am ap : List ℤ} {z : List GI}
    (hKt : 0 ≤ Kt) (hX : 0 ≤ X) (hz : AB X z) (hzn : z.length = n) (hnl : n ≤ lam)
    (tdi : TB (2 ^ P * Kt) di) (tgi : TB (2 ^ P * Kt) gi) (tga : TB (2 ^ P * Kt) gam)
    (tdd : TB (2 ^ P * Kt) dd) (tam : TB (2 ^ P * Kt) am) (tap : TB (2 ^ P * Kt) ap)
    (hdi : n ≤ di.length) (hgi : n ≤ gi.length) (hga : n ≤ gam.length) (hdd : n ≤ dd.length)
    (ham : n ≤ am.length) (hap : n ≤ ap.length)
    (hpk : Xs ((lam + 1) * Kt + 1) X 7 ≤ 2 ^ pk) :
    blkOK P (2 ^ pk) (2 * n) di gi gam dd am ap z := 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.KR.blkOK_of`, Solutions/J6SegKr6.lean (lines 163–220) of the round-six development.

View graph