The wrapper with `skip` on a zero role (round six, `wrapQ_zero`)

Proved

IntMul.Kappa.R6.IL3H.wrapQ_zero

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

complexity-theoryinteger-multiplicationkappa-improvement

The wrapper with skip on a zero role.

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

theorem IntMul.Kappa.R6.IL3H.wrapQ_zero {r n : ℕ} (hr : 0 < r) (hn : 0 < n) {e : ℕ} (Z : ℕ)
    (hZ : zsz ((2 * (2 * (n * r)) : ℕ) : ℤ) ≤ Z)
    {σ : Fin HS → Option ℤ} {ρ ρE : Fin HS} (hR : WReg σ ρ ρE (n * r) e)
    (s : IState HS) (hs : Agree σ s) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ)
    (xs : List (Fin r → ℂ)) (F x : ℕ) (hC : Clean0 f) (h0 : f 0 = gflat zs ++ l)
    (hxs : xs.length = n) (hx : RecRep r F zs (xs ++ List.replicate n 0)) (hb : GB x zs) :
    ∃ zs', RecRep r (F + e) zs' (xs ++ List.replicate n 0) ∧ GB (x + (e + 2) * 2) zs' ∧
      IRuns I iprog (wrapQ 2 1 ρ ρE (.skip : IStmt HS Pp)) (encK s f)
        (encK s (Function.update f 0 (gflat zs' ++ l))) (cWrapQ 2 (n * r) Z e 0 (fun _ => 1) x)

Context. Round six, item language (I3): the scale pad

scaleQ xL xQ ρ ρE = padCU xL xQ (wrapQ 2 1 ρ ρE .skip): append n zero records, swap the zero half to the front, level the data half by 2^e, swap back, drop the zeros.

wrapQ_zero: the wrapper with U = skip on a zero role (zeros sit at every scale);
sImplQ_scale: scaleQ implements the identity with scale shift e.

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 IntMul IntMul.Kappa IntMul.Kappa.R6
open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW Complex P8Lift Butterfly
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

Formal statement

theorem IntMul.Kappa.R6.IL3H.wrapQ_zero {r n : ℕ} (hr : 0 < r) (hn : 0 < n) {e : ℕ} (Z : ℕ)
    (hZ : zsz ((2 * (2 * (n * r)) : ℕ) : ℤ) ≤ Z)
    {σ : Fin HS → Option ℤ} {ρ ρE : Fin HS} (hR : WReg σ ρ ρE (n * r) e)
    (s : IState HS) (hs : Agree σ s) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ)
    (xs : List (Fin r → ℂ)) (F x : ℕ) (hC : Clean0 f) (h0 : f 0 = gflat zs ++ l)
    (hxs : xs.length = n) (hx : RecRep r F zs (xs ++ List.replicate n 0)) (hb : GB x zs) :
    ∃ zs', RecRep r (F + e) zs' (xs ++ List.replicate n 0) ∧ GB (x + (e + 2) * 2) zs' ∧
      IRuns I iprog (wrapQ 2 1 ρ ρE (.skip : IStmt HS Pp)) (encK s f)
        (encK s (Function.update f 0 (gflat zs' ++ l))) (cWrapQ 2 (n * r) Z e 0 (fun _ => 1) x) := 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.IL3H.wrapQ_zero`, Solutions/R6IL3Pad.lean (lines 33–173) of the round-six development.

View graph