The rebuild of a gate computes `gateApply` (`sumS_gate`)

Proved

IntMul.Kappa.R6.IL.sumS_gate

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

complexity-theoryinteger-multiplicationkappa-improvement

The rebuild of a gate computes gateApply.

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

theorem IntMul.Kappa.R6.IL.sumS_gate {v : ℕ} (g : Matrix (Fin W ⊕ Fin T) (Fin W ⊕ Fin T) (ZMod 2))
    (S : Finset (Fin W ⊕ Fin T)) (st : Fin W ⊕ Fin T → List (ZMod 2))
    (h : ∀ x, (st x).length = v) (n : ℕ) (hn : n < T + W) :
    sumS (tabS st) v (srcT (ngOf g S) n) = tabS (Bit.gateApply v g S st) n

Context. Round six, item language: a QHNet program on a table of T + W streams

The wires Fin W ⊕ Fin T of a round-six network are laid out as a table of T + W streams of length v on stack 0 (temporaries first: inr t ↦ t, inl w ↦ T + w, eqv).

gateH_fsp: a gate (g, S) is one fine rebuild rebuildCU (T + W) (srcT (ngOf g S)) (frozen KIL3/KFD table code), with denotation gateApply;
instrH, netH: the code of an instruction / of a program, an edge (x, e) being run in place by applyCF with an edge code E e;
netH_runs: the program code computes netRunH v impl prog whenever every edge code computes impl e on single streams (under the invariant Inv G0).

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_Defs13

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset
variable {W T m : ℕ}

Formal statement

theorem IntMul.Kappa.R6.IL.sumS_gate {v : ℕ} (g : Matrix (Fin W ⊕ Fin T) (Fin W ⊕ Fin T) (ZMod 2))
    (S : Finset (Fin W ⊕ Fin T)) (st : Fin W ⊕ Fin T → List (ZMod 2))
    (h : ∀ x, (st x).length = v) (n : ℕ) (hn : n < T + W) :
    sumS (tabS st) v (srcT (ngOf g S) n) = tabS (Bit.gateApply v g S st) n := 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.IL.sumS_gate`, Solutions/R6ILNet.lean (lines 84–127) of the round-six development.

View graph