Stage two, checked (round six, `stage2Seg`)

Proved

IntMul.Kappa.R6.Cx.NetSeg.stage2Seg

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

complexity-theoryinteger-multiplicationkappa-improvement

Stage two, checked.

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

theorem IntMul.Kappa.R6.Cx.NetSeg.stage2Seg (hD : DataOK dat) (hw : S2_0.wf 8 = true) :
    Seg NL (mvOK2 dat) wd2 (specs2 dat) S2_0 S2_14 (H2_0 + H2_1 + H2_2 + H2_3 + H2_4 + H2_5 + H2_6 + H2_7 + H2_8 + H2_9 + H2_10 + H2_11 + H2_12 + H2_13) (51232 + 24335 + 9328 + 7228 + 8554 + 8886 + 8436 + 8309 + 7634 + 7034 + 6335 + 10138 + 18629 + 51232) ∧ S2_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.stage2Seg (hD : DataOK dat) (hw : S2_0.wf 8 = true) :
    Seg NL (mvOK2 dat) wd2 (specs2 dat) S2_0 S2_14 (H2_0 + H2_1 + H2_2 + H2_3 + H2_4 + H2_5 + H2_6 + H2_7 + H2_8 + H2_9 + H2_10 + H2_11 + H2_12 + H2_13) (51232 + 24335 + 9328 + 7228 + 8554 + 8886 + 8436 + 8309 + 7634 + 7034 + 6335 + 10138 + 18629 + 51232) ∧ S2_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.stage2Seg`, Solutions/R6CxNetSeg.lean (lines 135–153) of the round-six development.

View graph