The eleven updates (round six, `keyMid_fsp`)

Proved

IntMul.Kappa.R6.IL2C.keyMid_fsp

by xuanji · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

The eleven updates: stU 1; phK; stU (-1); phK; stT realise Psi and Tl.

The following holds (Lean statement, in the scope of module Solutions.R6IL2CKeyRunB):

theorem IntMul.Kappa.R6.IL2C.keyMid_fsp {l : Lay} {K ρ G n L M Bb : ℕ} (hV : KVal l K ρ G n L M Bb)
    {s : IState HS} {G0 : Fin HS → List ℤ} (hc : G0 IntMul.Kappa.R6.IL2C.rC = []) (hE : KEnv (encK s G0) l K ρ G n)
    {x t u y : ℕ} (hx : x < l.QL) (ht : t < l.QC) (hu : u < l.QC) (hy : y < l.QL) :
    ∃ t4 u2 y4 : ℕ, Psi K ρ G n L x ⟨t, u, y⟩ = ⟨t4, u2, y4⟩ ∧ t4 < l.QC ∧ u2 < l.QC ∧
      Tl K ρ n x y4 < l.QL ∧
      ∀ {rest : RS} {fin : IState HS} {c : ℕ},
        FSp rest (encK s (IntMul.Kappa.R6.IL2C.KS G0 n ((2 : ℤ) ^ G) x t4 u2 (Tl K ρ n x y4))) fin c →
        FSp (.seq (stU 1) (.seq phK (.seq (stU (-1)) (.seq phK (.seq IntMul.Kappa.R6.IL2C.stT rest)))))
          (encK s (IntMul.Kappa.R6.IL2C.KS G0 n ((2 : ℤ) ^ G) x t u y)) fin (IntMul.Kappa.R6.IL2C.cMid Bb n + c)

Context. Round six, compact controls (I2C): the run of the key program, part B

The eleven register updates of keyProgC (keyMid_fsp, continuation style).

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_Defs21

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2C
open NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul NLogN.RS

Formal statement

theorem IntMul.Kappa.R6.IL2C.keyMid_fsp {l : Lay} {K ρ G n L M Bb : ℕ} (hV : KVal l K ρ G n L M Bb)
    {s : IState HS} {G0 : Fin HS → List ℤ} (hc : G0 IntMul.Kappa.R6.IL2C.rC = []) (hE : KEnv (encK s G0) l K ρ G n)
    {x t u y : ℕ} (hx : x < l.QL) (ht : t < l.QC) (hu : u < l.QC) (hy : y < l.QL) :
    ∃ t4 u2 y4 : ℕ, Psi K ρ G n L x ⟨t, u, y⟩ = ⟨t4, u2, y4⟩ ∧ t4 < l.QC ∧ u2 < l.QC ∧
      Tl K ρ n x y4 < l.QL ∧
      ∀ {rest : RS} {fin : IState HS} {c : ℕ},
        FSp rest (encK s (IntMul.Kappa.R6.IL2C.KS G0 n ((2 : ℤ) ^ G) x t4 u2 (Tl K ρ n x y4))) fin c →
        FSp (.seq (stU 1) (.seq phK (.seq (stU (-1)) (.seq phK (.seq IntMul.Kappa.R6.IL2C.stT rest)))))
          (encK s (IntMul.Kappa.R6.IL2C.KS G0 n ((2 : ℤ) ^ G) x t u y)) fin (IntMul.Kappa.R6.IL2C.cMid Bb n + c) := 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.IL2C.keyMid_fsp`, Solutions/R6IL2CKeyRunB.lean (lines 20–90) of the round-six development.

View graph