The round-six complex network in the item-language gate class (round six, `cxNetR6G`)

Proved

IntMul.Kappa.R6.Cx.cxNetR6G

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

complexity-theoryinteger-multiplicationkappa-improvement

The round-six complex network in the item-language gate class.

The following holds (Lean statement, in the scope of module R6Pk.R6CxNetG):

theorem IntMul.Kappa.R6.Cx.cxNetR6G : ∃ T, ∃ J : Prop8IfaceH 207387136 T 576 IntMul.Kappa.Jain.cxR6, ∃ A, GClassH J A

Context. The round-six complex network in the item-language gate class (GClassH)

R6CxNetFinal.net uses mergedChunk (an opaque Classical.choose of merge_chunk) for its frame changes; its steps cannot be inspected. netG is the same network with every merged chunk replaced by the explicit chunkH (row additions, one child, row additions) chosen from merge_identity: same denotation, same child widths. Its only gates are the chunk gates GOp.mat:

z_d += (k/2) z_s with d ≠ s (all local ops, C1, C2): |k| KFG atoms (d, s, sign k, h = 1);
z_X += -2 z_X (C3): the ±1 diagonal -1 at X.

cxNetR6G : ∃ T (J : Prop8IfaceH 207387136 T 576 Jain.cxR6) A, GClassH J A.

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_Kappa_R6_Defs2
import Definitions.Def_IntMul_Kappa_R6_Defs21

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Cx
open IntMul.Kappa.R6.IL3H

Formal statement

theorem IntMul.Kappa.R6.Cx.cxNetR6G : ∃ T, ∃ J : Prop8IfaceH 207387136 T 576 IntMul.Kappa.Jain.cxR6, ∃ A, GClassH J A := 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.cxNetR6G`, Solutions/R6CxNetG.lean (lines 482–485) of the round-six development.

View graph