Round-six lemma `gth_step`

Proved

J6A.ST.gth_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.gth_step (s0 : IState HS) (G : Fin HS → List ℤ) {iS iT iH iW iM iV : Fin HS}
    (fS : Free iS) (fT : Free iT) (fH : Free iH) (fW : Free iW) (fM : Free iM) (fV : Free iV)
    {s t H W M win A : ℕ} {LS LT LH LW LM LV : List ℤ}
    (hGS : G iS = (s : ℤ) :: LS) (hGT : G iT = (t : ℤ) :: LT) (hGH : G iH = (H : ℤ) :: LH)
    (hGW : G iW = (W : ℤ) :: LW) (hGM : G iM = (M : ℤ) :: LM) (hGV : G iV = (win : ℤ) :: LV)
    (hH : 1 ≤ H) (hWs : W ≤ s) (hwin : 0 < win) (hM : 0 < M) (ht : 0 < t)
    (hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A) (hHA : H ≤ 2 ^ A) (hWA : W ≤ 2 ^ A) (hMA : M ≤ 2 ^ A)
    (hVA : win ≤ 2 ^ A) (hA : 2 ≤ A) {n' j : ℕ} (hj : j < n') (hjA : j + 1 ≤ 2 ^ A) :
    Sp (gthB iS iT iH iW iM iV)
      (encK s0 (tbS G [(j : ℤ) + 1] (tlT (J6A.srcG s t H W M win) (fun _ => 0) n' (j + 1) ++ G 44)))
      (encK s0 (tbS G [(j : ℤ) + 1] (tlT (J6A.srcG s t H W M win) (fun _ => 0) n' j ++ G 44)))
      (303 * 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.gth_step (s0 : IState HS) (G : Fin HS → List ℤ) {iS iT iH iW iM iV : Fin HS}
    (fS : Free iS) (fT : Free iT) (fH : Free iH) (fW : Free iW) (fM : Free iM) (fV : Free iV)
    {s t H W M win A : ℕ} {LS LT LH LW LM LV : List ℤ}
    (hGS : G iS = (s : ℤ) :: LS) (hGT : G iT = (t : ℤ) :: LT) (hGH : G iH = (H : ℤ) :: LH)
    (hGW : G iW = (W : ℤ) :: LW) (hGM : G iM = (M : ℤ) :: LM) (hGV : G iV = (win : ℤ) :: LV)
    (hH : 1 ≤ H) (hWs : W ≤ s) (hwin : 0 < win) (hM : 0 < M) (ht : 0 < t)
    (hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A) (hHA : H ≤ 2 ^ A) (hWA : W ≤ 2 ^ A) (hMA : M ≤ 2 ^ A)
    (hVA : win ≤ 2 ^ A) (hA : 2 ≤ A) {n' j : ℕ} (hj : j < n') (hjA : j + 1 ≤ 2 ^ A) :
    Sp (gthB iS iT iH iW iM iV)
      (encK s0 (tbS G [(j : ℤ) + 1] (tlT (J6A.srcG s t H W M win) (fun _ => 0) n' (j + 1) ++ G 44)))
      (encK s0 (tbS G [(j : ℤ) + 1] (tlT (J6A.srcG s t H W M win) (fun _ => 0) n' j ++ G 44)))
      (303 * 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.gth_step`, Solutions/J6AIL14.lean (lines 193–255) of the round-six development.

View graph