Pass 3 producer (round six, `gthP_sp`)

Proved

J6Seg.Src.gthP_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

Pass 3 producer.

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

theorem J6Seg.Src.gthP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {iN : Fin HS} (fN : Free iN)
    (L : List ℕ) {n' A : ℕ} {L30 L31 LN : List ℤ}
    (h30 : F 30 = zLs L ++ L30) (h31 : F 31 = (L.length : ℤ) :: L31)
    (hGN : F iN = (n' : ℤ) :: LN) (hLn : L.length ≤ n') (hLA : ∀ x ∈ L, x ≤ 2 ^ A)
    (hnA : n' ≤ 2 ^ A) (hA : 2 ≤ A) :
    Sp (gthP iN) (encK s0 F) (encK s0 (update F 44 (srcTab (gSrc L) (fun _ => 0) n' ++ F 44)))
      ((L.length + n' + 2) * (40 * uC A DD))

Context. B-line IL, source-table producers, part 9: pass 3 (jSrc, the gather)

gthP iN: with a list L (= LJ) on 30 (head = index 0) and |L| on 31 (as left by ljP), and n' (= G ≥ |L|) on iN (Free): move L reversed onto 15 (mvK 30 15 43 (reg 31)), then for j = n' - 1, …, 0 push 0 and code (src j) on 44, with src j = if j < |L| then some L[j] else none (jSrc for L = LJ), moving L[j] back from 15 to 30. Output: 44 := srcTab src (fun _ => 0) n' ++ F 44, everything else (in particular 15, 30, 31) unchanged. Theorem gthP_sp, cost (|L| + n' + 2) * (40 * uC A DD).

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_Defs65

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.Src
set_option maxRecDepth 20000
open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg.PreT J6Seg
open J6Seg.Slab (srcTab)

Formal statement

theorem J6Seg.Src.gthP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {iN : Fin HS} (fN : Free iN)
    (L : List ℕ) {n' A : ℕ} {L30 L31 LN : List ℤ}
    (h30 : F 30 = zLs L ++ L30) (h31 : F 31 = (L.length : ℤ) :: L31)
    (hGN : F iN = (n' : ℤ) :: LN) (hLn : L.length ≤ n') (hLA : ∀ x ∈ L, x ≤ 2 ^ A)
    (hnA : n' ≤ 2 ^ A) (hA : 2 ≤ A) :
    Sp (gthP iN) (encK s0 F) (encK s0 (update F 44 (srcTab (gSrc L) (fun _ => 0) n' ++ F 44)))
      ((L.length + n' + 2) * (40 * uC A DD)) := 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.Src.gthP_sp`, Solutions/J6SegILSrc9.lean (lines 203–246) of the round-six development.

View graph