The node inequality, split (`Gs_node_split`)

Proved

IntMul.Kappa.R6.IL3H.Gs_node_split

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

complexity-theoryinteger-multiplicationkappa-improvement

The node inequality, split: X = A (mF)^p with 2 ∑ Gs(sF) ≤ X, 2A ≤ X, X + E mod m ≤ Gs E.

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

theorem IntMul.Kappa.R6.IL3H.Gs_node_split {A p m E : ℕ} (ws : List ℕ) (hm : 1 ≤ m) (hp : 1 ≤ p) (hA1 : 1 ≤ A)
    (hE : 2 * m ≤ E) (hws : 2 * (ws.map fun s => (2 * s + 1) ^ p).sum ≤ (2 * m) ^ p) :
    ∃ X, 2 * (ws.map fun s => Gs A p m (s * (E / m))).sum ≤ X ∧ 2 * A ≤ X ∧
      X + E % m ≤ Gs A p m E

Context. Round six, item language (I3): the level claim and its side conditions

VbH: the size budget of a level (monotone, VbH_mono);
CfgOK c: the configuration conditions (network shape, the p-moment of the child widths, the scale constant Aw large against the local scale cLH and the local widths);
CBRec: the cost recursion the coefficients CB E must satisfy;
LvH: the level claim on E bits (scale Gs E, width (W' + 4) Gs E, cost ⌊CB E · n Y⌋);
side lemmas: het_sub, dvd_child, Gs_node_split, width_node (the width recursion), tens_fin0.

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

Formal statement

theorem IntMul.Kappa.R6.IL3H.Gs_node_split {A p m E : ℕ} (ws : List ℕ) (hm : 1 ≤ m) (hp : 1 ≤ p) (hA1 : 1 ≤ A)
    (hE : 2 * m ≤ E) (hws : 2 * (ws.map fun s => (2 * s + 1) ^ p).sum ≤ (2 * m) ^ p) :
    ∃ X, 2 * (ws.map fun s => Gs A p m (s * (E / m))).sum ≤ X ∧ 2 * A ≤ X ∧
      X + E % m ≤ Gs A p m 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.Gs_node_split`, Solutions/R6IL3Lev1.lean (lines 123–175) of the round-six development.

View graph