The final distribution (round six, `distAll_sp`)

Proved

J6Seg.PJ.distAll_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

The final distribution.

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

theorem J6Seg.PJ.distAll_sp (s : IState HS) (oN : Fin 19 → Fin HS) (hinj : Injective oN)
    (hlt : ∀ i, (oN i).val < 56)
    (hx : ∀ i, oN i ≠ sX ∧ oN i ≠ sLn ∧ oN i ≠ sOut ∧ oN i ≠ sT2 ∧ oN i ≠ cLC)
    (f : Cs) (vs T : List ℤ) (hvs : vs.length = 9) (hfX : f sX = vs)
    (hfL : f sLn = [(T.length : ℤ)]) (hfO : f sOut = T) (h43 : f sT2 = []) (hfo : ∀ i, f (oN i) = [])
    (V : Fin 19 → List ℤ) (hVs : ∀ i : Fin 9, V (Fin.castLE (by omega) i) = [vs.getD i 0])
    (hV9 : V 9 = [(T.length : ℤ)]) (hV10 : V 10 = T) (hVr : ∀ i : Fin 19, 11 ≤ i.val → V i = [])
    (B : ℕ) (hvB : ∀ a ∈ vs, zsz a ≤ B) (hlB : zsz (T.length : ℤ) ≤ B) (hTB : Bnd B T) :
    Sp (distAll oN) (encK s f)
      (encK s (update (update (update (extend oN V f) sX []) sLn []) sOut [])) (cDistAll B T.length)

Context. B5 set-up, part 6: the final distribution (plain Sp)

From 45 = [ρ0 … ρ8], 42 = [|T|], 41 = T: put [ρi] on oN i (i < 9), [|T|] on oN 9 and T (in order, through 43) on oN 10; 41, 42, 45 end empty (distAll_sp).

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_Defs69

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function

Formal statement

theorem J6Seg.PJ.distAll_sp (s : IState HS) (oN : Fin 19 → Fin HS) (hinj : Injective oN)
    (hlt : ∀ i, (oN i).val < 56)
    (hx : ∀ i, oN i ≠ sX ∧ oN i ≠ sLn ∧ oN i ≠ sOut ∧ oN i ≠ sT2 ∧ oN i ≠ cLC)
    (f : Cs) (vs T : List ℤ) (hvs : vs.length = 9) (hfX : f sX = vs)
    (hfL : f sLn = [(T.length : ℤ)]) (hfO : f sOut = T) (h43 : f sT2 = []) (hfo : ∀ i, f (oN i) = [])
    (V : Fin 19 → List ℤ) (hVs : ∀ i : Fin 9, V (Fin.castLE (by omega) i) = [vs.getD i 0])
    (hV9 : V 9 = [(T.length : ℤ)]) (hV10 : V 10 = T) (hVr : ∀ i : Fin 19, 11 ≤ i.val → V i = [])
    (B : ℕ) (hvB : ∀ a ∈ vs, zsz a ≤ B) (hlB : zsz (T.length : ℤ) ≤ B) (hTB : Bnd B T) :
    Sp (distAll oN) (encK s f)
      (encK s (update (update (update (extend oN V f) sX []) sLn []) sOut [])) (cDistAll B T.length) := 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.PJ.distAll_sp`, Solutions/J6SegILPreJC6.lean (lines 53–157) of the round-six development.

View graph