Round-six lemma `sp_rdP`

Proved

J6Seg.KR.sp_rdP

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6Seg.KR.sp_rdP {V O C R : Fin HS} (hVO : V ≠ O) (hVC : V ≠ C) (hOC : O ≠ C) (hRC : R ≠ C)
    (hRV : R ≠ V) (hRO : R ≠ O) (hPV : J6Seg.KR.rP ≠ V) (hPO : J6Seg.KR.rP ≠ O) (hPC : J6Seg.KR.rP ≠ C) (hQV : rP1 ≠ V)
    (hQO : rP1 ≠ O) (hQC : rP1 ≠ C)
    (hV5 : V.val < 56) (hO5 : O.val < 56) (hC5 : C.val < 56) (hR5 : R.val < 56)
    (s : IState HS) (f : Fin HS → List ℤ) (P : ℕ) (u : List GI) (lv lr l1 l2 : List ℤ)
    (hV : f V = gsw u ++ lv) (hC : f C = []) (hR : f R = (u.length : ℤ) :: lr)
    (hP : f J6Seg.KR.rP = 2 ^ P :: l1) (hP1 : f rP1 = 2 ^ (P + 1) :: l2) (B : ℕ)
    (hu : ∀ z ∈ u, zsz z.1 + 2 ≤ B ∧ zsz z.2 + 2 ≤ B) (hPB : P + 3 ≤ B)
    (hn : zsz (u.length : ℤ) ≤ B) :
    Sp (rdP V O C R) (encK s f)
      (encK s (Function.update (Function.update f V lv) O
        (gflat (u.reverse.map (rsG P)) ++ f O))) ((u.length + 1) * 200000 * (B + 2))

Context. B3 (chunk kernel), part 2: register loops on managed states

Counted register loops (RS.rep with the count on top of a register) on encK states:

mvP X Y T C R: move n Gaussian pairs from X to Y, keeping each pair's orientation (gflat z ++ lx on X ↦ gflat z.reverse on top of Y);
rdP V O C R: round pairs (rs P on both parts) from a reversed flat list on V to O (gsw u ++ lv ↦ gflat ((u.reverse).map rsG) on top of O);
rgP A Y C R: a real table as Gaussian pairs (a ++ la on A ↦ gflat (a.reverse.map (·, 0)) on top of Y);
zeroR, dropR, dupR: push zeros, drop, duplicate-move with a register count.

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_Defs64

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.KR
open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB

Formal statement

theorem J6Seg.KR.sp_rdP {V O C R : Fin HS} (hVO : V ≠ O) (hVC : V ≠ C) (hOC : O ≠ C) (hRC : R ≠ C)
    (hRV : R ≠ V) (hRO : R ≠ O) (hPV : J6Seg.KR.rP ≠ V) (hPO : J6Seg.KR.rP ≠ O) (hPC : J6Seg.KR.rP ≠ C) (hQV : rP1 ≠ V)
    (hQO : rP1 ≠ O) (hQC : rP1 ≠ C)
    (hV5 : V.val < 56) (hO5 : O.val < 56) (hC5 : C.val < 56) (hR5 : R.val < 56)
    (s : IState HS) (f : Fin HS → List ℤ) (P : ℕ) (u : List GI) (lv lr l1 l2 : List ℤ)
    (hV : f V = gsw u ++ lv) (hC : f C = []) (hR : f R = (u.length : ℤ) :: lr)
    (hP : f J6Seg.KR.rP = 2 ^ P :: l1) (hP1 : f rP1 = 2 ^ (P + 1) :: l2) (B : ℕ)
    (hu : ∀ z ∈ u, zsz z.1 + 2 ≤ B ∧ zsz z.2 + 2 ≤ B) (hPB : P + 3 ≤ B)
    (hn : zsz (u.length : ℤ) ≤ B) :
    Sp (rdP V O C R) (encK s f)
      (encK s (Function.update (Function.update f V lv) O
        (gflat (u.reverse.map (rsG P)) ++ f O))) ((u.length + 1) * 200000 * (B + 2)) := 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.KR.sp_rdP`, Solutions/J6SegKr2.lean (lines 444–525) of the round-six development.

View graph