The correction (round six, `corrG_fsp`)

Proved

IntMul.Kappa.R6.IL2C.corrG_fsp

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

complexity-theoryinteger-multiplicationkappa-improvement

The correction with an abstract key program: flR recs M ↦ flR (recs ∘ γ) M.

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

theorem IntMul.Kappa.R6.IL2C.corrG_fsp {kp : RS} {κ γ : ℕ → ℕ} {B M cK : ℕ} (hB : 1 ≤ B) (hM : 1 ≤ M)
    (hγκ : ∀ m, γ (κ m) = m) (hκγ : ∀ m, κ (γ m) = m) (hκ : ∀ m < M, κ m < M)
    (hγ : ∀ m < M, γ m < M) (hw : c1 ∉ kp.writes)
    (recs : ℕ → List ℤ) (hlen : ∀ m, (recs m).length = B) (hbits : ∀ m, Bnd 1 (recs m))
    (s : IState HS) (hkp : KeyOK kp s κ M cK) :
    FSp (corrG kp B M (zsz ((M * B : ℕ) : ℤ)))
      (encK s (Function.update (fun _ => []) 0 (flR recs M)))
      (encK s (Function.update (fun _ => []) 0 (flR (fun d => recs (γ d)) M)))
      (cCorrG cK B M (zsz ((M * B : ℕ) : ℤ)) (nMv κ M) (zsz ((M * B : ℕ) : ℤ) + 3))

Context. Round six, compact controls (I2C): the correction with an abstract key program

corrG kp B M A is KFL.corrRS with the key program keyProg replaced by any register program kp that pushes a key κ k on rK (KeyOK); the radix sort and pass 3 are the frozen ones.

corrG_fsp: for a bijection κ of ℕ (inverse γ) preserving [0, M), flR recs M ↦ flR (recs ∘ γ) M, at the cost cCorrG (moved records only in the sort).

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.corrG_fsp {kp : RS} {κ γ : ℕ → ℕ} {B M cK : ℕ} (hB : 1 ≤ B) (hM : 1 ≤ M)
    (hγκ : ∀ m, γ (κ m) = m) (hκγ : ∀ m, κ (γ m) = m) (hκ : ∀ m < M, κ m < M)
    (hγ : ∀ m < M, γ m < M) (hw : c1 ∉ kp.writes)
    (recs : ℕ → List ℤ) (hlen : ∀ m, (recs m).length = B) (hbits : ∀ m, Bnd 1 (recs m))
    (s : IState HS) (hkp : KeyOK kp s κ M cK) :
    FSp (corrG kp B M (zsz ((M * B : ℕ) : ℤ)))
      (encK s (Function.update (fun _ => []) 0 (flR recs M)))
      (encK s (Function.update (fun _ => []) 0 (flR (fun d => recs (γ d)) M)))
      (cCorrG cK B M (zsz ((M * B : ℕ) : ℤ)) (nMv κ M) (zsz ((M * B : ℕ) : ℤ) + 3)) := 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.corrG_fsp`, Solutions/R6IL2CCorr.lean (lines 186–310) of the round-six development.

View graph