Prove2Me

Push a reversed copy of stream `w` on stack `16` (fine) (`copyCU_fsp`)

Proved
NLogN.KFD.copyCU_fsp

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

complexity-theoryinteger-multiplicationkappa-improvement

Push a reversed copy of stream w on stack 16 (fine).

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

theorem NLogN.KFD.copyCU_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) {Bb : ℕ} (hB : TabB W v Bb) (hv1 : 1 ≤ v) :
    FSp (copyCU w) (encK s f) (encK s (Function.update f 16 ((F w).reverse ++ f 16)))
      (cCF (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.copyCU_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) {Bb : ℕ} (hB : TabB W v Bb) (hv1 : 1 ≤ v) :
    FSp (copyCU w) (encK s f) (encK s (Function.update f 16 ((F w).reverse ++ f 16)))
      (cCF (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.copyCU_fsp`, Solutions/KFDTab.lean (lines 34–113) of the round-six development.

View graph