A chain level (round six, `lv_chain`)

Proved

IntMul.Kappa.R6.IL3H.lv_chain

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

complexity-theoryinteger-multiplicationkappa-improvement

A chain level.

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

theorem IntMul.Kappa.R6.IL3H.lv_chain (hc : CfgOK c) {rowC : IStmt HS Pp} {jL : Fin Pp} (hj : tbl jL = levCH c jL rowC)
    {K r Z Zr H G : ℕ} {CB : ℕ → ℝ} {aK : ℕ → ℝ} {τ : ℝ} (hCB : CBRec c aK τ K CB) (hK : 1 ≤ K)
    (hr : 1 ≤ r) (hZr : Zr + 2 ≤ r) {E : ℕ} (hE1 : 1 ≤ E) (hE2 : E < 2 * c.m)
    (IH : LvH c Isym tbl jL rowC K r Z Zr H G CB (E - 1)) :
    LvH c Isym tbl jL rowC K r Z Zr H G CB E

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_chain (hc : CfgOK c) {rowC : IStmt HS Pp} {jL : Fin Pp} (hj : tbl jL = levCH c jL rowC)
    {K r Z Zr H G : ℕ} {CB : ℕ → ℝ} {aK : ℕ → ℝ} {τ : ℝ} (hCB : CBRec c aK τ K CB) (hK : 1 ≤ K)
    (hr : 1 ≤ r) (hZr : Zr + 2 ≤ r) {E : ℕ} (hE1 : 1 ≤ E) (hE2 : E < 2 * c.m)
    (IH : LvH c Isym tbl jL rowC K r Z Zr H G CB (E - 1)) :
    LvH c Isym tbl jL rowC K r Z Zr H G CB E := 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_chain`, Solutions/R6IL3Lev2.lean (lines 99–167) of the round-six development.

View graph