The block-length scan (round six, `scan_sp`)

Proved

J6Seg.PreT.scan_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

The block-length scan.

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

theorem J6Seg.PreT.scan_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {Cs : Fin HS}
    (hCs : Cs ∉ rg) (hCs5 : Cs.val < 56) (hcs : c Cs = []) {A sN tN lam st : ℕ} (hA : 2 ≤ A)
    (hv : VB v A) (h1 : v 1 = st) (h22 : v 22 = sN) (h23 : v 23 = tN) (h24 : v 24 = lam)
    (hl : 1 ≤ lam) (hlA : lam ≤ 2 ^ A) :
    Sp (scan Cs) (encK s (J6Seg.PreT.RF v c))
      (encK s (J6Seg.PreT.RF (Function.update (Function.update v 2 ((1 + J6Seg.enF sN tN lam st : ℕ) : ℤ)) 5 1) c))
      (cScan A lam)

Context. B-line IL, pre-tables (B5), part 10: the block-length scan

scan Cs: with the block start st on 1, sets 2 := 1 + enF s t λ st (the block length) and 5 := 1, by λ rounds (counter Cs) of if flag = 0 then (if g(st + n) > 0 then n++ else flag := 1), where g(j) = (j mod λ)·[b_j - b_{j-1} = t - s]·[j < s] is positive iff j is not a cut (gV_spec).

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_R6_Defs68

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PreT
open IntMul NLogN NLogN.KIL NLogN.RS IntMul.HvdH

Formal statement

theorem J6Seg.PreT.scan_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {Cs : Fin HS}
    (hCs : Cs ∉ rg) (hCs5 : Cs.val < 56) (hcs : c Cs = []) {A sN tN lam st : ℕ} (hA : 2 ≤ A)
    (hv : VB v A) (h1 : v 1 = st) (h22 : v 22 = sN) (h23 : v 23 = tN) (h24 : v 24 = lam)
    (hl : 1 ≤ lam) (hlA : lam ≤ 2 ^ A) :
    Sp (scan Cs) (encK s (J6Seg.PreT.RF v c))
      (encK s (J6Seg.PreT.RF (Function.update (Function.update v 2 ((1 + J6Seg.enF sN tN lam st : ℕ) : ℤ)) 5 1) c))
      (cScan A lam) := 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 `J6Seg.PreT.scan_sp`, Solutions/J6SegILPre10.lean (lines 183–310) of the round-six development.

View graph