Pass 7 producer (round six, `outP_sp`)

Proved

J6Seg.Src.outP_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

Pass 7 producer, on any state with 55 empty.

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

theorem J6Seg.Src.outP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {iP iS iT iA iN : Fin HS} (fP : Free7 iP)
    (fS : Free7 iS) (fT : Free7 iT) (fA : Free7 iA) (fN : Free iN) (h55 : F 55 = [])
    {p s t α n' A : ℕ} {LP LS LT LA LN : List ℤ}
    (hGP : F iP = (p : ℤ) :: LP) (hGS : F iS = (s : ℤ) :: LS) (hGT : F iT = (t : ℤ) :: LT)
    (hGA : F iA = (α : ℤ) :: LA) (hGN : F iN = (n' : ℤ) :: LN) (hs : 0 < s) (ha : 1 ≤ α)
    (hpA : p ≤ 2 ^ A) (hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A) (haA : α ≤ 2 ^ A) (hnA : n' ≤ 2 ^ A)
    (hA : 2 ≤ A) (hdA : ∀ l < s, |dTilde p s t α l| ≤ 2 ^ A) :
    Sp (outP iP iS iT iA iN) (encK s0 F)
      (encK s0 (update F 44 (srcTab (fun l => some l) (argO p s t α) n' ++ F 44)))
      ((n' + 1) * (c7 A p α + 4 * uC A DD + uC A DD))

Context. B-line IL, source-table producers, part 8: pass 7 (argO, the d̃_l values)

outP iP iS iT iA iN: src = some, argOf = argO p s t α (d̃_l = dTilde p s t α l for l < s, else 0), n' on iN; each entry with l < s calls the library program expPosP (callB, which uses 16, 17, 18, 19, 27 and restores them) with inputs p, s², α² · kOf s t l (the rounding residue b = t l - s · rowSel l is first pushed on 13), and 2α² - 2.

Inputs: p on iP, s on iS, t on iT, α on iA, n' on iN, all Free7 (Free and not 16, 17, 18, 19, 27); 0 < s, 1 ≤ α, all ≤ 2^A, 2 ≤ A, and |d̃_l| ≤ 2^A for l < s. Output: 44 := srcTab some (argO p s t α) n' ++ F 44. Theorem outP_sp, cost (n' + 1) * (c7 A p α + 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 IntMul.HvdH
open J6Seg.Slab (srcTab argO)

Formal statement

theorem J6Seg.Src.outP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {iP iS iT iA iN : Fin HS} (fP : Free7 iP)
    (fS : Free7 iS) (fT : Free7 iT) (fA : Free7 iA) (fN : Free iN) (h55 : F 55 = [])
    {p s t α n' A : ℕ} {LP LS LT LA LN : List ℤ}
    (hGP : F iP = (p : ℤ) :: LP) (hGS : F iS = (s : ℤ) :: LS) (hGT : F iT = (t : ℤ) :: LT)
    (hGA : F iA = (α : ℤ) :: LA) (hGN : F iN = (n' : ℤ) :: LN) (hs : 0 < s) (ha : 1 ≤ α)
    (hpA : p ≤ 2 ^ A) (hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A) (haA : α ≤ 2 ^ A) (hnA : n' ≤ 2 ^ A)
    (hA : 2 ≤ A) (hdA : ∀ l < s, |dTilde p s t α l| ≤ 2 ^ A) :
    Sp (outP iP iS iT iA iN) (encK s0 F)
      (encK s0 (update F 44 (srcTab (fun l => some l) (argO p s t α) n' ++ F 44)))
      ((n' + 1) * (c7 A p α + 4 * uC A DD + 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.outP_sp`, Solutions/J6SegILSrc8.lean (lines 285–331) of the round-six development.

View graph