Round-six lemma `accCU_fsp`

Proved

NLogN.KFD.accCU_fsp

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

complexity-theoryinteger-multiplicationkappa-improvement

acc ← acc ⊕ (stream w)ʳᵉᵛ (fine).

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

theorem NLogN.KFD.accCU_fsp {W v w : ℕ} {F : ℕ → List ℤ} (hU : Uni W v F) (hw : w < W)
    (s : IState HS) (f : Fin HS → List ℤ) (rest : List ℤ) (hf : f 0 = tabR 0 W F ++ rest)
    (hf21 : f 21 = []) (hR : RegS s f W v) (acc hr : List ℤ) (hf20 : f 20 = acc ++ hr)
    (hacc : acc.length = v) (hab : Bits acc) {Bb : ℕ} (hB : TabB W v Bb) (hv1 : 1 ≤ v) :
    FSp (accCU w) (encK s f)
      (encK s (Function.update f 20 (List.zipWith xr acc (F w).reverse ++ hr)))
      (cCF (W * v) Bb + 300 * cOF (W * v) Bb)

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

Formal statement

theorem NLogN.KFD.accCU_fsp {W v w : ℕ} {F : ℕ → List ℤ} (hU : Uni W v F) (hw : w < W)
    (s : IState HS) (f : Fin HS → List ℤ) (rest : List ℤ) (hf : f 0 = tabR 0 W F ++ rest)
    (hf21 : f 21 = []) (hR : RegS s f W v) (acc hr : List ℤ) (hf20 : f 20 = acc ++ hr)
    (hacc : acc.length = v) (hab : Bits acc) {Bb : ℕ} (hB : TabB W v Bb) (hv1 : 1 ≤ v) :
    FSp (accCU w) (encK s f)
      (encK s (Function.update f 20 (List.zipWith xr acc (F w).reverse ++ hr)))
      (cCF (W * v) Bb + 300 * cOF (W * v) Bb) := 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.accCU_fsp`, Solutions/KFDTab.lean (lines 115–162) of the round-six development.

View graph