All data facts of the scalar side (round six, `maskAll`)

Proved

IntMul.Kappa.R6.Cx.NetEff.maskAll

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

complexity-theoryinteger-multiplicationkappa-improvement

All data facts of the scalar side.

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

theorem IntMul.Kappa.R6.Cx.NetEff.maskAll : MaskOK dat ∧ GOK (dat.gates.flatMap gq) ∧ (∀ t < NV, dat.src t < NR) ∧ RdOK dat ∧
    dat.pieces.length = NV

Context. The mask identity for the network data

Chains the kernel segment checks chkM0 … chkM6 (gate DAG on spread inputs), the placement check chkMP and the readout check chkMR into MaskOK dat, plus the range facts used by the stage effects (NetEff.stage1, NetEff.stage2).

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_Defs24
import Definitions.Def_IntMul_Kappa_R6_Data_CxNetData_1

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.NetEff
open IntMul.Kappa.R6.Cx.NetBT IntMul.Kappa.R6.Cx.NetSpec IntMul.Kappa.R6.Cx.NetFast IntMul.Kappa.R6.Cx.NetMask IntMul.Kappa.R6.Cx.NetData

Formal statement

theorem IntMul.Kappa.R6.Cx.NetEff.maskAll : MaskOK dat ∧ GOK (dat.gates.flatMap gq) ∧ (∀ t < NV, dat.src t < NR) ∧ RdOK dat ∧
    dat.pieces.length = NV := 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.NetEff.maskAll`, Solutions/R6CxNetMaskAll.lean (lines 50–88) of the round-six development.

View graph