A node level (round six, `lv_node`)

Proved

IntMul.Kappa.R6.IL3H.lv_node

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

complexity-theoryinteger-multiplicationkappa-improvement

A node level.

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

theorem IntMul.Kappa.R6.IL3H.lv_node (hc : CfgOK c) {rowC : IStmt HS Pp} {aK : ℕ → ℝ} {τ : ℝ}
    {G : ℕ} (hRow : RowUCG c.m τ Isym tbl rowC aK G) (haK : ∀ K, 0 ≤ aK K) (hτ : 0 ≤ τ)
    {jL : Fin Pp} (hj : tbl jL = levCH c jL rowC) {K r Z Zr H : ℕ} (hK6 : 6 ≤ K) (hr : 1 ≤ r)
    (hZG : 4 * Z * (Z + 2) ≤ 2 ^ G) (hGK : 16 * Z * (Z + 2) * 2 ^ G ≤ 2 ^ K) (hGz : zsz (G : ℤ) ≤ Zr)
    (hZZ : Z ≤ Zr) (hZr : Zr + 2 ≤ r) (hHZ : H + 1 < 2 ^ Z)
    (hz3 : 3 ≤ Zr) {CB : ℕ → ℝ} (hCB : CBRec c aK τ K CB) {E : ℕ} (hE2 : 2 * c.m ≤ E)
    (IH : ∀ E' < E, LvH c Isym tbl jL rowC K r Z Zr H G CB E') :
    LvH c Isym tbl jL rowC K r Z Zr H G CB E

Context. Round six, item language (I3): the node levels and every level

lv_node: the level claim on E ≥ 2m bits from the claims on fewer bits;
lvH_all: the level claim on every number of bits (strong induction), for any cost coefficients satisfying the cost recursion CBRec.

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}

Formal statement

theorem IntMul.Kappa.R6.IL3H.lv_node (hc : CfgOK c) {rowC : IStmt HS Pp} {aK : ℕ → ℝ} {τ : ℝ}
    {G : ℕ} (hRow : RowUCG c.m τ Isym tbl rowC aK G) (haK : ∀ K, 0 ≤ aK K) (hτ : 0 ≤ τ)
    {jL : Fin Pp} (hj : tbl jL = levCH c jL rowC) {K r Z Zr H : ℕ} (hK6 : 6 ≤ K) (hr : 1 ≤ r)
    (hZG : 4 * Z * (Z + 2) ≤ 2 ^ G) (hGK : 16 * Z * (Z + 2) * 2 ^ G ≤ 2 ^ K) (hGz : zsz (G : ℤ) ≤ Zr)
    (hZZ : Z ≤ Zr) (hZr : Zr + 2 ≤ r) (hHZ : H + 1 < 2 ^ Z)
    (hz3 : 3 ≤ Zr) {CB : ℕ → ℝ} (hCB : CBRec c aK τ K CB) {E : ℕ} (hE2 : 2 * c.m ≤ E)
    (IH : ∀ E' < E, LvH c Isym tbl jL rowC K r Z Zr H G CB E') :
    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_node`, Solutions/R6IL3Lev3.lean (lines 35–162) of the round-six development.

View graph