Round-six lemma `KK_log`

Proved

IntMul.Kappa.R6.Cx.NetG.KK_log

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.R6CxNetGlobS):

theorem IntMul.Kappa.R6.Cx.NetG.KK_log : ∀ (P : List (ℕ × ℕ)), P.Nodup → (∀ p ∈ P, p.1 < NV ∧ p.2 < NV) →
    ∀ Λ : Rl → Vt, (∀ p ∈ P, Λ (τr p.1 p.2) = 0) →
      (∀ p ∈ P, runOps (progOps (P.flatMap K)) Λ (Xr p.1 p.2) = -Λ (Xr p.1 p.2)) ∧
      (∀ p ∈ P, runOps (progOps (P.flatMap K)) Λ (Yr p.1 p.2) = Λ (Yr p.1 p.2) + Λ (Xr p.1 p.2)) ∧
      (∀ r, (∀ p ∈ P, r ≠ Xr p.1 p.2 ∧ r ≠ Yr p.1 p.2 ∧ r ≠ τr p.1 p.2) →
        runOps (progOps (P.flatMap K)) Λ r = Λ r)

Context. The logical effect of the global chunk program

With all temporaries starting at zero (Λ0 (inr _) = 0), the logical state after CH is, on the data roles, X(a,b) ↦ Y0(a,b), Y(a,b) ↦ X0(a,b), A ↦ A0 (ΛF_X, ΛF_Y, ΛF_A1, ΛF_A2): stage one adds X to Y, stage two subtracts Y from X, the corrections fix the signs.

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
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
variable {Vt : Type*} [AddCommGroup Vt] [Module ℂ Vt]
variable (Λ0 : Rl → Vt) (htemp : ∀ n, Λ0 (Sum.inr n) = 0)
include htemp
omit htemp

Formal statement

theorem IntMul.Kappa.R6.Cx.NetG.KK_log : ∀ (P : List (ℕ × ℕ)), P.Nodup → (∀ p ∈ P, p.1 < NV ∧ p.2 < NV) →
    ∀ Λ : Rl → Vt, (∀ p ∈ P, Λ (τr p.1 p.2) = 0) →
      (∀ p ∈ P, runOps (progOps (P.flatMap K)) Λ (Xr p.1 p.2) = -Λ (Xr p.1 p.2)) ∧
      (∀ p ∈ P, runOps (progOps (P.flatMap K)) Λ (Yr p.1 p.2) = Λ (Yr p.1 p.2) + Λ (Xr p.1 p.2)) ∧
      (∀ r, (∀ p ∈ P, r ≠ Xr p.1 p.2 ∧ r ≠ Yr p.1 p.2 ∧ r ≠ τr p.1 p.2) →
        runOps (progOps (P.flatMap K)) Λ r = Λ r) := 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.KK_log`, Solutions/R6CxNetGlobS.lean (lines 167–220) of the round-six development.

View graph