The branch on `κ m ≠ m`, as an explicit state (`brB_fsp`)

Proved

NLogN.KFL.brB_fsp

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

complexity-theoryinteger-multiplicationkappa-improvement

The branch on κ m ≠ m, as an explicit state.

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

theorem NLogN.KFL.brB_fsp {B Bb : ℕ} (hB1 : 1 ≤ Bb) (s : IState HS) (G : Fin HS → List ℤ) (L l : List ℤ)
    (h0 : G 0 = L ++ l) (hL : L.length = B) (hLb : NLogN.Bnd 1 L) (zB : zsz (B : ℤ) ≤ Bb)
    {k kv nb : ℕ} {lk lm ln : List ℤ} (hK : G rK = (kv : ℤ) :: lk) (zk : zsz (kv : ℤ) ≤ Bb)
    (hm : G rm = (k : ℤ) :: lm) (zm : zsz (k : ℤ) ≤ Bb)
    (hN : G rNB = (nb : ℤ) :: ln) (zn : zsz (nb : ℤ) ≤ Bb) (zn1 : zsz ((nb : ℤ) + 1) ≤ Bb)
    (zd : zsz ((kv : ℤ) - k) ≤ Bb) :
    FSp (NLogN.KFL.brB B) (encK s G) (encK s (Function.update (Function.update (Function.update
      (Function.update (Function.update (Function.update G 0 l)
      NLogN.KFL.sT ((if decide (kv ≠ k) then [] else L.reverse) ++ G NLogN.KFL.sT))
      sKB ((if decide (kv ≠ k) then L.reverse else []) ++ G sKB))
      sKK ((if decide (kv ≠ k) then [(kv : ℤ)] else []) ++ G sKK))
      sFL ((if kv ≠ k then 1 else 0) :: G sFL))
      rNB (((nb + if kv ≠ k then 1 else 0 : ℕ) : ℤ) :: ln))) (2 * NLogN.KFL.cIte Bb + NLogN.KFL.cBr B Bb)

Context. KFL §12: the correction, pass 1 (extraction of the moved records)

The bit array flR recs M (record m = recs m, B bits) is on stack 0, record 0 on top. For m = 0, …, M-1 the pass computes the key κ m = keyR m (keyProg), and moves the record

to sKB (and pushes κ m on sKK) if κ m ≠ m (a moved record),
to sT otherwise, and pushes the flag [κ m ≠ m] on sFL; rNB counts the moved records. p1_fsp: the whole pass, as the list state P1 … M.

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.KFL
open IntMul NLogN.RS NLogN.KIL NLogN.KFD Butterfly

Formal statement

theorem NLogN.KFL.brB_fsp {B Bb : ℕ} (hB1 : 1 ≤ Bb) (s : IState HS) (G : Fin HS → List ℤ) (L l : List ℤ)
    (h0 : G 0 = L ++ l) (hL : L.length = B) (hLb : NLogN.Bnd 1 L) (zB : zsz (B : ℤ) ≤ Bb)
    {k kv nb : ℕ} {lk lm ln : List ℤ} (hK : G rK = (kv : ℤ) :: lk) (zk : zsz (kv : ℤ) ≤ Bb)
    (hm : G rm = (k : ℤ) :: lm) (zm : zsz (k : ℤ) ≤ Bb)
    (hN : G rNB = (nb : ℤ) :: ln) (zn : zsz (nb : ℤ) ≤ Bb) (zn1 : zsz ((nb : ℤ) + 1) ≤ Bb)
    (zd : zsz ((kv : ℤ) - k) ≤ Bb) :
    FSp (NLogN.KFL.brB B) (encK s G) (encK s (Function.update (Function.update (Function.update
      (Function.update (Function.update (Function.update G 0 l)
      NLogN.KFL.sT ((if decide (kv ≠ k) then [] else L.reverse) ++ G NLogN.KFL.sT))
      sKB ((if decide (kv ≠ k) then L.reverse else []) ++ G sKB))
      sKK ((if decide (kv ≠ k) then [(kv : ℤ)] else []) ++ G sKK))
      sFL ((if kv ≠ k then 1 else 0) :: G sFL))
      rNB (((nb + if kv ≠ k then 1 else 0 : ℕ) : ℤ) :: ln))) (2 * NLogN.KFL.cIte Bb + NLogN.KFL.cBr B 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.KFL.brB_fsp`, Solutions/KFLCorr1.lean (lines 203–290) of the round-six development.

View graph