A chain level (round six, `sImplQ_chainC`)

Proved

IntMul.Kappa.R6.IL3H.sImplQ_chainC

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.R6IL3Node5):

theorem IntMul.Kappa.R6.IL3H.sImplQ_chainC {rowC : IStmt HS Pp} {jL : Fin Pp} (hj : tbl jL = levCH c jL rowC)
    (hL : LevRH c σ K t S0 r H E e B) (hE1 : 1 ≤ E) (hS : 1 ≤ S0) (hB : 1 ≤ B) (hr : 1 ≤ r)
    (hK : 1 ≤ K) (hKe : K * (E - 1) ≤ e) (het : e - e % K + K ≤ t) (Zr : ℕ)
    (hz12 : zsz ((12 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ) ≤ Zr) (hZr : Zr + 2 ≤ r)
    (M : ℕ) (hM : E + e + K + 1 ≤ M) (hMZ : zsz (M : ℤ) ≤ Zr)
    (DW1 c1 : ℕ)
    (IH : SImplQ Isym tbl (fun s => Agree (σPush σ (frV σ chainFr)) s) 0 H r
      (fun j : Fin (E - 1) => 2 ^ ((e - K) - K * j.val) * S0) (nN B t S0)
      (tens Cm) (levCH c jL rowC) (c.G (E - 1)) DW1 (fun _ => c1)) :
    ∃ cost : ℕ → ℕ, SImplQ Isym tbl (fun s => Agree σ s) 0 H r
      (fun i : Fin E => 2 ^ (e - K * i.val) * S0) (nN B t S0) (tens Cm) (IntMul.Kappa.R6.IL3H.chainC jL)
      (ES 0 + c.G (E - 1)) (2 + DW1) cost ∧
      ∀ w, w + (2 + DW1) ≤ H → cost w ≤ c1 + 10 ^ 13 * (nN B t S0 * Yu r Zr H)

Context. Round six, item language (I3): a chain level

For 1 ≤ E < 2m, chainC jL (the frozen kernel on bit e in a level-0 frame, then the level call on the E - 1 bits below) implements tens Cm on the E bits, with scale 1 + (E - 1), width 2 + DW₁ and cost ≤ c₁ + 10^13 · n Y (sImplQ_chainC).

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.sImplQ_chainC {rowC : IStmt HS Pp} {jL : Fin Pp} (hj : tbl jL = levCH c jL rowC)
    (hL : LevRH c σ K t S0 r H E e B) (hE1 : 1 ≤ E) (hS : 1 ≤ S0) (hB : 1 ≤ B) (hr : 1 ≤ r)
    (hK : 1 ≤ K) (hKe : K * (E - 1) ≤ e) (het : e - e % K + K ≤ t) (Zr : ℕ)
    (hz12 : zsz ((12 * (B * 2 ^ t * S0 * r) : ℕ) : ℤ) ≤ Zr) (hZr : Zr + 2 ≤ r)
    (M : ℕ) (hM : E + e + K + 1 ≤ M) (hMZ : zsz (M : ℤ) ≤ Zr)
    (DW1 c1 : ℕ)
    (IH : SImplQ Isym tbl (fun s => Agree (σPush σ (frV σ chainFr)) s) 0 H r
      (fun j : Fin (E - 1) => 2 ^ ((e - K) - K * j.val) * S0) (nN B t S0)
      (tens Cm) (levCH c jL rowC) (c.G (E - 1)) DW1 (fun _ => c1)) :
    ∃ cost : ℕ → ℕ, SImplQ Isym tbl (fun s => Agree σ s) 0 H r
      (fun i : Fin E => 2 ^ (e - K * i.val) * S0) (nN B t S0) (tens Cm) (IntMul.Kappa.R6.IL3H.chainC jL)
      (ES 0 + c.G (E - 1)) (2 + DW1) cost ∧
      ∀ w, w + (2 + DW1) ≤ H → cost w ≤ c1 + 10 ^ 13 * (nN B t S0 * 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.sImplQ_chainC`, Solutions/R6IL3Node5.lean (lines 27–89) of the round-six development.

View graph