Round-six lemma `stgL_sp`

Proved

NLogN.KFUU.stgL_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

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.KFUURot3):

theorem NLogN.KFUU.stgL_sp (Q Bb : ℕ) (hQ1 : 1 ≤ Q) (rv : List (ℕ × ℕ)) (hrv : ∀ p ∈ rv, 1 ≤ p.1 ∧ p.2 < Q)
    (hBb : zsz ((2 * (Q * vol (rv.map Prod.fst)) : ℕ) : ℤ) ≤ Bb) (B : ℕ)
    (hiB : zsz (rv.length : ℤ) ≤ B)
    (s : IState HS) (g : Fin HS → List ℤ) (hgI : g oI = []) (hgC : g oCS = [])
    (hgN : g sNQ = [-(Q : ℤ)]) {LI : List Item} (hI : s.G oI = .int rv.length :: LI) :
    Sp (.rep oCS (.reg oI) stageU) (encK s (stF g rv Q 0)) (encK s (stF g rv Q rv.length))
      (2 * 2000 * (B + 2) + rv.length * (10 ^ 8 * (vol (rv.map Prod.fst) + 1) * (Bb + 2) +
        8000 * (B + 2) + 30) + 32)

Context. KFUU §7c: the loops of the uniform table set-up

coefL_sp: i steps of coefB (counter oCC, count oI = i);
stgL_sp: i uniform stages stageU of KIL4 (counter oCS), which turn the stage stacks of ac into the offset table tbl Q ac on stack 14.

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_Twiddle
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_MachineRef

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFUU
open IntMul NLogN.KIL AModel

Formal statement

theorem NLogN.KFUU.stgL_sp (Q Bb : ℕ) (hQ1 : 1 ≤ Q) (rv : List (ℕ × ℕ)) (hrv : ∀ p ∈ rv, 1 ≤ p.1 ∧ p.2 < Q)
    (hBb : zsz ((2 * (Q * vol (rv.map Prod.fst)) : ℕ) : ℤ) ≤ Bb) (B : ℕ)
    (hiB : zsz (rv.length : ℤ) ≤ B)
    (s : IState HS) (g : Fin HS → List ℤ) (hgI : g oI = []) (hgC : g oCS = [])
    (hgN : g sNQ = [-(Q : ℤ)]) {LI : List Item} (hI : s.G oI = .int rv.length :: LI) :
    Sp (.rep oCS (.reg oI) stageU) (encK s (stF g rv Q 0)) (encK s (stF g rv Q rv.length))
      (2 * 2000 * (B + 2) + rv.length * (10 ^ 8 * (vol (rv.map Prod.fst) + 1) * (Bb + 2) +
        8000 * (B + 2) + 30) + 32) := 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.KFUU.stgL_sp`, Solutions/KFUURot3.lean (lines 76–175) of the round-six development.

View graph