Label consistency of generated chunks (round six, `genF_labGates`)

Proved

IntMul.Kappa.R6.Bit.genF_labGates

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

complexity-theoryinteger-multiplicationkappa-improvement

Label consistency of generated chunks.

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

theorem IntMul.Kappa.R6.Bit.genF_labGates (hι : ∀ w w', D w → D w' → ι w = ι w' → w = w') :
    ∀ (W : List LInstr) (f : ℕ → ℕ) (L : Wr → FMat m N),
      (∀ i ∈ W, (∀ w ∈ i.2.1, D w) ∧ ∀ p ∈ i.2.2, p.1 ∈ i.2.1 ∧ p.2 ∈ i.2.1) →
      (∀ ch ∈ (genF f W).2, ∀ mv ∈ ch.2.1, edgeMat N (E mv.2 ch.1) * lab mv.2 = lab ch.1) →
      (∀ w, D w → L (ι w) = lab (f w)) →
      LabGates N (chunkProg (R := R) ι E (genF f W).2) L ∧
        (∀ w, D w → (chunkProg (R := R) ι E (genF f W).2).foldl (labStepH N) L (ι w) =
          lab ((genF f W).1 w)) ∧
        ∀ x, (∀ w, D w → ι w ≠ x) → (chunkProg (R := R) ι E (genF f W).2).foldl (labStepH N) L x = L x

Context. Round six, bit network: programs from generated chunks

A local program is a list of chunks (code, moves, gates) over local wires ℕ. Mapped to global wires by ι, a chunk becomes: one frame-change edge per move (E old code), then one XOR gate x_d ← x_d + x_s per gate.

genF_labGates: for chunks produced by genF (the label generator), all gates are label consistent (LabGates) as soon as every move edge maps the frame of its old code to the frame of its new code; the final labels are the frames of the final codes.
chunkProg_scalar: the (module-valued) scalar circuit of a mapped chunk program is the local XOR run xrL of its gates.

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_Defs51

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Bit
open R6Chk.Bit.Loc Matrix
variable {Wr : Type*} [Fintype Wr] [DecidableEq Wr] {R : Type*} [CommRing R] {m N : ℕ}
variable (ι : ℕ → Wr) (D : ℕ → Prop) (lab : ℕ → FMat m N) (E : ℕ → ℕ → Edge m)

Formal statement

theorem IntMul.Kappa.R6.Bit.genF_labGates (hι : ∀ w w', D w → D w' → ι w = ι w' → w = w') :
    ∀ (W : List LInstr) (f : ℕ → ℕ) (L : Wr → FMat m N),
      (∀ i ∈ W, (∀ w ∈ i.2.1, D w) ∧ ∀ p ∈ i.2.2, p.1 ∈ i.2.1 ∧ p.2 ∈ i.2.1) →
      (∀ ch ∈ (genF f W).2, ∀ mv ∈ ch.2.1, edgeMat N (E mv.2 ch.1) * lab mv.2 = lab ch.1) →
      (∀ w, D w → L (ι w) = lab (f w)) →
      LabGates N (chunkProg (R := R) ι E (genF f W).2) L ∧
        (∀ w, D w → (chunkProg (R := R) ι E (genF f W).2).foldl (labStepH N) L (ι w) =
          lab ((genF f W).1 w)) ∧
        ∀ x, (∀ w, D w → ι w ≠ x) → (chunkProg (R := R) ι E (genF f W).2).foldl (labStepH N) L x = L 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.Bit.genF_labGates`, Solutions/R6BitNBLabGen.lean (lines 143–206) of the round-six development.

View graph