Round-six lemma `stG_spX`

Proved

J6Seg.PreT.stG_spX

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

theorem J6Seg.PreT.stG_spX (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {O : Fin HS}
    (hO : O ∉ rg) (hO5 : O.val < 56) (hOC : O ≠ Cu) (hc : c Cu = []) {P R sN tN lam aN A : ℕ}
    (hi : StIn2 v P R sN tN lam aN A) (hPA : P ≤ A)
    {eF : Ex HS} (hiF : InRg eF) (hpF : Poly eF = true) (hdF : J6Seg.PreT.dg eF ≤ 40)
    (hoF : ∀ (u : Fin HS → ℤ) (cu : Fin HS → List ℤ), eF.ok (encK s (J6Seg.PreT.RF u cu))) (F : ℕ → ℤ)
    (hF : ∀ k (u : Fin HS → ℤ) (cu : Fin HS → List ℤ), u 4 = gamI P sN tN aN k → u 9 = 2 ^ P →
      eF.eval (encK s (J6Seg.PreT.RF u cu)) = F k)
    (bq : ∀ k < lam, |expNeg P sN (2 * aN ^ 2 * tN * (k + 1))| ≤ 2 ^ A)
    (bF : ∀ k < lam, |F k| ≤ 2 ^ A) (bG : ∀ k < lam, |gamI P sN tN aN (k + 1)| ≤ 2 ^ A) :
    (∀ j, j ≠ 4 → j ≠ 5 → j ≠ 11 → j ≠ 12 → stGV v P sN tN aN F lam j = v j) ∧
    VB (stGV v P sN tN aN F lam) A ∧
    Sp (stG O eF) (encK s (J6Seg.PreT.RF v c)) (encK s (J6Seg.PreT.RF (stGV v P sN tN aN F lam)
      (Function.update c O (rv F lam ++ c O)))) (cStG A lam eF)

Context. B5 J side, part K12: the line tables as Rn steps

stG_spX: stG_sp (J6SegILPre8) with the final registers explicit (stGV); the table stage tabP = stDI SDI; stDD SDD; stGam SGM; stGi SGI (Rn.tabP).

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_Defs71

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PreT
open IntMul NLogN NLogN.KIL NLogN.RS IntMul.HvdH

Formal statement

theorem J6Seg.PreT.stG_spX (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {O : Fin HS}
    (hO : O ∉ rg) (hO5 : O.val < 56) (hOC : O ≠ Cu) (hc : c Cu = []) {P R sN tN lam aN A : ℕ}
    (hi : StIn2 v P R sN tN lam aN A) (hPA : P ≤ A)
    {eF : Ex HS} (hiF : InRg eF) (hpF : Poly eF = true) (hdF : J6Seg.PreT.dg eF ≤ 40)
    (hoF : ∀ (u : Fin HS → ℤ) (cu : Fin HS → List ℤ), eF.ok (encK s (J6Seg.PreT.RF u cu))) (F : ℕ → ℤ)
    (hF : ∀ k (u : Fin HS → ℤ) (cu : Fin HS → List ℤ), u 4 = gamI P sN tN aN k → u 9 = 2 ^ P →
      eF.eval (encK s (J6Seg.PreT.RF u cu)) = F k)
    (bq : ∀ k < lam, |expNeg P sN (2 * aN ^ 2 * tN * (k + 1))| ≤ 2 ^ A)
    (bF : ∀ k < lam, |F k| ≤ 2 ^ A) (bG : ∀ k < lam, |gamI P sN tN aN (k + 1)| ≤ 2 ^ A) :
    (∀ j, j ≠ 4 → j ≠ 5 → j ≠ 11 → j ≠ 12 → stGV v P sN tN aN F lam j = v j) ∧
    VB (stGV v P sN tN aN F lam) A ∧
    Sp (stG O eF) (encK s (J6Seg.PreT.RF v c)) (encK s (J6Seg.PreT.RF (stGV v P sN tN aN F lam)
      (Function.update c O (rv F lam ++ c O)))) (cStG A lam eF) := 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.PreT.stG_spX`, Solutions/J6SegILPreJK12.lean (lines 23–82) of the round-six development.

View graph