Round-six lemma `pack1`

Proved

IntMul.Kappa.R6.Cx.NetG.pack1

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem IntMul.Kappa.R6.Cx.NetG.pack1 : packH h1 = H1_0 + H1_1 + H1_2 + H1_3 + H1_4 + H1_5 + H1_6 + H1_7 + H1_8 + H1_9 + H1_10 +
    H1_11 + H1_12 + H1_13

Context. The child-width histogram of the global chunk program

W1, W2 (nonzero move widths of the two checked local programs) have the histograms h1, h2 (decoded from the kernel-checked packed sums, multiset_of_pack);
progWidths CH = v copies of W1, v·R widths 552 (E4), v copies of W2, v² widths 1 (E5);
CH_hist: its multiset is histMS cxR6; CH_small: every width is < 576.

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_Defs25

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Cx IntMul.Kappa.R6.Cx.NetG
attribute [local irreducible] IntMul.Kappa.R6.Cx.NetG.G1 IntMul.Kappa.R6.Cx.NetG.G2 IntMul.Kappa.R6.Cx.NetG.cs1 IntMul.Kappa.R6.Cx.NetG.cs2 IntMul.Kappa.R6.Cx.NetG.E4mv IntMul.Kappa.R6.Cx.NetG.S1 IntMul.Kappa.R6.Cx.NetG.E4s IntMul.Kappa.R6.Cx.NetG.S2 IntMul.Kappa.R6.Cx.NetG.KK IntMul.Kappa.R6.Cx.NetG.PL
open Matrix Finset Matrix.Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 IntMul.Kappa.R6.Cx.NetF2 IntMul.Kappa.R6.Cx.NetT IntMul.Kappa.R6.Cx.NetLoc IntMul.Kappa.R6.Cx.NetSpec IntMul.Kappa.R6.Cx.NetBT IntMul.Kappa.R6.Cx.NetFast IntMul.Kappa.R6.Cx.NetMask IntMul.Kappa.R6.Cx.NetData IntMul.Kappa.R6.Cx.NetEff IntMul.Kappa.R6.Cx.NetSeg IntMul.Kappa.R6.Cx.NetScal IntMul.Kappa.R6.Cx.NetFr IntMul.Kappa.R6.Cx.NetRaw

Formal statement

theorem IntMul.Kappa.R6.Cx.NetG.pack1 : packH h1 = H1_0 + H1_1 + H1_2 + H1_3 + H1_4 + H1_5 + H1_6 + H1_7 + H1_8 + H1_9 + H1_10 +
    H1_11 + H1_12 + H1_13 := 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.Cx.NetG.pack1`, Solutions/R6CxNetHist.lean (lines 33–34) of the round-six development.

View graph