The dirty-scratch word (round six, `word_dirty`)

Proved

IntMul.Kappa.R6.Bit.word_dirty

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

complexity-theoryinteger-multiplicationkappa-improvement

The dirty-scratch word. A and A' are inverse on the scratch. Starting from any scratch s, the word L J L⁻¹ V L J L⁻¹ V ends with scratch s and targets y + B (A (C x)).

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

theorem IntMul.Kappa.R6.Bit.word_dirty (hy : ∀ z : My, z + z = 0) (hs : ∀ z : Ms, z + z = 0)
    (A A' : Ms →ₗ[R] Ms) (hA : ∀ z, A' (A z) = z) (B : Ms →ₗ[R] My) (C : Mx →ₗ[R] Ms)
    (x : Mx) (y : My) (s : Ms) :
    let s1 := A s
    let y1 := y + B s1
    let s2 := A' s1
    let s3 := s2 + C x
    let s4 := A s3
    let y2 := y1 + B s4
    let s5 := A' s4
    let s6 := s5 + C x
    s6 = s ∧ y2 = y + B (A (C x))

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 {R : Type*} [CommRing R] {Mx My Ms : Type*} [AddCommGroup Mx] [AddCommGroup My]
  [AddCommGroup Ms] [Module R Mx] [Module R My] [Module R Ms]

Formal statement

theorem IntMul.Kappa.R6.Bit.word_dirty (hy : ∀ z : My, z + z = 0) (hs : ∀ z : Ms, z + z = 0)
    (A A' : Ms →ₗ[R] Ms) (hA : ∀ z, A' (A z) = z) (B : Ms →ₗ[R] My) (C : Mx →ₗ[R] Ms)
    (x : Mx) (y : My) (s : Ms) :
    let s1 := A s
    let y1 := y + B s1
    let s2 := A' s1
    let s3 := s2 + C x
    let s4 := A s3
    let y2 := y1 + B s4
    let s5 := A' s4
    let s6 := s5 + C x
    s6 = s ∧ y2 = y + B (A (C 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.word_dirty`, Solutions/R6BitNBWord.lean (lines 26–49) of the round-six development.

View graph