Round-six lemma `coeff_mod_two`

Proved

IntMul.Kappa.R6.Bit.coeff_mod_two

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

complexity-theoryinteger-multiplicationkappa-improvement

|S ∩ T| + [|S ∩ T| = 1] ≡ [S = T] (mod 2) for triples.

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

theorem IntMul.Kappa.R6.Bit.coeff_mod_two {S T : Finset (Fin h)} (hS : S.card = 3) (hT : T.card = 3) :
    ((S ∩ T).card + if (S ∩ T).card = 1 then 1 else 0) % 2 = if S = T then 1 else 0

Context. Round six, bit side: data-free scalar facts of the invocation word

The scalar part of one invocation (L, J, L⁻¹, V, L, J, L⁻¹, V, dirty scratch, characteristic two) and the coefficient identity behind it, stated for any modules (in particular for the module of formal frame values of R6BitNBFormal, where the two-stage motif needs them):

word_dirty: with an invertible producer A on the scratch, an injection B (scratch → targets) and a source copy C (inputs → scratch), the word restores arbitrary scratch and adds B (A (C x)) to the targets;
coeff_mod_two: for triples S, T, |S ∩ T| + [|S ∩ T| = 1] ≡ [S = T] (mod 2);
inject_identity: if target T receives the retained point totals star c (c ∈ T) and the excluded sums star c \ (star t₁ ∪ star t₂) (T = {c, t₁, t₂}), the total injected into T is x_T (in characteristic two). This is the identity M = I of the scalar exchange.

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

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6
variable {h : ℕ}

Formal statement

theorem IntMul.Kappa.R6.Bit.coeff_mod_two {S T : Finset (Fin h)} (hS : S.card = 3) (hT : T.card = 3) :
    ((S ∩ T).card + if (S ∩ T).card = 1 then 1 else 0) % 2 = if S = T then 1 else 0 := 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.coeff_mod_two`, Solutions/R6BitNBWord.lean (lines 57–69) of the round-six development.

View graph