Round-six lemma `applyCF_runs`

Proved

NLogN.KFD.applyCF_runs

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

theorem NLogN.KFD.applyCF_runs {G0 : Fin HS → List Item} {W v w : ℕ} {F : ℕ → List ℤ} (hU : Uni W v F)
    (hw : w < W) {code : IStmt HS Pp} {ys' : List ℤ} {c : ℕ}
    (hc : ∀ (t : IState HS) (R : List Item), Inv G0 t → IRuns I iprog code
      (t.upd 0 (ints (F w) ++ R)) (t.upd 0 (ints ys' ++ R)) c)
    (s : IState HS) (hs : Inv G0 s) (f : Fin HS → List ℤ) (hfp : ∀ r, Prot r → f r = [])
    (hR : RegS s f W v) (rest : List ℤ) (hf : f 0 = tabR 0 W F ++ rest)
    (Bb : ℕ) (hV : zsz ((W * v : ℕ) : ℤ) ≤ Bb) (hv1 : 1 ≤ v) :
    IRuns I iprog (applyCF w code) (encK s f)
      (encK s (Function.update f 0 (tabR 0 W (Function.update F w ys') ++ rest)))
      (c + 2 * cOF (W * v) Bb + cPushT Bb + (2 * Bb + 2))

Context. KFD: fine stream-table operations

The register programs copyCU, accCU, accLU, buildCU, buildsCU, rebuildCU of KIL5Tab are unchanged; here they get fine specifications (FSp, i.e. compiled by fcode, unary loop counters). The cost unit is cCF V Bb = O(V) + O((Bb + 2)^2): linear in the table volume V = W · v, plus one multiplication (w · v) per operation. applyCF is the fine applyCU.

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.KFD
open IntMul NLogN.RS
open NLogN.KIL
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

Formal statement

theorem NLogN.KFD.applyCF_runs {G0 : Fin HS → List Item} {W v w : ℕ} {F : ℕ → List ℤ} (hU : Uni W v F)
    (hw : w < W) {code : IStmt HS Pp} {ys' : List ℤ} {c : ℕ}
    (hc : ∀ (t : IState HS) (R : List Item), Inv G0 t → IRuns I iprog code
      (t.upd 0 (ints (F w) ++ R)) (t.upd 0 (ints ys' ++ R)) c)
    (s : IState HS) (hs : Inv G0 s) (f : Fin HS → List ℤ) (hfp : ∀ r, Prot r → f r = [])
    (hR : RegS s f W v) (rest : List ℤ) (hf : f 0 = tabR 0 W F ++ rest)
    (Bb : ℕ) (hV : zsz ((W * v : ℕ) : ℤ) ≤ Bb) (hv1 : 1 ≤ v) :
    IRuns I iprog (applyCF w code) (encK s f)
      (encK s (Function.update f 0 (tabR 0 W (Function.update F w ys') ++ rest)))
      (c + 2 * cOF (W * v) Bb + cPushT Bb + (2 * Bb + 2)) := 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.KFD.applyCF_runs`, Solutions/KFDTab.lean (lines 321–399) of the round-six development.

View graph