Round-six lemma `fsR_sp`

Proved

J6A.FS.fsR_sp

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

theorem J6A.FS.fsR_sp {X dF : Fin HS} (hXr : X ∉ rg) (hX5 : X.val < 56) (hXT : X ≠ sTmp)
    (hXC : X ≠ cRdC) (hXQ : ∀ i, Q dF i ≠ X)
    {ea ey : Ex HS} (hea : J6A.PA.OnRg ea) (hey : J6A.PA.OnRg ey) (hpa : Plain ea = true)
    (hpy : Plain ey = true) {fl : ℕ}
    (s : IState HS) (F : Fin HS → List ℤ) (hrg : ∀ j ∈ rg, F j = []) (h13 : F cL = [])
    (hQ : ∀ i, F (Q dF i) = [])
    {k pre post sr t p α d W : ℕ} (hc : F X = J6A.PA.dL k pre post sr t p α d)
    (hL : ∀ x ∈ J6A.PA.dL k pre post sr t p α d, |x| < 2 ^ W)
    (hp : 1 ≤ p) (hα : 1 ≤ α) (hmW : sWidth p α + 4 ≤ W) (hfl : fl ≤ 2 ^ W)
    (hta : Tame (2 ^ W) ea) (hty : Tame (2 ^ W) ey) {a y : ℤ}
    (hA : ∀ v c, J6A.PA.PV pre post sr t p α W v → ev v c ea = a)
    (hY : ∀ v c, J6A.PA.PV pre post sr t p α W v → ev v c ey = y) :
    Sp (fsR X ea ey fl dF) (encK s F) (encK s (fsG F dF ((p + 2 : ℕ) : ℤ) fl a y))
      (cFsR W p (sWidth p α) ea ey fl)

Context. A lines, IL side 13: the fine-descriptor set-ups

For a fine descriptor descFine w f a y with w = p + 2, f a literal and a, y expressions in the registers of parAX X:

fsR X ea ey fl Q: enter the register file, parAX X, push w, f, a, y on four temporaries Q 0 … Q 3 (outside rg, away from dF), leave the register file;
fsUp: then copy y, a, f, w onto dF and drop the temporaries; fsDn: drop four from dF.

fsUp_runs / fsDn_runs.

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 J6A J6A.FS
open IntMul NLogN NLogN.KIL NLogN.RS J6Seg.PJ IntMul.HvdH Function J6A.PA IntMul.Kappa.R6

Formal statement

theorem J6A.FS.fsR_sp {X dF : Fin HS} (hXr : X ∉ rg) (hX5 : X.val < 56) (hXT : X ≠ sTmp)
    (hXC : X ≠ cRdC) (hXQ : ∀ i, Q dF i ≠ X)
    {ea ey : Ex HS} (hea : J6A.PA.OnRg ea) (hey : J6A.PA.OnRg ey) (hpa : Plain ea = true)
    (hpy : Plain ey = true) {fl : ℕ}
    (s : IState HS) (F : Fin HS → List ℤ) (hrg : ∀ j ∈ rg, F j = []) (h13 : F cL = [])
    (hQ : ∀ i, F (Q dF i) = [])
    {k pre post sr t p α d W : ℕ} (hc : F X = J6A.PA.dL k pre post sr t p α d)
    (hL : ∀ x ∈ J6A.PA.dL k pre post sr t p α d, |x| < 2 ^ W)
    (hp : 1 ≤ p) (hα : 1 ≤ α) (hmW : sWidth p α + 4 ≤ W) (hfl : fl ≤ 2 ^ W)
    (hta : Tame (2 ^ W) ea) (hty : Tame (2 ^ W) ey) {a y : ℤ}
    (hA : ∀ v c, J6A.PA.PV pre post sr t p α W v → ev v c ea = a)
    (hY : ∀ v c, J6A.PA.PV pre post sr t p α W v → ev v c ey = y) :
    Sp (fsR X ea ey fl dF) (encK s F) (encK s (fsG F dF ((p + 2 : ℕ) : ℤ) fl a y))
      (cFsR W p (sWidth p α) ea ey fl) := 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.FS.fsR_sp`, Solutions/J6AIL13.lean (lines 98–152) of the round-six development.

View graph