Round-six lemma `cmp_step`

Proved

J6A.ST.cmp_step

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

theorem J6A.ST.cmp_step (s0 : IState HS) (G : Fin HS → List ℤ) {iH iV : Fin HS}
    (fH : Free iH) (fV : Free iV) {H win A : ℕ} {LH LV : List ℤ}
    (hGH : G iH = (H : ℤ) :: LH) (hGV : G iV = (win : ℤ) :: LV)
    (hH : 1 ≤ H) (hHA : H ≤ 2 ^ A) (hVA : win ≤ 2 ^ A) (hA : 2 ≤ A) {n' j : ℕ} (hj : j < n')
    (hjA : j + 1 ≤ 2 ^ A) :
    Sp (cmpB iH iV)
      (encK s0 (tbS G [(j : ℤ) + 1] (tlT (J6A.srcC H win) (fun _ => 0) n' (j + 1) ++ G 44)))
      (encK s0 (tbS G [(j : ℤ) + 1] (tlT (J6A.srcC H win) (fun _ => 0) n' j ++ G 44)))
      (203 * uC A 32)

Context. A lines, IL side 14: the source tables of the gather and compress slab passes

The code code (srcG s t H W M win j) / code (srcC H win j) as one expression gE / cE' in the loop index j = (43) - 1 and registers holding s, t, H, W, M, win (gE_eval, gE_ok), and the producers gthA_sp / cmpA_sp: rep 43 n' of push 44 0; push 44 code builds srcTab src (fun _ => 0) n' on 44 (B1's tab_loop).

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 J6A J6A.ST
open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg.PreT J6Seg J6Seg.Src
open J6Seg.Slab (srcTab code)

Formal statement

theorem J6A.ST.cmp_step (s0 : IState HS) (G : Fin HS → List ℤ) {iH iV : Fin HS}
    (fH : Free iH) (fV : Free iV) {H win A : ℕ} {LH LV : List ℤ}
    (hGH : G iH = (H : ℤ) :: LH) (hGV : G iV = (win : ℤ) :: LV)
    (hH : 1 ≤ H) (hHA : H ≤ 2 ^ A) (hVA : win ≤ 2 ^ A) (hA : 2 ≤ A) {n' j : ℕ} (hj : j < n')
    (hjA : j + 1 ≤ 2 ^ A) :
    Sp (cmpB iH iV)
      (encK s0 (tbS G [(j : ℤ) + 1] (tlT (J6A.srcC H win) (fun _ => 0) n' (j + 1) ++ G 44)))
      (encK s0 (tbS G [(j : ℤ) + 1] (tlT (J6A.srcC H win) (fun _ => 0) n' j ++ G 44)))
      (203 * uC A 32) := 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 `J6A.ST.cmp_step`, Solutions/J6AIL14.lean (lines 286–345) of the round-six development.

View graph