Round-six lemma `sp_cand`

Proved

IntMul.Kappa.R6.sp_cand

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.R6SLoop):

theorem IntMul.Kappa.R6.sp_cand (s : IState HS) (f : Fin HS → List ℤ) (A P w Aa Bb cm : ℕ)
    (l41 l36 l40 l42 : List ℤ) (h49 : f 49 = []) (h50 : f 50 = [])
    (h41 : f 41 = (A : ℤ) :: l41) (h36 : f 36 = (P : ℤ) :: l36) (h40 : f 40 = (w : ℤ) :: l40)
    (h42 : f 42 = 0 :: l42) (hA2 : 2 ≤ A) (hcm : A + w ≤ cm) (hAa : 2 ≤ Aa)
    (hcA : cm * cm ≤ Aa) (hPA : 2 * P ≤ Aa) (hB : Aa ^ 6 < 2 ^ Bb) :
    Sp candR (encK s f) (encK s (update f 42 ((pick A (2 * P) w : ℕ) :: l42)))
      ((w * (22 * cm + 30) + 1) * kU Bb)

Context. Round-six setup, part 3: the candidate loop

Registers (all fixed): 36 the product P, 40 the window width w, 41 the left end A, 42 the selected candidate, 44 the candidate c, 45 the residue 2P mod c, 46 the sum, counters 49 (candidates) and 50 (sum).

sumT_eq: the inverse sum is muInv Q c if Q is coprime to c, else 0.
sp_cand (candR): the loop over c = A + w, …, A + 1 leaves pick A (2P) w on 42.

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 IntMul IntMul.Kappa IntMul.Kappa.R6
open IntMul NLogN NLogN.KIL NLogN.KFM NLogN.RS Finset Function

Formal statement

theorem IntMul.Kappa.R6.sp_cand (s : IState HS) (f : Fin HS → List ℤ) (A P w Aa Bb cm : ℕ)
    (l41 l36 l40 l42 : List ℤ) (h49 : f 49 = []) (h50 : f 50 = [])
    (h41 : f 41 = (A : ℤ) :: l41) (h36 : f 36 = (P : ℤ) :: l36) (h40 : f 40 = (w : ℤ) :: l40)
    (h42 : f 42 = 0 :: l42) (hA2 : 2 ≤ A) (hcm : A + w ≤ cm) (hAa : 2 ≤ Aa)
    (hcA : cm * cm ≤ Aa) (hPA : 2 * P ≤ Aa) (hB : Aa ^ 6 < 2 ^ Bb) :
    Sp candR (encK s f) (encK s (update f 42 ((pick A (2 * P) w : ℕ) :: l42)))
      ((w * (22 * cm + 30) + 1) * kU Bb) := 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 `IntMul.Kappa.R6.sp_cand`, Solutions/R6SLoop.lean (lines 93–229) of the round-six development.

View graph