The two tests of a level (round six, `lv_wrap`)

Proved

IntMul.Kappa.R6.IL3H.lv_wrap

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

complexity-theoryinteger-multiplicationkappa-improvement

The two tests of a level around the chain/node branch.

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

theorem IntMul.Kappa.R6.IL3H.lv_wrap {ι : Type*} [Fintype ι] [DecidableEq ι] {st : ι → ℕ} {n : ℕ}
    {rowC : IStmt HS Pp} {jL : Fin Pp} (hL : LevRH c σ K t S0 r H E e B) (hE1 : 1 ≤ E)
    (hm : 1 ≤ c.m) (Zr M : ℕ) (hMZ : zsz (M : ℤ) ≤ Zr) (hM : E + 2 * c.m + 1 ≤ M)
    (hZr : Zr + 2 ≤ r) {e' dw : ℕ} (CBE : ℝ) (cost0 : ℕ → ℕ)
    (Hin : SImplQ Isym tbl (fun s => Agree (σPush σ [((19 : Fin HS),
        (((ltNE c).val (vOf σ) : ℕ) : ℤ))]) s) 0 H r st n (tens Cm)
      (if (ltNE c).val (vOf σ) = 0 then IntMul.Kappa.R6.IL3H.chainC jL else IntMul.Kappa.R6.IL3H.nodeC c jL rowC) e' dw cost0)
    (hc : ∀ w, w + dw ≤ H →
      (cost0 w : ℝ) + 10 ^ 9 * (Yu r Zr H : ℝ) ≤ CBE * ((n * Yu r Zr H : ℕ) : ℝ)) :
    SImplQ Isym tbl (fun s => Agree σ s) 0 H r st n (tens Cm) (levCH c jL rowC) e' dw
      (fun _ => ⌊CBE * ((n * Yu r Zr H : ℕ) : ℝ)⌋₊)

Context. Round six, item language (I3): the empty level, the level wrapper, the chain levels

lv_wrap: the zero test on vk and the chain test on 19 around the chain/node branch;
lv_zero: the level claim on 0 bits (skip);
lv_chain: the level claim on 1 ≤ E < 2m bits from the claim on E - 1 bits.

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_Defs22

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL3H
open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW Complex P8Lift Butterfly IntMul.Kappa.R6.Cx
variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}
variable {c : IntMul.Kappa.R6.IL3H.Cfg} {σ : Fin HS → Option ℤ} {K t S0 r H E e B : ℕ}

Formal statement

theorem IntMul.Kappa.R6.IL3H.lv_wrap {ι : Type*} [Fintype ι] [DecidableEq ι] {st : ι → ℕ} {n : ℕ}
    {rowC : IStmt HS Pp} {jL : Fin Pp} (hL : LevRH c σ K t S0 r H E e B) (hE1 : 1 ≤ E)
    (hm : 1 ≤ c.m) (Zr M : ℕ) (hMZ : zsz (M : ℤ) ≤ Zr) (hM : E + 2 * c.m + 1 ≤ M)
    (hZr : Zr + 2 ≤ r) {e' dw : ℕ} (CBE : ℝ) (cost0 : ℕ → ℕ)
    (Hin : SImplQ Isym tbl (fun s => Agree (σPush σ [((19 : Fin HS),
        (((ltNE c).val (vOf σ) : ℕ) : ℤ))]) s) 0 H r st n (tens Cm)
      (if (ltNE c).val (vOf σ) = 0 then IntMul.Kappa.R6.IL3H.chainC jL else IntMul.Kappa.R6.IL3H.nodeC c jL rowC) e' dw cost0)
    (hc : ∀ w, w + dw ≤ H →
      (cost0 w : ℝ) + 10 ^ 9 * (Yu r Zr H : ℝ) ≤ CBE * ((n * Yu r Zr H : ℕ) : ℝ)) :
    SImplQ Isym tbl (fun s => Agree σ s) 0 H r st n (tens Cm) (levCH c jL rowC) e' dw
      (fun _ => ⌊CBE * ((n * Yu r Zr H : ℕ) : ℝ)⌋₊) := 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.lv_wrap`, Solutions/R6IL3Lev2.lean (lines 30–73) of the round-six development.

View graph