Round-six lemma `net_main`

Proved

IntMul.Kappa.R6.Cx.NetG.net_main

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem IntMul.Kappa.R6.Cx.NetG.net_main (F : Rl × Addr 576 κ → ℂ) (hF : ∀ n z, F (Sum.inr n, z) = 0) (w : Fin Wn)
    (x : Addr 576 κ) :
    (denListH (chEx (κ := κ)) net *ᵥ F) (Sum.inl w, x) =
      ((Butterfly.tens Cm : Op (Fin 576 × κ)) *ᵥ fun z => F (Sum.inl w, z)) x

Context. Track B: the round-six complex network as a Prop8IfaceH

net = Z_u on every X ++ steps of CH ++ i^{wt u} Z_u on every Y ++ (X ↔ Y), on the roles Fin 207387136 ⊕ Fin 4193728.

net_correct: for every column type κ, the data block of its denotation is C^{⊗} on every data role (clean temporaries), from prog_sim with the initial labels g0, the final labels gF_* and the logical effect ΛF_*, as in P8Lift.prog_correct;
net_widths: its child widths are progWidths CH (histogram cxR6, all < 576).

cxNetR6 : ∃ T, Nonempty (Prop8IfaceH 207387136 T 576 Jain.cxR6).

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.NetG
attribute [local irreducible] IntMul.Kappa.R6.Cx.NetG.G1 IntMul.Kappa.R6.Cx.NetG.G2 IntMul.Kappa.R6.Cx.NetG.cs1 IntMul.Kappa.R6.Cx.NetG.cs2 IntMul.Kappa.R6.Cx.NetG.E4mv IntMul.Kappa.R6.Cx.NetG.S1 IntMul.Kappa.R6.Cx.NetG.E4s IntMul.Kappa.R6.Cx.NetG.S2 IntMul.Kappa.R6.Cx.NetG.KK IntMul.Kappa.R6.Cx.NetG.PL IntMul.Kappa.R6.Cx.NetG.CH
open Matrix Finset Matrix.Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 IntMul.Kappa.R6.Cx.NetF2 IntMul.Kappa.R6.Cx.NetT IntMul.Kappa.R6.Cx.NetLoc IntMul.Kappa.R6.Cx.NetSpec IntMul.Kappa.R6.Cx.NetBT IntMul.Kappa.R6.Cx.NetFast IntMul.Kappa.R6.Cx.NetMask IntMul.Kappa.R6.Cx.NetData IntMul.Kappa.R6.Cx.NetEff IntMul.Kappa.R6.Cx.NetSeg IntMul.Kappa.R6.Cx.NetScal IntMul.Kappa.R6.Cx.NetFr IntMul.Kappa.R6.Cx.NetRaw Complex Butterfly P8Lift
variable {κ : Type} [Fintype κ] [DecidableEq κ]

Formal statement

theorem IntMul.Kappa.R6.Cx.NetG.net_main (F : Rl × Addr 576 κ → ℂ) (hF : ∀ n z, F (Sum.inr n, z) = 0) (w : Fin Wn)
    (x : Addr 576 κ) :
    (denListH (chEx (κ := κ)) net *ᵥ F) (Sum.inl w, x) =
      ((Butterfly.tens Cm : Op (Fin 576 × κ)) *ᵥ fun z => F (Sum.inl w, z)) x := 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.NetG.net_main`, Solutions/R6CxNetFinal.lean (lines 166–289) of the round-six development.

View graph