A uniform stream program on one role (round six, `rImplQ_onRole`)

Proved

NLogN.KFW.rImplQ_onRole

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

complexity-theoryinteger-multiplicationkappa-improvement

A uniform stream program on one role.

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

theorem NLogN.KFW.rImplQ_onRole (hW : 0 < W) (w : Fin W) {ι : Type*} [Fintype ι] [DecidableEq ι]
    {r n : ℕ} (hr : 0 < r) (hn : 0 < n) (st' : ι → ℕ) (Tw : Matrix (ι → Fin 2) (ι → Fin 2) ℂ)
    {U : IStmt HS Pp} {e dw : ℕ} {cost : ℕ → ℕ}
    (h : SImplQ I iprog Q lo hi r st' n Tw U e dw cost) (st : Fin m × κ → ℕ)
    (A : ROp (Fin W) m κ)
    (hA : ∀ X : Fin W → List (Fin r → ℂ), (∀ v, (X v).length = n) →
      roleOpF st n A X = Function.update X w (selOpF st' n Tw (X w)))
    (Z : ℕ) (hZ : zsz ((2 * (W * (n * r)) : ℕ) : ℤ) ≤ Z)
    {σ : Fin HS → Option ℤ} {ρ ρE : Fin HS} (hR : WReg σ ρ ρE (n * r) e)
    (hQ : ∀ s, Q s → Agree σ s) :
    RImplQ I iprog Q lo hi r n st A (wrapQ W w.val ρ ρE U) e (dw + (e + 2) * W)
      (cWrapQ W (n * r) Z e dw cost)

Context. KFW: a uniform program on one role

wrapQ W w ρ ρE U: swap role w to the front, run U on the first segment, level the other roles by 2^e (the shift read from ρE), swap back. The role length is read from ρ.

rImplQ_onRole: the uniform analogue of KFN.rImplI_onRole.

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFW
open IntMul NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN Complex P8Lift Butterfly
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
variable {W m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]
variable {Q : IState HS → Prop} {lo hi : ℕ}

Formal statement

theorem NLogN.KFW.rImplQ_onRole (hW : 0 < W) (w : Fin W) {ι : Type*} [Fintype ι] [DecidableEq ι]
    {r n : ℕ} (hr : 0 < r) (hn : 0 < n) (st' : ι → ℕ) (Tw : Matrix (ι → Fin 2) (ι → Fin 2) ℂ)
    {U : IStmt HS Pp} {e dw : ℕ} {cost : ℕ → ℕ}
    (h : SImplQ I iprog Q lo hi r st' n Tw U e dw cost) (st : Fin m × κ → ℕ)
    (A : ROp (Fin W) m κ)
    (hA : ∀ X : Fin W → List (Fin r → ℂ), (∀ v, (X v).length = n) →
      roleOpF st n A X = Function.update X w (selOpF st' n Tw (X w)))
    (Z : ℕ) (hZ : zsz ((2 * (W * (n * r)) : ℕ) : ℤ) ≤ Z)
    {σ : Fin HS → Option ℤ} {ρ ρE : Fin HS} (hR : WReg σ ρ ρE (n * r) e)
    (hQ : ∀ s, Q s → Agree σ s) :
    RImplQ I iprog Q lo hi r n st A (wrapQ W w.val ρ ρE U) e (dw + (e + 2) * W)
      (cWrapQ W (n * r) Z e dw cost) := 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 `NLogN.KFW.rImplQ_onRole`, Solutions/KFWWrap.lean (lines 47–208) of the round-six development.

View graph