Stage one, checked (round six, `stage1Seg`)

Proved

IntMul.Kappa.R6.Cx.NetSeg.stage1Seg

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

complexity-theoryinteger-multiplicationkappa-improvement

Stage one, checked.

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

theorem IntMul.Kappa.R6.Cx.NetSeg.stage1Seg (hD : DataOK dat) (hw : S1_0.wf 8 = true) :
    Seg NL mvOK1 wd1 (specs1 dat) S1_0 S1_14 (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) (2024 + 16654 + 10476 + 6218 + 7203 + 7661 + 8320 + 8429 + 8886 + 8455 + 6887 + 9328 + 22288 + 51225) ∧ S1_14.wf 8 = true

Context. Chaining the kernel label checks of the two stage programs

stage1Seg / stage2Seg: the checked programs specs1 dat / specs2 dat from the snapshot states S1_0 / S2_0 are valid (progChk … = true), with the summed packed histograms and move counts, ending in S1_14 / S2_14.

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.NetSeg
open IntMul.Kappa.R6.Cx.NetBT IntMul.Kappa.R6.Cx.NetLoc IntMul.Kappa.R6.Cx.NetSpec IntMul.Kappa.R6.Cx.NetFast IntMul.Kappa.R6.Cx.NetRaw IntMul.Kappa.R6.Cx.NetData IntMul.Kappa.R6.Cx.NetEff
variable {nl : ℕ} {mvOK : ℕ → ℕ → ℕ → Bool} {wd : ℕ → ℕ → ℕ → ℕ}

Formal statement

theorem IntMul.Kappa.R6.Cx.NetSeg.stage1Seg (hD : DataOK dat) (hw : S1_0.wf 8 = true) :
    Seg NL mvOK1 wd1 (specs1 dat) S1_0 S1_14 (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) (2024 + 16654 + 10476 + 6218 + 7203 + 7661 + 8320 + 8429 + 8886 + 8455 + 6887 + 9328 + 22288 + 51225) ∧ S1_14.wf 8 = true := 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.NetSeg.stage1Seg`, Solutions/R6CxNetSeg.lean (lines 115–133) of the round-six development.

View graph